# HG changeset patch
# User wenzelm
# Date 1621790958 -7200
# Node ID 08db0a06e13108cf08f4f2b718739b192a6d8213
# Parent  c73c22c62d081be47368fdd4e8281e99aeab95e9
clarified treatment of type constructors;

diff -r c73c22c62d08 -r 08db0a06e131 src/Doc/Implementation/ML.thy
--- 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"} \\
diff -r c73c22c62d08 -r 08db0a06e131 src/Doc/Isar_Ref/Document_Preparation.thy
--- 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>.
 
diff -r c73c22c62d08 -r 08db0a06e131 src/Doc/Isar_Ref/Outer_Syntax.thy
--- 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>
 
diff -r c73c22c62d08 -r 08db0a06e131 src/Pure/Thy/document_antiquotations.ML
--- 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 =>