# HG changeset patch
# User wenzelm
# Date 1697812841 -7200
# Node ID d4e9d6b7f48d5455841fa4d64a11ad3462825bdb
# Parent  577835250124c7c5239a752391a8c623d79b97af
clarified signature;

diff -r 577835250124 -r d4e9d6b7f48d src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Fri Oct 20 11:03:09 2023 +0200
+++ b/src/Pure/Isar/parse.ML	Fri Oct 20 16:40:41 2023 +0200
@@ -123,7 +123,6 @@
   val embedded_ml: ML_Lex.token Antiquote.antiquote list parser
   val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
   val read_embedded: Proof.context -> Keyword.keywords -> 'a parser -> Input.source -> 'a
-  val read_embedded_src: Proof.context -> Keyword.keywords -> 'a parser -> Token.src -> 'a
 end;
 
 structure Parse: PARSE =
@@ -533,8 +532,4 @@
     | NONE => error ("Bad input" ^ Position.here (Input.pos_of input)))
   end;
 
-fun read_embedded_src ctxt keywords parse src =
-  Token.read ctxt embedded_input src
-  |> read_embedded ctxt keywords parse;
-
 end;
diff -r 577835250124 -r d4e9d6b7f48d src/Pure/ML/ml_antiquotation.ML
--- a/src/Pure/ML/ml_antiquotation.ML	Fri Oct 20 11:03:09 2023 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML	Fri Oct 20 16:40:41 2023 +0200
@@ -70,10 +70,9 @@
 (* ML macros *)
 
 fun special_form binding parse =
-  ML_Context.add_antiquotation binding true
-    (fn _ => fn src => fn ctxt =>
+  ML_Context.add_antiquotation_embedded binding
+    (fn _ => fn input => fn ctxt =>
       let
-        val input = Token.read ctxt Parse.embedded_input src;
         val tokenize = ML_Lex.tokenize_no_range;
         val tokenize_range = ML_Lex.tokenize_range (Input.range_of input);
         val eq = tokenize " = ";
@@ -97,12 +96,10 @@
       in (decl', ctxt') end);
 
 fun conditional binding check =
-  ML_Context.add_antiquotation binding true
-    (fn _ => fn src => fn ctxt =>
-      let val s = Token.read ctxt Parse.embedded_input src in
-        if check ctxt then ML_Context.read_antiquotes s ctxt
-        else (K ([], []), ctxt)
-      end);
+  ML_Context.add_antiquotation_embedded binding
+    (fn _ => fn input => fn ctxt =>
+      if check ctxt then ML_Context.read_antiquotes input ctxt
+      else (K ([], []), ctxt));
 
 
 (* basic antiquotations *)
diff -r 577835250124 -r d4e9d6b7f48d src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Fri Oct 20 11:03:09 2023 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Fri Oct 20 16:40:41 2023 +0200
@@ -229,11 +229,11 @@
 fun ml_pair (x, y) = ml_parens (ml_commas [x, y]);
 
 fun type_antiquotation binding {function} =
-  ML_Context.add_antiquotation binding true
-    (fn range => fn src => fn ctxt =>
+  ML_Context.add_antiquotation_embedded binding
+    (fn range => fn input => fn ctxt =>
       let
-        val ((s, type_args), fn_body) = src
-          |> Parse.read_embedded_src ctxt keywords (parse_name_args -- parse_body function);
+        val ((s, type_args), fn_body) = input
+          |> Parse.read_embedded ctxt keywords (parse_name_args -- parse_body function);
         val pos = Input.pos_of s;
 
         val Type (c, Ts) =
@@ -264,11 +264,11 @@
       in (decl', ctxt2) end);
 
 fun const_antiquotation binding {pattern, function} =
-  ML_Context.add_antiquotation binding true
-    (fn range => fn src => fn ctxt =>
+  ML_Context.add_antiquotation_embedded binding
+    (fn range => fn input => fn ctxt =>
       let
-        val (((s, type_args), term_args), fn_body) = src
-          |> Parse.read_embedded_src ctxt keywords
+        val (((s, type_args), term_args), fn_body) = input
+          |> Parse.read_embedded ctxt keywords
               (parse_name_args -- parse_for_args -- parse_body function);
 
         val Const (c, T) =
@@ -400,13 +400,12 @@
 (* special form for option type *)
 
 val _ = Theory.setup
-  (ML_Context.add_antiquotation \<^binding>\<open>if_none\<close> true
-    (fn _ => fn src => fn ctxt =>
+  (ML_Context.add_antiquotation_embedded \<^binding>\<open>if_none\<close>
+    (fn _ => fn input => fn ctxt =>
       let
-        val s = Token.read ctxt Parse.embedded_input src;
         val tokenize = ML_Lex.tokenize_no_range;
 
-        val (decl, ctxt') = ML_Context.read_antiquotes s ctxt;
+        val (decl, ctxt') = ML_Context.read_antiquotes input ctxt;
         fun decl' ctxt'' =
           let
             val (ml_env, ml_body) = decl ctxt'';
diff -r 577835250124 -r d4e9d6b7f48d src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Fri Oct 20 11:03:09 2023 +0200
+++ b/src/Pure/ML/ml_context.ML	Fri Oct 20 16:40:41 2023 +0200
@@ -11,8 +11,9 @@
   val variant: string -> Proof.context -> string * Proof.context
   type decl = Proof.context -> ML_Lex.token list * ML_Lex.token list
   type decls = Proof.context -> (ML_Lex.token list * ML_Lex.token list) list
-  type antiquotation = Position.range -> Token.src -> Proof.context -> decl * Proof.context
-  val add_antiquotation: binding -> bool -> antiquotation -> theory -> theory
+  type 'a antiquotation = Position.range -> 'a -> Proof.context -> decl * Proof.context
+  val add_antiquotation: binding -> bool -> Token.src antiquotation -> theory -> theory
+  val add_antiquotation_embedded: binding -> Input.source antiquotation -> theory -> theory
   val print_antiquotations: bool -> Proof.context -> unit
   val expand_antiquotes: ML_Lex.token Antiquote.antiquote list ->
     Proof.context -> decl * Proof.context
@@ -62,12 +63,11 @@
 
 type decls = Proof.context -> (ML_Lex.token list * ML_Lex.token list) list;
 
-type antiquotation =
-  Position.range -> Token.src -> Proof.context -> decl * Proof.context;
+type 'a antiquotation = Position.range -> 'a -> Proof.context -> decl * Proof.context;
 
 structure Antiquotations = Theory_Data
 (
-  type T = (bool * antiquotation) Name_Space.table;
+  type T = (bool * Token.src antiquotation) Name_Space.table;
   val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
   fun merge data : T = Name_Space.merge_tables data;
 );
@@ -81,6 +81,11 @@
   thy |> Antiquotations.map
     (Name_Space.define (Context.Theory thy) true (name, (embedded, antiquotation)) #> #2);
 
+fun add_antiquotation_embedded name antiquotation =
+  add_antiquotation name true
+    (fn range => fn src => fn ctxt =>
+      antiquotation range (Token.read ctxt Parse.embedded_input src) ctxt);
+
 fun print_antiquotations verbose ctxt =
   Pretty.big_list "ML antiquotations:"
     (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_antiquotations ctxt)))
diff -r 577835250124 -r d4e9d6b7f48d src/Pure/ML/ml_instantiate.ML
--- a/src/Pure/ML/ml_instantiate.ML	Fri Oct 20 11:03:09 2023 +0200
+++ b/src/Pure/ML/ml_instantiate.ML	Fri Oct 20 16:40:41 2023 +0200
@@ -231,11 +231,11 @@
   (command_name "lemma" >> #2) -- parse_schematic -- ML_Thms.embedded_lemma >> prepare_lemma range;
 
 val _ = Theory.setup
-  (ML_Context.add_antiquotation \<^binding>\<open>instantiate\<close> true
-    (fn range => fn src => fn ctxt =>
+  (ML_Context.add_antiquotation_embedded \<^binding>\<open>instantiate\<close>
+    (fn range => fn input => fn ctxt =>
       let
-        val (insts, prepare_val) = src
-          |> Parse.read_embedded_src ctxt (make_keywords ctxt)
+        val (insts, prepare_val) = input
+          |> Parse.read_embedded ctxt (make_keywords ctxt)
               ((parse_insts --| Parse.$$$ "in") -- parse_body range);
 
         val (((ml_env, ml_body), decls), ctxt1) = ctxt