--- a/src/Doc/Implementation/ML.thy Sun May 23 18:04:35 2021 +0200
+++ b/src/Doc/Implementation/ML.thy Sun May 23 19:29:18 2021 +0200
@@ -1593,7 +1593,7 @@
text %mlref \<open>
\begin{mldecls}
- @{define_ML_type "'a Unsynchronized.ref"} \\
+ @{define_ML_type 'a "Unsynchronized.ref"} \\
@{define_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\
@{define_ML "!": "'a Unsynchronized.ref -> 'a"} \\
@{define_ML_infix ":=" : "'a Unsynchronized.ref * 'a -> unit"} \\
@@ -1790,7 +1790,7 @@
text %mlref \<open>
\begin{mldecls}
- @{define_ML_type "'a Synchronized.var"} \\
+ @{define_ML_type 'a "Synchronized.var"} \\
@{define_ML Synchronized.var: "string -> 'a -> 'a Synchronized.var"} \\
@{define_ML Synchronized.guarded_access: "'a Synchronized.var ->
('a -> ('b * 'a) option) -> 'b"} \\
@@ -1890,7 +1890,7 @@
text %mlref \<open>
\begin{mldecls}
- @{define_ML_type "'a Exn.result"} \\
+ @{define_ML_type 'a "Exn.result"} \\
@{define_ML Exn.capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
@{define_ML Exn.interruptible_capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
@{define_ML Exn.release: "'a Exn.result -> 'a"} \\
@@ -2009,7 +2009,7 @@
text %mlref \<open>
\begin{mldecls}
- @{define_ML_type "'a lazy"} \\
+ @{define_ML_type 'a "lazy"} \\
@{define_ML Lazy.lazy: "(unit -> 'a) -> 'a lazy"} \\
@{define_ML Lazy.value: "'a -> 'a lazy"} \\
@{define_ML Lazy.force: "'a lazy -> 'a"} \\
@@ -2090,7 +2090,7 @@
text %mlref \<open>
\begin{mldecls}
- @{define_ML_type "'a future"} \\
+ @{define_ML_type 'a "future"} \\
@{define_ML Future.fork: "(unit -> 'a) -> 'a future"} \\
@{define_ML Future.forks: "Future.params -> (unit -> 'a) list -> 'a future list"} \\
@{define_ML Future.join: "'a future -> 'a"} \\
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Sun May 23 18:04:35 2021 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Sun May 23 19:29:18 2021 +0200
@@ -206,7 +206,7 @@
@@{antiquotation ML_text} options @{syntax text} |
@@{antiquotation ML} options @{syntax text} |
@@{antiquotation ML_infix} options @{syntax text} |
- @@{antiquotation ML_type} options @{syntax text} |
+ @@{antiquotation ML_type} options @{syntax typeargs} @{syntax text} |
@@{antiquotation ML_structure} options @{syntax text} |
@@{antiquotation ML_functor} options @{syntax text} |
@@{antiquotation emph} options @{syntax text} |
@@ -303,6 +303,12 @@
document index: ``def'' means to make a bold entry, ``ref'' means to make a
regular entry.
+ There are two forms for type constructors, with or without separate type
+ arguments: this impacts only the index entry. For example, \<open>@{ML_type_ref
+ \<open>'a list\<close>}\<close> makes an entry literally for ``\<open>'a list\<close>'' (sorted under the
+ letter ``a''), but \<open>@{ML_type_ref 'a \<open>list\<close>}\<close> makes an entry for the
+ constructor name ``\<open>list\<close>''.
+
\<^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/Outer_Syntax.thy Sun May 23 18:04:35 2021 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Sun May 23 19:29:18 2021 +0200
@@ -343,12 +343,16 @@
no infixes.
\<^rail>\<open>
- @{syntax_def typespec}:
- (() | @{syntax type_ident} | '(' ( @{syntax type_ident} + ',' ) ')') @{syntax name}
+ @{syntax_def typeargs}:
+ (() | @{syntax type_ident} | '(' ( @{syntax type_ident} + ',' ) ')')
;
- @{syntax_def typespec_sorts}:
+ @{syntax_def typeargs_sorts}:
(() | (@{syntax type_ident} ('::' @{syntax sort})?) |
- '(' ( (@{syntax type_ident} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name}
+ '(' ( (@{syntax type_ident} ('::' @{syntax sort})?) + ',' ) ')')
+ ;
+ @{syntax_def typespec}: @{syntax typeargs} @{syntax name}
+ ;
+ @{syntax_def typespec_sorts}: @{syntax typeargs_sorts} @{syntax name}
\<close>
\<close>
--- a/src/Pure/Thy/document_antiquotations.ML Sun May 23 18:04:35 2021 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML Sun May 23 19:29:18 2021 +0200
@@ -327,10 +327,17 @@
ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok))
| test_functor _ = raise Fail "Bad ML functor specification";
-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;
+val parse_ml0 = Args.text_input >> (fn source => ("", (source, Input.empty)));
+
+val parse_ml =
+ Args.text_input -- Scan.optional (Args.colon |-- Args.text_input) Input.empty >> pair "";
+
+val parse_exn =
+ Args.text_input -- Scan.optional (Args.$$$ "of" |-- Args.text_input) Input.empty >> pair "";
+
+val parse_type =
+ (Parse.type_args >> (fn [] => "" | [a] => a ^ " " | bs => enclose "(" ") " (commas bs))) --
+ (Args.text_input -- Scan.optional (Args.$$$ "=" |-- Args.text_input) Input.empty);
fun eval ctxt pos ml =
ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos ml
@@ -351,16 +358,18 @@
fun antiquotation_ml parse test kind show_kind binding index =
Document_Output.antiquotation_raw binding (Scan.lift parse)
- (fn ctxt => fn sources =>
+ (fn ctxt => fn (txt0, sources) =>
let
- val _ = apply2 ML_Lex.read_source sources |> test |> eval ctxt (Input.pos_of (#1 sources));
+ val (ml1, ml2) = apply2 ML_Lex.read_source sources;
+ val ml0 = ML_Lex.read_source (Input.string txt0);
+ val _ = test (ml0 @ ml1, ml2) |> eval ctxt (Input.pos_of (#1 sources));
val sep = if kind = "type" then "=" else if kind = "exception" then "of" else ":";
val (txt, idx) = make_text sep sources;
val main_text =
Document_Output.verbatim ctxt
- (if kind = "" orelse not show_kind then txt else kind ^ " " ^ txt);
+ ((if kind = "" orelse not show_kind then "" else kind ^ " ") ^ txt0 ^ txt);
val index_text =
index |> Option.map (fn def =>