From 72d8000f7b10146cfa0bf3f92214ae2e946abad9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= <nicolasmeric@posteo.net>
Date: Mon, 9 Jan 2023 15:34:59 +0100
Subject: [PATCH] Further explain evaluator option syntax for value_ text
 antiquotation

---
 .../technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy   | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy
index ff8c52e3..9af526d8 100644
--- a/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy
+++ b/examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy
@@ -701,6 +701,11 @@ term antiquotations:
 \<^item> \<^theory_text>\<open>@{value_ \<open>term\<close> }\<close> performs the evaluation of \<open>term\<close> with term antiquotations,
   for instance \<^theory_text>\<open>@{value_ \<open>mcc @{cenelec-term \<open>FT\<close>}\<close>}\<close>
   will print the value of the \<^const>\<open>mcc\<close> attribute of the instance \<open>FT\<close>.
+  \<^theory_text>\<open>value_\<close> may have an optional argument between square brackets to specify the evaluator but this
+  argument must be specified after a default optional argument already defined
+  by the text antiquotation implementation.
+  So one must use the following syntax if he does not want to specify the first optional argument:
+  \<open>@{value_ [] [nbe] \<open>r @{F \<open>xcv4\<close>}\<close>}\<close>. Note the empty brackets.
 \<close>
 
 (*<*)