# HG changeset patch
# User wenzelm
# Date 1621717090 -7200
# Node ID ebaed09ce06e32ebd9fcbbefaefdd26fbb08047f
# Parent  35d8132633c65250e15c7ac080969500fc22db35
more uniform document antiquotations for ML: consolidate former setup for manuals;

diff -r 35d8132633c6 -r ebaed09ce06e src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Sat May 22 21:52:13 2021 +0200
+++ b/src/Doc/Implementation/Logic.thy	Sat May 22 22:58:10 2021 +0200
@@ -624,7 +624,7 @@
 
   \<^descr> \<^ML>\<open>Thm.apply\<close>, \<^ML>\<open>Thm.lambda\<close>, \<^ML>\<open>Thm.all\<close>, \<^ML>\<open>Drule.mk_implies\<close>
   etc.\ compose certified terms (or propositions) incrementally. This is
-  equivalent to \<^ML>\<open>Thm.cterm_of\<close> after unchecked \<^ML_op>\<open>$\<close>, \<^ML>\<open>lambda\<close>,
+  equivalent to \<^ML>\<open>Thm.cterm_of\<close> after unchecked \<^ML_infix>\<open>$\<close>, \<^ML>\<open>lambda\<close>,
   \<^ML>\<open>Logic.all\<close>, \<^ML>\<open>Logic.mk_implies\<close> etc., but there can be a big
   difference in performance when large existing entities are composed by a few
   extra constructions on top. There are separate operations to decompose
diff -r 35d8132633c6 -r ebaed09ce06e src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Sat May 22 21:52:13 2021 +0200
+++ b/src/Doc/Implementation/ML.thy	Sat May 22 22:58:10 2021 +0200
@@ -1608,7 +1608,7 @@
 
   The unwieldy name of \<^ML>\<open>Unsynchronized.ref\<close> for the constructor for
   references in Isabelle/ML emphasizes the inconveniences caused by
-  mutability. Existing operations \<^ML>\<open>!\<close> and \<^ML_op>\<open>:=\<close> are unchanged,
+  mutability. Existing operations \<^ML>\<open>!\<close> and \<^ML_infix>\<open>:=\<close> are unchanged,
   but should be used with special precautions, say in a strictly local
   situation that is guaranteed to be restricted to sequential evaluation ---
   now and in the future.
diff -r 35d8132633c6 -r ebaed09ce06e src/Doc/Implementation/Tactic.thy
--- a/src/Doc/Implementation/Tactic.thy	Sat May 22 21:52:13 2021 +0200
+++ b/src/Doc/Implementation/Tactic.thy	Sat May 22 22:58:10 2021 +0200
@@ -494,9 +494,9 @@
 text \<open>
   Sequential composition and alternative choices are the most basic ways to
   combine tactics, similarly to ``\<^verbatim>\<open>,\<close>'' and ``\<^verbatim>\<open>|\<close>'' in Isar method notation.
-  This corresponds to \<^ML_op>\<open>THEN\<close> and \<^ML_op>\<open>ORELSE\<close> in ML, but there
+  This corresponds to \<^ML_infix>\<open>THEN\<close> and \<^ML_infix>\<open>ORELSE\<close> in ML, but there
   are further possibilities for fine-tuning alternation of tactics such as
-  \<^ML_op>\<open>APPEND\<close>. Further details become visible in ML due to explicit
+  \<^ML_infix>\<open>APPEND\<close>. Further details become visible in ML due to explicit
   subgoal addressing.
 \<close>
 
@@ -515,32 +515,32 @@
   @{define_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\
   \end{mldecls}
 
-  \<^descr> \<open>tac\<^sub>1\<close>~\<^ML_op>\<open>THEN\<close>~\<open>tac\<^sub>2\<close> is the sequential composition of \<open>tac\<^sub>1\<close> and
+  \<^descr> \<open>tac\<^sub>1\<close>~\<^ML_infix>\<open>THEN\<close>~\<open>tac\<^sub>2\<close> is the sequential composition of \<open>tac\<^sub>1\<close> and
   \<open>tac\<^sub>2\<close>. Applied to a goal state, it returns all states reachable in two
   steps by applying \<open>tac\<^sub>1\<close> followed by \<open>tac\<^sub>2\<close>. First, it applies \<open>tac\<^sub>1\<close> to
   the goal state, getting a sequence of possible next states; then, it applies
   \<open>tac\<^sub>2\<close> to each of these and concatenates the results to produce again one
   flat sequence of states.
 
-  \<^descr> \<open>tac\<^sub>1\<close>~\<^ML_op>\<open>ORELSE\<close>~\<open>tac\<^sub>2\<close> makes a choice between \<open>tac\<^sub>1\<close> and
+  \<^descr> \<open>tac\<^sub>1\<close>~\<^ML_infix>\<open>ORELSE\<close>~\<open>tac\<^sub>2\<close> makes a choice between \<open>tac\<^sub>1\<close> and
   \<open>tac\<^sub>2\<close>. Applied to a state, it tries \<open>tac\<^sub>1\<close> and returns the result if
   non-empty; if \<open>tac\<^sub>1\<close> fails then it uses \<open>tac\<^sub>2\<close>. This is a deterministic
   choice: if \<open>tac\<^sub>1\<close> succeeds then \<open>tac\<^sub>2\<close> is excluded from the result.
 
-  \<^descr> \<open>tac\<^sub>1\<close>~\<^ML_op>\<open>APPEND\<close>~\<open>tac\<^sub>2\<close> concatenates the possible results of
-  \<open>tac\<^sub>1\<close> and \<open>tac\<^sub>2\<close>. Unlike \<^ML_op>\<open>ORELSE\<close> there is \<^emph>\<open>no commitment\<close> to
-  either tactic, so \<^ML_op>\<open>APPEND\<close> helps to avoid incompleteness during
+  \<^descr> \<open>tac\<^sub>1\<close>~\<^ML_infix>\<open>APPEND\<close>~\<open>tac\<^sub>2\<close> concatenates the possible results of
+  \<open>tac\<^sub>1\<close> and \<open>tac\<^sub>2\<close>. Unlike \<^ML_infix>\<open>ORELSE\<close> there is \<^emph>\<open>no commitment\<close> to
+  either tactic, so \<^ML_infix>\<open>APPEND\<close> helps to avoid incompleteness during
   search, at the cost of potential inefficiencies.
 
-  \<^descr> \<^ML>\<open>EVERY\<close>~\<open>[tac\<^sub>1, \<dots>, tac\<^sub>n]\<close> abbreviates \<open>tac\<^sub>1\<close>~\<^ML_op>\<open>THEN\<close>~\<open>\<dots>\<close>~\<^ML_op>\<open>THEN\<close>~\<open>tac\<^sub>n\<close>. Note that \<^ML>\<open>EVERY []\<close> is the same as
+  \<^descr> \<^ML>\<open>EVERY\<close>~\<open>[tac\<^sub>1, \<dots>, tac\<^sub>n]\<close> abbreviates \<open>tac\<^sub>1\<close>~\<^ML_infix>\<open>THEN\<close>~\<open>\<dots>\<close>~\<^ML_infix>\<open>THEN\<close>~\<open>tac\<^sub>n\<close>. Note that \<^ML>\<open>EVERY []\<close> is the same as
   \<^ML>\<open>all_tac\<close>: it always succeeds.
 
-  \<^descr> \<^ML>\<open>FIRST\<close>~\<open>[tac\<^sub>1, \<dots>, tac\<^sub>n]\<close> abbreviates \<open>tac\<^sub>1\<close>~\<^ML_op>\<open>ORELSE\<close>~\<open>\<dots>\<close>~\<^ML_op>\<open>ORELSE\<close>~\<open>tac\<^sub>n\<close>. Note that \<^ML>\<open>FIRST []\<close> is the
+  \<^descr> \<^ML>\<open>FIRST\<close>~\<open>[tac\<^sub>1, \<dots>, tac\<^sub>n]\<close> abbreviates \<open>tac\<^sub>1\<close>~\<^ML_infix>\<open>ORELSE\<close>~\<open>\<dots>\<close>~\<^ML_infix>\<open>ORELSE\<close>~\<open>tac\<^sub>n\<close>. Note that \<^ML>\<open>FIRST []\<close> is the
   same as \<^ML>\<open>no_tac\<close>: it always fails.
 
-  \<^descr> \<^ML_op>\<open>THEN'\<close> is the lifted version of \<^ML_op>\<open>THEN\<close>, for tactics
-  with explicit subgoal addressing. So \<open>(tac\<^sub>1\<close>~\<^ML_op>\<open>THEN'\<close>~\<open>tac\<^sub>2) i\<close> is
-  the same as \<open>(tac\<^sub>1 i\<close>~\<^ML_op>\<open>THEN\<close>~\<open>tac\<^sub>2 i)\<close>.
+  \<^descr> \<^ML_infix>\<open>THEN'\<close> is the lifted version of \<^ML_infix>\<open>THEN\<close>, for tactics
+  with explicit subgoal addressing. So \<open>(tac\<^sub>1\<close>~\<^ML_infix>\<open>THEN'\<close>~\<open>tac\<^sub>2) i\<close> is
+  the same as \<open>(tac\<^sub>1 i\<close>~\<^ML_infix>\<open>THEN\<close>~\<open>tac\<^sub>2 i)\<close>.
 
   The other primed tacticals work analogously.
 \<close>
@@ -567,7 +567,7 @@
   applies \<open>tac\<close> at most once.
 
   Note that for tactics with subgoal addressing, the combinator can be applied
-  via functional composition: \<^ML>\<open>TRY\<close>~\<^ML_op>\<open>o\<close>~\<open>tac\<close>. There is no need
+  via functional composition: \<^ML>\<open>TRY\<close>~\<^ML_infix>\<open>o\<close>~\<open>tac\<close>. There is no need
   for \<^verbatim>\<open>TRY'\<close>.
 
   \<^descr> \<^ML>\<open>REPEAT\<close>~\<open>tac\<close> applies \<open>tac\<close> to the goal state and, recursively, to
@@ -592,10 +592,10 @@
 text %mlex \<open>
   The basic tactics and tacticals considered above follow some algebraic laws:
 
-  \<^item> \<^ML>\<open>all_tac\<close> is the identity element of the tactical \<^ML_op>\<open>THEN\<close>.
+  \<^item> \<^ML>\<open>all_tac\<close> is the identity element of the tactical \<^ML_infix>\<open>THEN\<close>.
 
-  \<^item> \<^ML>\<open>no_tac\<close> is the identity element of \<^ML_op>\<open>ORELSE\<close> and \<^ML_op>\<open>APPEND\<close>. Also, it is a zero element for \<^ML_op>\<open>THEN\<close>, which means that
-  \<open>tac\<close>~\<^ML_op>\<open>THEN\<close>~\<^ML>\<open>no_tac\<close> is equivalent to \<^ML>\<open>no_tac\<close>.
+  \<^item> \<^ML>\<open>no_tac\<close> is the identity element of \<^ML_infix>\<open>ORELSE\<close> and \<^ML_infix>\<open>APPEND\<close>. Also, it is a zero element for \<^ML_infix>\<open>THEN\<close>, which means that
+  \<open>tac\<close>~\<^ML_infix>\<open>THEN\<close>~\<^ML>\<open>no_tac\<close> is equivalent to \<^ML>\<open>no_tac\<close>.
 
   \<^item> \<^ML>\<open>TRY\<close> and \<^ML>\<open>REPEAT\<close> can be expressed as (recursive) functions over
   more basic combinators (ignoring some internal implementation tricks):
@@ -607,7 +607,7 @@
 \<close>
 
 text \<open>
-  If \<open>tac\<close> can return multiple outcomes then so can \<^ML>\<open>REPEAT\<close>~\<open>tac\<close>. \<^ML>\<open>REPEAT\<close> uses \<^ML_op>\<open>ORELSE\<close> and not \<^ML_op>\<open>APPEND\<close>, it applies \<open>tac\<close>
+  If \<open>tac\<close> can return multiple outcomes then so can \<^ML>\<open>REPEAT\<close>~\<open>tac\<close>. \<^ML>\<open>REPEAT\<close> uses \<^ML_infix>\<open>ORELSE\<close> and not \<^ML_infix>\<open>APPEND\<close>, it applies \<open>tac\<close>
   as many times as possible in each outcome.
 
   \begin{warn}
@@ -650,11 +650,11 @@
   @{define_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\
   \end{mldecls}
 
-  \<^descr> \<^ML>\<open>ALLGOALS\<close>~\<open>tac\<close> is equivalent to \<open>tac n\<close>~\<^ML_op>\<open>THEN\<close>~\<open>\<dots>\<close>~\<^ML_op>\<open>THEN\<close>~\<open>tac 1\<close>. It applies the \<open>tac\<close> to all the subgoals, counting downwards.
+  \<^descr> \<^ML>\<open>ALLGOALS\<close>~\<open>tac\<close> is equivalent to \<open>tac n\<close>~\<^ML_infix>\<open>THEN\<close>~\<open>\<dots>\<close>~\<^ML_infix>\<open>THEN\<close>~\<open>tac 1\<close>. It applies the \<open>tac\<close> to all the subgoals, counting downwards.
 
-  \<^descr> \<^ML>\<open>SOMEGOAL\<close>~\<open>tac\<close> is equivalent to \<open>tac n\<close>~\<^ML_op>\<open>ORELSE\<close>~\<open>\<dots>\<close>~\<^ML_op>\<open>ORELSE\<close>~\<open>tac 1\<close>. It applies \<open>tac\<close> to one subgoal, counting downwards.
+  \<^descr> \<^ML>\<open>SOMEGOAL\<close>~\<open>tac\<close> is equivalent to \<open>tac n\<close>~\<^ML_infix>\<open>ORELSE\<close>~\<open>\<dots>\<close>~\<^ML_infix>\<open>ORELSE\<close>~\<open>tac 1\<close>. It applies \<open>tac\<close> to one subgoal, counting downwards.
 
-  \<^descr> \<^ML>\<open>FIRSTGOAL\<close>~\<open>tac\<close> is equivalent to \<open>tac 1\<close>~\<^ML_op>\<open>ORELSE\<close>~\<open>\<dots>\<close>~\<^ML_op>\<open>ORELSE\<close>~\<open>tac n\<close>. It applies \<open>tac\<close> to one subgoal, counting upwards.
+  \<^descr> \<^ML>\<open>FIRSTGOAL\<close>~\<open>tac\<close> is equivalent to \<open>tac 1\<close>~\<^ML_infix>\<open>ORELSE\<close>~\<open>\<dots>\<close>~\<^ML_infix>\<open>ORELSE\<close>~\<open>tac n\<close>. It applies \<open>tac\<close> to one subgoal, counting upwards.
 
   \<^descr> \<^ML>\<open>HEADGOAL\<close>~\<open>tac\<close> is equivalent to \<open>tac 1\<close>. It applies \<open>tac\<close>
   unconditionally to the first subgoal.
@@ -666,7 +666,7 @@
   upwards.
 
   \<^descr> \<^ML>\<open>RANGE\<close>~\<open>[tac\<^sub>1, \<dots>, tac\<^sub>k] i\<close> is equivalent to \<open>tac\<^sub>k (i + k -
-  1)\<close>~\<^ML_op>\<open>THEN\<close>~\<open>\<dots>\<close>~\<^ML_op>\<open>THEN\<close>~\<open>tac\<^sub>1 i\<close>. It applies the given list of
+  1)\<close>~\<^ML_infix>\<open>THEN\<close>~\<open>\<dots>\<close>~\<^ML_infix>\<open>THEN\<close>~\<open>tac\<^sub>1 i\<close>. It applies the given list of
   tactics to the corresponding range of subgoals, counting downwards.
 \<close>
 
@@ -714,7 +714,7 @@
   \<^descr> \<^ML>\<open>DEPTH_FIRST\<close>~\<open>sat tac\<close> returns the goal state if \<open>sat\<close> returns true.
   Otherwise it applies \<open>tac\<close>, then recursively searches from each element of
   the resulting sequence. The code uses a stack for efficiency, in effect
-  applying \<open>tac\<close>~\<^ML_op>\<open>THEN\<close>~\<^ML>\<open>DEPTH_FIRST\<close>~\<open>sat tac\<close> to the state.
+  applying \<open>tac\<close>~\<^ML_infix>\<open>THEN\<close>~\<^ML>\<open>DEPTH_FIRST\<close>~\<open>sat tac\<close> to the state.
 
   \<^descr> \<^ML>\<open>DEPTH_SOLVE\<close>\<open>tac\<close> uses \<^ML>\<open>DEPTH_FIRST\<close> to search for states having
   no subgoals.
diff -r 35d8132633c6 -r ebaed09ce06e src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Sat May 22 21:52:13 2021 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Sat May 22 22:58:10 2021 +0200
@@ -100,11 +100,22 @@
     @{antiquotation_def subgoals} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def prf} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def full_prf} & : & \<open>antiquotation\<close> \\
+    @{antiquotation_def ML_text} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def ML} & : & \<open>antiquotation\<close> \\
-    @{antiquotation_def ML_op} & : & \<open>antiquotation\<close> \\
+    @{antiquotation_def ML_def} & : & \<open>antiquotation\<close> \\
+    @{antiquotation_def ML_ref} & : & \<open>antiquotation\<close> \\
+    @{antiquotation_def ML_infix} & : & \<open>antiquotation\<close> \\
+    @{antiquotation_def ML_infix_def} & : & \<open>antiquotation\<close> \\
+    @{antiquotation_def ML_infix_ref} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def ML_type} & : & \<open>antiquotation\<close> \\
+    @{antiquotation_def ML_type_def} & : & \<open>antiquotation\<close> \\
+    @{antiquotation_def ML_type_ref} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def ML_structure} & : & \<open>antiquotation\<close> \\
+    @{antiquotation_def ML_structure_def} & : & \<open>antiquotation\<close> \\
+    @{antiquotation_def ML_structure_ref} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def ML_functor} & : & \<open>antiquotation\<close> \\
+    @{antiquotation_def ML_functor_def} & : & \<open>antiquotation\<close> \\
+    @{antiquotation_def ML_functor_ref} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def emph} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def bold} & : & \<open>antiquotation\<close> \\
     @{antiquotation_def verbatim} & : & \<open>antiquotation\<close> \\
@@ -192,8 +203,9 @@
       @@{antiquotation subgoals} options |
       @@{antiquotation prf} options @{syntax thms} |
       @@{antiquotation full_prf} options @{syntax thms} |
+      @@{antiquotation ML_text} options @{syntax text} |
       @@{antiquotation ML} options @{syntax text} |
-      @@{antiquotation ML_op} options @{syntax text} |
+      @@{antiquotation ML_infix} options @{syntax text} |
       @@{antiquotation ML_type} options @{syntax text} |
       @@{antiquotation ML_structure} options @{syntax text} |
       @@{antiquotation ML_functor} options @{syntax text} |
@@ -280,10 +292,16 @@
   \<^descr> \<open>@{full_prf a\<^sub>1 \<dots> a\<^sub>n}\<close> is like \<open>@{prf a\<^sub>1 \<dots> a\<^sub>n}\<close>, but prints the full
   proof terms, i.e.\ also displays information omitted in the compact proof
   term, which is denoted by ``\<open>_\<close>'' placeholders there.
-  
-  \<^descr> \<open>@{ML s}\<close>, \<open>@{ML_op s}\<close>, \<open>@{ML_type s}\<close>, \<open>@{ML_structure s}\<close>, and
+
+  \<^descr> \<open>@{ML_text s}\<close> prints ML text verbatim: only the token language is
+  checked.
+
+  \<^descr> \<open>@{ML s}\<close>, \<open>@{ML_infix s}\<close>, \<open>@{ML_type s}\<close>, \<open>@{ML_structure s}\<close>, and
   \<open>@{ML_functor s}\<close> check text \<open>s\<close> as ML value, infix operator, type,
-  structure, and functor respectively. The source is printed verbatim.
+  exception, structure, and functor respectively. The source is printed
+  verbatim. The variants \<open>@{ML_def s}\<close> and \<open>@{ML_ref s}\<close> etc. maintain the
+  document index: ``def'' means to make a bold entry, ``ref'' means to make a
+  regular entry.
 
   \<^descr> \<open>@{emph s}\<close> prints document source recursively, with {\LaTeX} markup
   \<^verbatim>\<open>\emph{\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>.
diff -r 35d8132633c6 -r ebaed09ce06e src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Sat May 22 21:52:13 2021 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Sat May 22 22:58:10 2021 +0200
@@ -153,7 +153,7 @@
 
   \<^descr> @{attribute THEN}~\<open>a\<close> composes rules by resolution; it resolves with the
   first premise of \<open>a\<close> (an alternative position may be also specified). See
-  also \<^ML_op>\<open>RS\<close> in @{cite "isabelle-implementation"}.
+  also \<^ML_infix>\<open>RS\<close> in @{cite "isabelle-implementation"}.
   
   \<^descr> @{attribute unfolded}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> and @{attribute folded}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close>
   expand and fold back again the given definitions throughout a rule.
diff -r 35d8132633c6 -r ebaed09ce06e src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Sat May 22 21:52:13 2021 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Sat May 22 22:58:10 2021 +0200
@@ -626,7 +626,7 @@
   Structural composition ``\<open>m\<^sub>1\<close>\<^verbatim>\<open>;\<close>~\<open>m\<^sub>2\<close>'' means that method \<open>m\<^sub>1\<close> is
   applied with restriction to the first subgoal, then \<open>m\<^sub>2\<close> is applied
   consecutively with restriction to each subgoal that has newly emerged due to
-  \<open>m\<^sub>1\<close>. This is analogous to the tactic combinator \<^ML_op>\<open>THEN_ALL_NEW\<close> in
+  \<open>m\<^sub>1\<close>. This is analogous to the tactic combinator \<^ML_infix>\<open>THEN_ALL_NEW\<close> in
   Isabelle/ML, see also @{cite "isabelle-implementation"}. For example, \<open>(rule
   r; blast)\<close> applies rule \<open>r\<close> and then solves all new subgoals by \<open>blast\<close>.
 
diff -r 35d8132633c6 -r ebaed09ce06e src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Sat May 22 21:52:13 2021 +0200
+++ b/src/Doc/antiquote_setup.ML	Sat May 22 22:58:10 2021 +0200
@@ -33,94 +33,6 @@
   | clean_name s = s |> translate (fn "_" => "-" | "\<hyphen>" => "-" | c => c);
 
 
-(* ML text *)
-
-local
-
-fun test_val (ml1, []) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read ");"
-  | test_val (ml1, ml2) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : " @ ml2 @ ML_Lex.read ");";
-
-fun test_op (ml1, ml2) = test_val (ML_Lex.read "op " @ ml1, ml2);
-
-fun test_type (ml1, []) = ML_Lex.read "val _ = NONE : (" @ ml1 @ ML_Lex.read ") option;"
-  | test_type (ml1, ml2) =
-      ML_Lex.read "val _ = [NONE : (" @ ml1 @ ML_Lex.read ") option, NONE : (" @
-      ml2 @ ML_Lex.read ") option];";
-
-fun text_exn (ml1, []) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : exn);"
-  | text_exn (ml1, ml2) =
-      ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : " @ ml2 @ ML_Lex.read " -> exn);";
-
-fun test_struct (ml, _) =
-  ML_Lex.read "functor XXX() = struct structure XX = " @ ml @ ML_Lex.read " end;";
-
-fun test_functor (Antiquote.Text tok :: _, _) =
-      ML_Lex.read "ML_Env.check_functor " @
-      ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok))
-  | test_functor _ = raise Fail "Bad ML functor specification";
-
-val is_name =
-  ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.Long_Ident);
-
-fun is_ml_identifier ants =
-  forall Antiquote.is_text ants andalso
-    (case filter is_name (map (Antiquote.the_text "") ants) of
-      toks as [_] => Symbol_Pos.is_identifier (Long_Name.base_name (ML_Lex.flatten toks))
-    | _ => false);
-
-val parse_ml = Args.text_input -- Scan.optional (Args.colon |-- Args.text_input) Input.empty;
-val parse_type = Args.text_input -- Scan.optional (Args.$$$ "=" |-- Args.text_input) Input.empty;
-val parse_exn = Args.text_input -- Scan.optional (Args.$$$ "of" |-- Args.text_input) Input.empty;
-val parse_struct = Args.text_input >> rpair Input.empty;
-
-fun antiquotation_ml parse test kind show_kind binding index =
-  Document_Output.antiquotation_raw binding (Scan.lift parse)
-    (fn ctxt => fn (source1, source2) =>
-      let
-        val (ml1, ml2) = apply2 ML_Lex.read_source (source1, source2);
-        val pos = Input.pos_of source1;
-        val _ =
-          ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (test (ml1, ml2))
-            handle ERROR msg => error (msg ^ Position.here pos);
-
-        val (txt1, txt2) = apply2 (#1 o Input.source_content) (source1, source2);
-        val sep = if kind = "type" then "=" else if kind = "exception" then "of" else ":";
-        val txt =
-          if txt2 = "" then txt1
-          else if sep = ":" andalso is_ml_identifier ml1 then txt1 ^ ": " ^ txt2
-          else txt1 ^ " " ^ sep ^ " " ^ txt2;
-
-        val main_text =
-          Document_Output.verbatim ctxt
-            (if kind = "" orelse not show_kind then txt else kind ^ " " ^ txt);
-
-        val index_text =
-          index |> Option.map (fn def =>
-            let
-              val ctxt' = Config.put Document_Antiquotation.thy_output_display false ctxt;
-              val kind' = if kind = "" then " (ML)" else " (ML " ^ kind ^ ")";
-              val txt' = Latex.block [Document_Output.verbatim ctxt' txt1, Latex.string kind'];
-              val like = Document_Antiquotation.approx_content ctxt source1;
-            in Latex.index_entry {items = [{text = txt', like = like}], def = def} end);
-      in Latex.block (the_list index_text @ [main_text]) end);
-
-fun antiquotation_ml' parse test kind binding =
-  antiquotation_ml parse test kind true binding (SOME true);
-
-in
-
-val _ =
-  Theory.setup
-   (antiquotation_ml' parse_ml test_val "" \<^binding>\<open>define_ML\<close> #>
-    antiquotation_ml' parse_ml test_op "infix" \<^binding>\<open>define_ML_infix\<close> #>
-    antiquotation_ml' parse_type test_type "type" \<^binding>\<open>define_ML_type\<close> #>
-    antiquotation_ml' parse_exn text_exn "exception" \<^binding>\<open>define_ML_exception\<close> #>
-    antiquotation_ml' parse_struct test_struct "structure" \<^binding>\<open>define_ML_structure\<close> #>
-    antiquotation_ml' parse_struct test_functor "functor" \<^binding>\<open>define_ML_functor\<close>);
-
-end;
-
-
 (* named theorems *)
 
 val _ =
diff -r 35d8132633c6 -r ebaed09ce06e src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Sat May 22 21:52:13 2021 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML	Sat May 22 22:58:10 2021 +0200
@@ -305,30 +305,97 @@
 
 local
 
-fun ml_text name ml =
-  Document_Output.antiquotation_verbatim_embedded name (Scan.lift Args.text_input)
-    (fn ctxt => fn text =>
-      let val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of text) (ml text)
-      in #1 (Input.source_content text) end);
+fun test_val (ml1, []) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read ");"
+  | test_val (ml1, ml2) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : " @ ml2 @ ML_Lex.read ");";
+
+fun test_op (ml1, ml2) = test_val (ML_Lex.read "op " @ ml1, ml2);
+
+fun test_type (ml1, []) = ML_Lex.read "val _ = NONE : (" @ ml1 @ ML_Lex.read ") option;"
+  | test_type (ml1, ml2) =
+      ML_Lex.read "val _ = [NONE : (" @ ml1 @ ML_Lex.read ") option, NONE : (" @
+      ml2 @ ML_Lex.read ") option];";
+
+fun test_exn (ml1, []) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : exn);"
+  | test_exn (ml1, ml2) =
+      ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : " @ ml2 @ ML_Lex.read " -> exn);";
+
+fun test_struct (ml, _) =
+  ML_Lex.read "functor XXX() = struct structure XX = " @ ml @ ML_Lex.read " end;";
+
+fun test_functor (Antiquote.Text tok :: _, _) =
+      ML_Lex.read "ML_Env.check_functor " @
+      ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok))
+  | test_functor _ = raise Fail "Bad ML functor specification";
 
-fun ml_enclose bg en source =
-  ML_Lex.read bg @ ML_Lex.read_source source @ ML_Lex.read en;
+val is_name =
+  ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.Long_Ident);
+
+fun is_ml_identifier ants =
+  forall Antiquote.is_text ants andalso
+    (case filter is_name (map (Antiquote.the_text "") ants) of
+      toks as [_] => Symbol_Pos.is_identifier (Long_Name.base_name (ML_Lex.flatten toks))
+    | _ => false);
+
+val parse_ml0 = Args.text_input >> rpair Input.empty;
+val parse_ml = Args.text_input -- Scan.optional (Args.colon |-- Args.text_input) Input.empty;
+val parse_type = Args.text_input -- Scan.optional (Args.$$$ "=" |-- Args.text_input) Input.empty;
+val parse_exn = Args.text_input -- Scan.optional (Args.$$$ "of" |-- Args.text_input) Input.empty;
+
+fun antiquotation_ml parse test kind show_kind binding index =
+  Document_Output.antiquotation_raw binding (Scan.lift parse)
+    (fn ctxt => fn (source1, source2) =>
+      let
+        val (ml1, ml2) = apply2 ML_Lex.read_source (source1, source2);
+        val pos = Input.pos_of source1;
+        val _ =
+          ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (test (ml1, ml2))
+            handle ERROR msg => error (msg ^ Position.here pos);
 
-val _ = Theory.setup
- (ml_text \<^binding>\<open>ML\<close> (ml_enclose "fn _ => (" ");") #>
-  ml_text \<^binding>\<open>ML_op\<close> (ml_enclose "fn _ => (op " ");") #>
-  ml_text \<^binding>\<open>ML_type\<close> (ml_enclose "val _ = NONE : (" ") option;") #>
-  ml_text \<^binding>\<open>ML_structure\<close>
-    (ml_enclose "functor XXX() = struct structure XX = " " end;") #>
+        val (txt1, txt2) = apply2 (#1 o Input.source_content) (source1, source2);
+        val sep = if kind = "type" then "=" else if kind = "exception" then "of" else ":";
+        val txt =
+          if txt2 = "" then txt1
+          else if sep = ":" andalso is_ml_identifier ml1 then txt1 ^ ": " ^ txt2
+          else txt1 ^ " " ^ sep ^ " " ^ txt2;
+
+        val main_text =
+          Document_Output.verbatim ctxt
+            (if kind = "" orelse not show_kind then txt else kind ^ " " ^ txt);
+
+        val index_text =
+          index |> Option.map (fn def =>
+            let
+              val ctxt' = Config.put Document_Antiquotation.thy_output_display false ctxt;
+              val kind' = if kind = "" then " (ML)" else " (ML " ^ kind ^ ")";
+              val txt' = Latex.block [Document_Output.verbatim ctxt' txt1, Latex.string kind'];
+              val like = Document_Antiquotation.approx_content ctxt source1;
+            in Latex.index_entry {items = [{text = txt', like = like}], def = def} end);
+      in Latex.block (the_list index_text @ [main_text]) end);
 
-  ml_text \<^binding>\<open>ML_functor\<close>   (* FIXME formal treatment of functor name (!?) *)
-    (fn source =>
-      ML_Lex.read ("ML_Env.check_functor " ^
-        ML_Syntax.print_string (#1 (Input.source_content source)))) #>
+fun antiquotation_ml0 test kind =
+  antiquotation_ml parse_ml0 test kind false;
+
+fun antiquotation_ml1 parse test kind binding =
+  antiquotation_ml parse test kind true binding (SOME true);
+
+in
 
-  ml_text \<^binding>\<open>ML_text\<close> (K []));
+val _ =
+  Theory.setup
+   (Latex.index_variants (antiquotation_ml0 test_val "") \<^binding>\<open>ML\<close> #>
+    Latex.index_variants (antiquotation_ml0 test_op "infix") \<^binding>\<open>ML_infix\<close> #>
+    Latex.index_variants (antiquotation_ml0 test_type "type") \<^binding>\<open>ML_type\<close> #>
+    Latex.index_variants (antiquotation_ml0 test_struct "structure") \<^binding>\<open>ML_structure\<close> #>
+    Latex.index_variants (antiquotation_ml0 test_functor "functor") \<^binding>\<open>ML_functor\<close> #>
+    antiquotation_ml0 (K []) "text" \<^binding>\<open>ML_text\<close> NONE #>
+    antiquotation_ml1 parse_ml test_val "" \<^binding>\<open>define_ML\<close> #>
+    antiquotation_ml1 parse_ml test_op "infix" \<^binding>\<open>define_ML_infix\<close> #>
+    antiquotation_ml1 parse_type test_type "type" \<^binding>\<open>define_ML_type\<close> #>
+    antiquotation_ml1 parse_exn test_exn "exception" \<^binding>\<open>define_ML_exception\<close> #>
+    antiquotation_ml1 parse_ml0 test_struct "structure" \<^binding>\<open>define_ML_structure\<close> #>
+    antiquotation_ml1 parse_ml0 test_functor "functor" \<^binding>\<open>define_ML_functor\<close>);
 
-in end;
+end;
 
 
 (* URLs *)