--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Wed Oct 20 20:25:33 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Thu Oct 21 18:10:51 2021 +0200
@@ -41,7 +41,7 @@
val ctxt = Proof_Context.init_global thy
val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords thy)
- fun read_actions () = Token.read_embedded ctxt keywords
+ fun read_actions () = Parse.read_embedded ctxt keywords
(Parse.enum ";" (Parse.name -- Sledgehammer_Commands.parse_params))
(Input.string str)
fun split_name_label (name, args) labels =
--- a/src/Pure/Isar/method.ML Wed Oct 20 20:25:33 2021 +0200
+++ b/src/Pure/Isar/method.ML Thu Oct 21 18:10:51 2021 +0200
@@ -741,7 +741,7 @@
fun read_closure_input ctxt =
let val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords' ctxt)
- in Token.read_embedded ctxt keywords (Scan.many Token.not_eof) #> read_closure ctxt end;
+ in Parse.read_embedded ctxt keywords (Scan.many Token.not_eof) #> read_closure ctxt end;
val text_closure =
Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) =>
--- a/src/Pure/Isar/parse.ML Wed Oct 20 20:25:33 2021 +0200
+++ b/src/Pure/Isar/parse.ML Thu Oct 21 18:10:51 2021 +0200
@@ -121,6 +121,9 @@
val options: ((string * Position.T) * (string * Position.T)) list parser
val embedded_ml: ML_Lex.token Antiquote.antiquote list parser
val embedded_ml_underscore: 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 =
@@ -508,4 +511,35 @@
val embedded_ml_underscore =
input underscore >> ML_Lex.read_source || embedded_ml;
+
+(* read embedded source, e.g. for antiquotations *)
+
+fun read_antiq keywords scan (syms, pos) =
+ let
+ val toks = syms
+ |> Token.tokenize (Keyword.no_command_keywords keywords) {strict = true}
+ |> filter Token.is_proper;
+ in
+ (case Scan.read Token.stopper scan toks of
+ SOME res => res
+ | NONE => error ("Malformed antiquotation" ^ Position.here pos))
+ end;
+
+fun read_embedded ctxt keywords parse input =
+ let
+ val toks = input
+ |> Input.source_explode
+ |> Token.tokenize keywords {strict = true}
+ |> filter Token.is_proper;
+ val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks);
+ in
+ (case Scan.read Token.stopper parse toks of
+ SOME res => res
+ | NONE => error ("Bad input" ^ Position.here (Input.pos_of input)))
+ end;
+
+fun read_embedded_src ctxt keywords parse src =
+ Token.syntax (Scan.lift embedded_input) src ctxt
+ |> #1 |> read_embedded ctxt keywords parse;
+
end;
--- a/src/Pure/Isar/token.ML Wed Oct 20 20:25:33 2021 +0200
+++ b/src/Pure/Isar/token.ML Thu Oct 21 18:10:51 2021 +0200
@@ -104,8 +104,6 @@
val make_src: string * Position.T -> T list -> src
type 'a parser = T list -> 'a * T list
type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
- 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 syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
end;
@@ -766,33 +764,6 @@
type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list);
-(* embedded source, e.g. for antiquotations *)
-
-fun read_antiq keywords scan (syms, pos) =
- let
- val toks = syms
- |> tokenize (Keyword.no_command_keywords keywords) {strict = true}
- |> filter is_proper;
- in
- (case Scan.read stopper scan toks of
- SOME res => res
- | NONE => error ("Malformed antiquotation" ^ Position.here pos))
- end;
-
-fun read_embedded ctxt keywords parse input =
- let
- val toks = input
- |> Input.source_explode
- |> tokenize keywords {strict = true}
- |> filter is_proper;
- val _ = Context_Position.reports_text ctxt (maps (reports keywords) toks);
- in
- (case Scan.read stopper parse toks of
- SOME res => res
- | NONE => error ("Bad input" ^ Position.here (Input.pos_of input)))
- end;
-
-
(* wrapped syntax *)
fun syntax_generic scan src context =
--- a/src/Pure/ML/ml_antiquotations.ML Wed Oct 20 20:25:33 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Thu Oct 21 18:10:51 2021 +0200
@@ -221,10 +221,6 @@
(* type/term constructors *)
-fun read_embedded ctxt keywords parse src =
- Token.syntax (Scan.lift Parse.embedded_input) src ctxt
- |> #1 |> Token.read_embedded ctxt keywords parse;
-
local
val keywords = Keyword.add_minor_keywords ["for", "=>"] Keyword.empty_keywords;
@@ -257,7 +253,7 @@
(fn range => fn src => fn ctxt =>
let
val ((s, type_args), fn_body) = src
- |> read_embedded ctxt keywords (parse_name -- parse_args -- parse_body function);
+ |> Parse.read_embedded_src ctxt keywords (parse_name -- parse_args -- parse_body function);
val pos = Input.pos_of s;
val Type (c, Ts) =
@@ -292,7 +288,7 @@
(fn range => fn src => fn ctxt =>
let
val (((s, type_args), term_args), fn_body) = src
- |> read_embedded ctxt keywords
+ |> Parse.read_embedded_src ctxt keywords
(parse_name -- parse_args -- parse_for_args -- parse_body function);
val Const (c, T) =
--- a/src/Pure/ML/ml_context.ML Wed Oct 20 20:25:33 2021 +0200
+++ b/src/Pure/ML/ml_context.ML Thu Oct 21 18:10:51 2021 +0200
@@ -111,7 +111,7 @@
(Token.make_src name (if null body then [] else [Token.read_cartouche body]))
| Antiquote.Antiq {range, body, ...} =>
ctxt |> apply_antiquotation range
- (Token.read_antiq (Thy_Header.get_keywords' ctxt) antiq (body, #1 range)));
+ (Parse.read_antiq (Thy_Header.get_keywords' ctxt) antiq (body, #1 range)));
in
--- a/src/Pure/Thy/document_antiquotation.ML Wed Oct 20 20:25:33 2021 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML Thu Oct 21 18:10:51 2021 +0200
@@ -188,7 +188,7 @@
in
fun read_antiq ctxt ({range = (pos, _), body, ...}: Antiquote.antiq) =
- Token.read_antiq (Thy_Header.get_keywords' ctxt) parse_antiq (body, pos);
+ Parse.read_antiq (Thy_Header.get_keywords' ctxt) parse_antiq (body, pos);
fun evaluate eval_text ctxt antiq =
(case antiq of
--- a/src/Pure/Thy/document_marker.ML Wed Oct 20 20:25:33 2021 +0200
+++ b/src/Pure/Thy/document_marker.ML Thu Oct 21 18:10:51 2021 +0200
@@ -62,7 +62,7 @@
val body = Symbol_Pos.cartouche_content syms;
val markers =
Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body)
- |> Token.read_embedded ctxt keywords (Parse.list parse_marker);
+ |> Parse.read_embedded ctxt keywords (Parse.list parse_marker);
in
ctxt
|> Config.put config_command_name cmd_name