--- a/src/Pure/Isar/method.ML Wed Jan 24 20:08:33 2018 +0100
+++ b/src/Pure/Isar/method.ML Wed Jan 24 20:47:36 2018 +0100
@@ -777,9 +777,9 @@
in (text, src2) end;
fun read_closure_input ctxt =
- Input.source_explode #>
- Token.read_no_commands (Thy_Header.get_keywords' ctxt) (Scan.one Token.not_eof) #>
- read_closure ctxt;
+ Input.source_explode
+ #> Token.read_body (Thy_Header.get_keywords' ctxt) (Scan.one Token.not_eof)
+ #> read_closure ctxt;
val text_closure =
Args.context -- Scan.lift (Parse.token Parse.text) >> (fn (ctxt, tok) =>
--- a/src/Pure/Isar/token.ML Wed Jan 24 20:08:33 2018 +0100
+++ b/src/Pure/Isar/token.ML Wed Jan 24 20:47:36 2018 +0100
@@ -93,7 +93,7 @@
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_no_commands: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a list
+ val read_body: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a list
val read_antiq: Keyword.keywords -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a
val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
@@ -707,22 +707,21 @@
type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list);
-(* read antiquotation source *)
+(* read body -- e.g. antiquotation source *)
-fun read_no_commands keywords scan syms =
- Source.of_list syms
- |> make_source (Keyword.no_command_keywords keywords) {strict = true}
- |> Source.filter is_proper
- |> Source.source stopper (Scan.error (Scan.bulk scan))
- |> Source.exhaust;
+fun read_body keywords scan =
+ tokenize (Keyword.no_command_keywords keywords) {strict = true}
+ #> filter is_proper
+ #> Source.of_list
+ #> Source.source stopper (Scan.error (Scan.bulk scan))
+ #> Source.exhaust;
fun read_antiq keywords scan (syms, pos) =
- let
- fun err msg =
- cat_error msg ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^
- "@{" ^ Symbol_Pos.content syms ^ "}");
- val res = read_no_commands keywords scan syms handle ERROR msg => err msg;
- in (case res of [x] => x | _ => err "") end;
+ (case read_body keywords scan syms of
+ [x] => x
+ | _ =>
+ error ("Malformed antiquotation" ^ Position.here pos ^ ":\n" ^
+ "@{" ^ Symbol_Pos.content syms ^ "}"));
(* wrapped syntax *)