more uniform document antiquotations for ML: consolidate former setup for manuals;
--- 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
--- 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.
--- 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.
--- 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>.
--- 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.
--- 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>.
--- 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 _ =
--- 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 *)