# HG changeset patch
# User wenzelm
# Date 1638705036 -3600
# Node ID 944d4d616ca0ed7955b161790a4e38d8e5fef346
# Parent  89c7f74b5ae118f978bb5b07d5ae2c7ba9735867
clarified corner cases of syntax;

diff -r 89c7f74b5ae1 -r 944d4d616ca0 src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Sun Dec 05 12:23:10 2021 +0100
+++ b/src/Doc/Implementation/Logic.thy	Sun Dec 05 12:50:36 2021 +0100
@@ -217,10 +217,10 @@
   \<^rail>\<open>
     @{syntax_def type_const}: @{syntax name} (@{syntax embedded_ml}*)
     ;
-    @{syntax_def type_const_fn}: @{syntax type_const} @'=>' @{syntax embedded}
+    @{syntax_def type_const_fn}: @{syntax type_const} @'=>' @{syntax embedded_ml}
     ;
-    @{syntax_def embedded_ml}: @{syntax embedded} |
-      @{syntax control_symbol} @{syntax embedded} | @'_'
+    @{syntax_def embedded_ml}:
+      @'_' | @{syntax embedded} | @{syntax control_symbol} @{syntax embedded}
   \<close>
 
   The text provided as @{syntax embedded_ml} is treated as regular Isabelle/ML
@@ -491,9 +491,10 @@
     @{syntax_def term_const}:
       @{syntax name} (@{syntax embedded_ml}*) (@{syntax for_args})?
     ;
-    @{syntax_def type_const_fn}: @{ syntax term_const} @'=>' @{syntax embedded}
+    @{syntax_def term_const_fn}:
+      @{ syntax term_const} @'=>' @{syntax embedded_ml}
     ;
-    @{syntax_def for_args}: @'for' (@{syntax embedded_ml}*)
+    @{syntax_def for_args}: @'for' (@{syntax embedded_ml}+)
   \<close>
 \<close>
 
diff -r 89c7f74b5ae1 -r 944d4d616ca0 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Sun Dec 05 12:23:10 2021 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML	Sun Dec 05 12:50:36 2021 +0100
@@ -205,14 +205,14 @@
 
 val keywords = Keyword.add_minor_keywords ["for", "=>"] Keyword.empty_keywords;
 
-val parse_name = Parse.input Parse.name;
+val parse_name_args =
+  Parse.input Parse.name -- Scan.repeat Parse.embedded_ml;
 
-val parse_args = Scan.repeat Parse.embedded_ml;
-val parse_for_args = Scan.optional (Parse.$$$ "for" |-- Parse.!!! parse_args) [];
+val parse_for_args =
+  Scan.optional (Parse.$$$ "for" |-- Parse.!!! (Scan.repeat1 Parse.embedded_ml)) [];
 
 fun parse_body b =
-  if b then Parse.$$$ "=>" |-- Parse.!!! Parse.embedded_input >> (ML_Lex.read_source #> single)
-  else Scan.succeed [];
+  if b then Parse.$$$ "=>" |-- Parse.!!! (Parse.embedded_ml >> single) else Scan.succeed [];
 
 fun is_dummy [Antiquote.Text tok] = ML_Lex.content_of tok = "_"
   | is_dummy _ = false;
@@ -233,7 +233,7 @@
     (fn range => fn src => fn ctxt =>
       let
         val ((s, type_args), fn_body) = src
-          |> Parse.read_embedded_src ctxt keywords (parse_name -- parse_args -- parse_body function);
+          |> Parse.read_embedded_src ctxt keywords (parse_name_args -- parse_body function);
         val pos = Input.pos_of s;
 
         val Type (c, Ts) =
@@ -269,7 +269,7 @@
       let
         val (((s, type_args), term_args), fn_body) = src
           |> Parse.read_embedded_src ctxt keywords
-              (parse_name -- parse_args -- parse_for_args -- parse_body function);
+              (parse_name_args -- parse_for_args -- parse_body function);
 
         val Const (c, T) =
           Proof_Context.read_const {proper = true, strict = true} ctxt