clarified signature: more detailed token positions for antiquotations;

--- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 08 20:52:19 2021 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri Apr 09 21:07:11 2021 +0200
@@ -115,7 +115,7 @@
 fun oracle (name, range) source =
   ML_Context.expression (Input.pos_of source)
     (ML_Lex.read "val " @
-     ML_Lex.read_set_range range name @
+     ML_Lex.read_range range name @
      ML_Lex.read
       (" = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (" ^
         ML_Syntax.make_binding (name, #1 range) ^ ", ") @

--- a/src/Pure/ML/ml_antiquotation.ML	Thu Apr 08 20:52:19 2021 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML	Fri Apr 09 21:07:11 2021 +0200
@@ -6,11 +6,13 @@
 
 signature ML_ANTIQUOTATION =
 sig
+  val value_decl: string -> string -> Proof.context ->
+    (Proof.context -> string * string) * Proof.context
   val declaration: binding -> 'a context_parser ->
-    (Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
+    (Token.src -> 'a -> Proof.context -> (Proof.context -> string * string) * Proof.context) ->
     theory -> theory
   val declaration_embedded: binding -> 'a context_parser ->
-    (Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
+    (Token.src -> 'a -> Proof.context -> (Proof.context -> string * string) * Proof.context) ->
     theory -> theory
   val inline: binding -> string context_parser -> theory -> theory
   val inline_embedded: binding -> string context_parser -> theory -> theory
@@ -23,19 +25,29 @@
 
 (* define antiquotations *)
 
+fun value_decl a s ctxt =
+  let
+    val (b, ctxt') = ML_Context.variant a ctxt;
+    val env = "val " ^ b ^ " = " ^ s ^ ";\n";
+    val body = ML_Context.struct_name ctxt ^ "." ^ b;
+    fun decl (_: Proof.context) = (env, body);
+  in (decl, ctxt') end;
+
 local
 
 fun gen_declaration name embedded scan body =
   ML_Context.add_antiquotation name embedded
-    (fn src => fn orig_ctxt =>
-      let val (x, _) = Token.syntax scan src orig_ctxt
-      in body src x orig_ctxt end);
+    (fn range => fn src => fn orig_ctxt =>
+      let
+        val (x, _) = Token.syntax scan src orig_ctxt;
+        val (decl, ctxt') = body src x orig_ctxt;
+      in (decl #> apply2 (ML_Lex.tokenize_range range), ctxt') end);
 
 fun gen_inline name embedded scan =
   gen_declaration name embedded scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
 
 fun gen_value name embedded scan =
-  gen_declaration name embedded scan (fn _ => ML_Context.value_decl (Binding.name_of name));
+  gen_declaration name embedded scan (fn _ => value_decl (Binding.name_of name));
 
 in
 
@@ -56,7 +68,7 @@
 val _ = Theory.setup
  (declaration (Binding.make ("here", \<^here>)) (Scan.succeed ())
     (fn src => fn () =>
-      ML_Context.value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #>
+      value_decl "position" (ML_Syntax.print_position (#2 (Token.name_of_src src)))) #>
 
   inline (Binding.make ("make_string", \<^here>)) (Args.context >> K ML_Pretty.make_string_fn) #>
 

--- a/src/Pure/ML/ml_context.ML	Thu Apr 08 20:52:19 2021 +0200
+++ b/src/Pure/ML/ml_context.ML	Fri Apr 09 21:07:11 2021 +0200
@@ -9,10 +9,9 @@
   val check_antiquotation: Proof.context -> xstring * Position.T -> string
   val struct_name: Proof.context -> string
   val variant: string -> Proof.context -> string * Proof.context
-  type decl = Proof.context -> string * string
-  val value_decl: string -> string -> Proof.context -> decl * Proof.context
-  val add_antiquotation: binding -> bool -> (Token.src -> Proof.context -> decl * Proof.context) ->
-    theory -> theory
+  type decl = Proof.context -> ML_Lex.token list * ML_Lex.token list
+  type antiquotation = Position.range -> Token.src -> Proof.context -> decl * Proof.context
+  val add_antiquotation: binding -> bool -> antiquotation -> theory -> theory
   val print_antiquotations: bool -> Proof.context -> unit
   val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
   val eval_file: ML_Compiler.flags -> Path.T -> unit
@@ -50,24 +49,17 @@
   in (b, ctxt') end;
 
 
-(* decl *)
-
-type decl = Proof.context -> string * string;  (*final context -> ML env, ML body*)
+(* theory data *)
 
-fun value_decl a s ctxt =
-  let
-    val (b, ctxt') = variant a ctxt;
-    val env = "val " ^ b ^ " = " ^ s ^ ";\n";
-    val body = struct_name ctxt ^ "." ^ b;
-    fun decl (_: Proof.context) = (env, body);
-  in (decl, ctxt') end;
+type decl =
+  Proof.context -> ML_Lex.token list * ML_Lex.token list;  (*final context -> ML env, ML body*)
 
-
-(* theory data *)
+type antiquotation =
+  Position.range -> Token.src -> Proof.context -> decl * Proof.context;
 
 structure Antiquotations = Theory_Data
 (
-  type T = (bool * (Token.src -> Proof.context -> decl * Proof.context)) Name_Space.table;
+  type T = (bool * antiquotation) Name_Space.table;
   val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
   val extend = I;
   fun merge data : T = Name_Space.merge_tables data;
@@ -78,23 +70,24 @@
 fun check_antiquotation ctxt =
   #1 o Name_Space.check (Context.Proof ctxt) (get_antiquotations ctxt);
 
-fun add_antiquotation name embedded scan thy = thy
-  |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, (embedded, scan)) #> snd);
+fun add_antiquotation name embedded antiquotation thy =
+  thy |> Antiquotations.map
+    (Name_Space.define (Context.Theory thy) true (name, (embedded, antiquotation)) #> #2);
 
 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)))
   |> Pretty.writeln;
 
-fun apply_antiquotation pos src ctxt =
+fun apply_antiquotation range src ctxt =
   let
-    val (src', (embedded, scan)) = Token.check_src ctxt get_antiquotations src;
+    val (src', (embedded, antiquotation)) = Token.check_src ctxt get_antiquotations src;
     val _ =
       if Options.default_bool "update_control_cartouches" then
         Context_Position.reports_text ctxt
-          (Antiquote.update_reports embedded pos (map Token.content_of src'))
+          (Antiquote.update_reports embedded (#1 range) (map Token.content_of src'))
       else ();
-  in scan src' ctxt end;
+  in antiquotation range src' ctxt end;
 
 
 (* parsing and evaluation *)
@@ -126,18 +119,12 @@
       then (([], map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
       else
         let
-          fun tokenize range = apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range));
-
-          fun expand_src range src ctxt =
-            let val (decl, ctxt') = apply_antiquotation (#1 range) src ctxt;
-            in (decl #> tokenize range, ctxt') end;
-
           fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
             | expand (Antiquote.Control {name, range, body}) ctxt =
-                expand_src range
+                apply_antiquotation range
                   (Token.make_src name (if null body then [] else [Token.read_cartouche body])) ctxt
             | expand (Antiquote.Antiq {range, body, ...}) ctxt =
-                expand_src range
+                apply_antiquotation range
                   (Token.read_antiq (Thy_Header.get_keywords' ctxt) antiq (body, #1 range)) ctxt;
 
           val ctxt =

--- a/src/Pure/ML/ml_lex.ML	Thu Apr 08 20:52:19 2021 +0200
+++ b/src/Pure/ML/ml_lex.ML	Fri Apr 09 21:07:11 2021 +0200
@@ -27,9 +27,10 @@
     (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
       Source.source) Source.source
   val tokenize: string -> token list
+  val tokenize_range: Position.range -> string -> token list
   val read_text: Symbol_Pos.text * Position.T -> token Antiquote.antiquote list
   val read: Symbol_Pos.text -> token Antiquote.antiquote list
-  val read_set_range: Position.range -> Symbol_Pos.text -> token Antiquote.antiquote list
+  val read_range: Position.range -> Symbol_Pos.text -> token Antiquote.antiquote list
   val read_source': {language: bool -> Markup.T, opaque_warning: bool, symbols: bool} ->
     token Antiquote.antiquote Symbol_Pos.scanner -> Input.source -> token Antiquote.antiquote list
   val read_source: Input.source -> token Antiquote.antiquote list
@@ -357,11 +358,12 @@
   |> Source.source Symbol_Pos.stopper (Scan.recover (Scan.bulk (!!! "bad input" scan_sml)) recover);
 
 val tokenize = Symbol.explode #> Source.of_list #> source #> Source.exhaust;
+fun tokenize_range range = tokenize #> map (set_range range);
 
 val read_text = reader {opaque_warning = true} scan_ml_antiq o Symbol_Pos.explode;
 fun read text = read_text (text, Position.none);
 
-fun read_set_range range =
+fun read_range range =
   read #> map (fn Antiquote.Text tok => Antiquote.Text (set_range range tok) | antiq => antiq);
 
 fun read_source' {language, symbols, opaque_warning} scan source =

--- a/src/Pure/ML/ml_thms.ML	Thu Apr 08 20:52:19 2021 +0200
+++ b/src/Pure/ML/ml_thms.ML	Fri Apr 09 21:07:11 2021 +0200
@@ -45,7 +45,7 @@
       let val i = serial () in
         ctxt
         |> put_attributes (i, srcs)
-        |> ML_Context.value_decl "attributes"
+        |> ML_Antiquotation.value_decl "attributes"
             ("ML_Thms.the_attributes ML_context " ^ string_of_int i)
       end));