# HG changeset patch
# User wenzelm
# Date 1695561285 -7200
# Node ID 37b49c592265d24f22f3aa7dc353f017961b0ef0
# Parent  ff7db9055002b7735b937820aaa85d0b39992f4a
clarified signature;

diff -r ff7db9055002 -r 37b49c592265 src/Pure/ML/ml_antiquotation.ML
--- a/src/Pure/ML/ml_antiquotation.ML	Sun Sep 24 15:07:40 2023 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML	Sun Sep 24 15:14:45 2023 +0200
@@ -75,7 +75,7 @@
         val tokenize = ML_Lex.tokenize_no_range;
         val tokenize_range = ML_Lex.tokenize_range (Input.range_of s);
 
-        val (decl, ctxt') = ML_Context.expand_antiquotes (ML_Lex.read_source s) ctxt;
+        val (decl, ctxt') = ML_Context.read_antiquotes s ctxt;
         fun decl' ctxt'' =
           let
             val (ml_env, ml_body) = decl ctxt'';
@@ -90,8 +90,7 @@
   ML_Context.add_antiquotation binding true
     (fn _ => fn src => fn ctxt =>
       let val (s, _) = Token.syntax (Scan.lift Parse.embedded_input) src ctxt in
-        if check ctxt then
-          ML_Context.expand_antiquotes (ML_Lex.read_source s) ctxt
+        if check ctxt then ML_Context.read_antiquotes s ctxt
         else (K ([], []), ctxt)
       end);
 
diff -r ff7db9055002 -r 37b49c592265 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Sun Sep 24 15:07:40 2023 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Sun Sep 24 15:14:45 2023 +0200
@@ -351,7 +351,7 @@
         val (s, _) = Token.syntax (Scan.lift Parse.embedded_input) src ctxt;
         val tokenize = ML_Lex.tokenize_no_range;
 
-        val (decl, ctxt') = ML_Context.expand_antiquotes (ML_Lex.read_source s) ctxt;
+        val (decl, ctxt') = ML_Context.read_antiquotes s ctxt;
         fun decl' ctxt'' =
           let
             val (ml_env, ml_body) = decl ctxt'';
diff -r ff7db9055002 -r 37b49c592265 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Sun Sep 24 15:07:40 2023 +0200
+++ b/src/Pure/ML/ml_context.ML	Sun Sep 24 15:14:45 2023 +0200
@@ -18,6 +18,7 @@
     Proof.context -> decl * Proof.context
   val expand_antiquotes_list: ML_Lex.token Antiquote.antiquote list list ->
     Proof.context -> decls * Proof.context
+  val read_antiquotes: Input.source -> Proof.context -> decl * Proof.context
   val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
   val eval_file: ML_Compiler.flags -> Path.T -> unit
   val eval_source: ML_Compiler.flags -> Input.source -> unit
@@ -129,6 +130,8 @@
 
 end;
 
+val read_antiquotes = expand_antiquotes o ML_Lex.read_source;
+
 
 (* evaluation *)