--- 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);
--- 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'';
--- 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 *)