Document term _ and value_ text antiquotations

examples/technical_report/Isabelle_DOF-Manual/03_GuidedTour.thy

@@ -692,8 +692,24 @@ text\<open>There are options to display sub-parts of formulas etc., but it is a
 of tight-checking that the information must be given complete and exactly in the syntax of
 Isabelle. This may be over-precise and a burden to readers not familiar with Isabelle, which may
 motivate authors to choose the aforementioned freeform-style.
+
+Additionally, documents antiquotations were added to check and evaluate terms with
+term antiquotations:
+\<^item> \<^theory_text>\<open>@{term_ \<open>term\<close> }\<close> parses and type-checks \<open>term\<close> with term antiquotations,
+  for instance \<^theory_text>\<open>@{term_ \<open>@{cenelec-term \<open>FT\<close>}\<close>}\<close> will parse and check
+  that \<open>FT\<close> is indeed an instance of the class \<^typ>\<open>cenelec_term\<close>,
+\<^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>.
 \<close>
 
+(*<*)
+declare_reference*["subsec:onto-term-ctxt"::technical]
+(*>*)
+
+text\<open>They are text-contexts equivalents to the \<^theory_text>\<open>term*\<close> and \<^theory_text>\<open>value*\<close> commands
+     for term-contexts introduced in @{technical (unchecked) \<open>subsec:onto-term-ctxt\<close>}\<close>
+
 subsection\<open>A Technical Report with Tight Checking\<close>
 text\<open>An example of tight checking is a small programming manual developed by the
 second author in order to document programming trick discoveries while implementing in Isabelle.

examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy

@@ -410,7 +410,7 @@ in the context of the SML toplevel of the Isabelle system as in the correspondin
 declare_reference*["text-elements-expls"::technical]
 (*>*)
 
-subsection\<open>Ontological Term-Contexts and their Management\<close>
+subsection*["subsec:onto-term-ctxt"::technical]\<open>Ontological Term-Contexts and their Management\<close>
 text\<open>The major commands providing term-contexts are 
 \<^theory_text>\<open>term*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close>,
 \<^theory_text>\<open>value*[oid::cid, ...] \<open> \<dots> HOL-term \<dots> \<close>\<close> and
@@ -418,8 +418,9 @@ text\<open>The major commands providing term-contexts are
 Wrt. creation, track-ability and checking they are analogous to the ontological text and 
 code-commands. However the argument terms may contain term-antiquotations stemming from an
 ontology definition. Both term-contexts were type-checked and \<^emph>\<open>validated\<close> against
-the global context (so: in the term \<open>@{A \<open>oid\<close>}\<close>, \<open>oid\<close> is indeed a string which refers 
-to a meta-object belonging to the document class \<open>A\<close>, for example).
+the global context (so: in the term @{term_ \<open>@{author \<open>bu\<close>}\<close>}, \<open>bu\<close>
+is indeed a string which refers to a meta-object belonging
+to the document class \<^typ>\<open>author\<close>, for example).
 The term-context in the \<open>value*\<close>-command and \<^emph>\<open>assert*\<close>-command is additionally expanded
 (\<^eg> replaced) by a term denoting the meta-object.
 This expansion happens \<^emph>\<open>before\<close> evaluation of the term, thus permitting
@@ -1201,7 +1202,7 @@ text\<open>
   when opening a monitor, when closing a monitor, or both
   by using the \<^ML>\<open>DOF_core.update_class_eager_invariant\<close>,
   \<^ML>\<open>DOF_core.update_class_lazy_invariant\<close>, or \<^ML>\<open>DOF_core.update_class_invariant\<close> commands
-  respectfully, to add the invariants to the theory context
+  respectively, to add the invariants to the theory context
   (See \<^technical>\<open>sec:low_level_inv\<close> for an example).
 \<close>
 

src/tests/TermAntiquotations.thy

@@ -104,15 +104,19 @@ text\<open>We can also reference an attribute of the instance.
 Here we reference the attribute r of the class F which has the type @{typ \<open>thm list\<close>}.\<close>
 term*\<open>r @{F \<open>xcv4\<close>}\<close>
 
-term \<open>@{A \<open>xcv2\<close>}\<close>
-
 text\<open>We declare a new text element. Note that the class name contains an underscore "_".\<close>
 text*[te::text_element]\<open>Lorem ipsum...\<close>
 
 text\<open>Unfortunately due to different lexical conventions for constant symbols and mixfix symbols
-     this term antiquotation has to be denoted like this: @{term\<open>@{text-element \<open>ee\<close>}\<close>}.
+     this term antiquotation has to be denoted like this: @{term_ \<open>@{text-element \<open>te\<close>}\<close>}.
      We need to substitute an hyphen "-" for the underscore "_".\<close>
 term*\<open>@{text-element \<open>te\<close>}\<close>
 
+text\<open>Terms containing term antiquotations can be checked and evaluated
+using \<^theory_text>\<open>term_\<close> and \<^theory_text>\<open>value_\<close> text antiquotations respectively:
+We can print the term @{term_ \<open>r @{F \<open>xcv4\<close>}\<close>} with \<open>@{term_ \<open>r @{F \<open>xcv4\<close>}\<close>}\<close>
+or get the value of the \<^const>\<open>F.r\<close> attribute of @{docitem \<open>xcv4\<close>} with \<open>@{value_ \<open>r @{F \<open>xcv4\<close>}\<close>}\<close>
+\<close>
+
 end