--- a/src/HOL/Eisbach/method_closure.ML Tue Dec 22 21:58:27 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML Wed Dec 23 14:40:18 2015 +0100
@@ -65,16 +65,12 @@
(* read method text *)
fun read ctxt src =
- let
- val parser =
- Parse.!!! (Method.parser 0 --| Scan.ahead Parse.eof)
- >> apfst (Method.check_text ctxt);
- in
- (case Scan.read Token.stopper parser src of
- SOME (text, range) => (Method.report (text, range); text)
- | NONE =>
- error ("Failed to parse method" ^ Position.here (Position.set_range (Token.range_of src))))
- end;
+ (case Scan.read Token.stopper (Parse.!!! (Method.parser 0 --| Scan.ahead Parse.eof)) src of
+ SOME (text, range) =>
+ if Method.checked_text text then text
+ else (Method.report (text, range); Method.check_text ctxt text)
+ | NONE =>
+ error ("Failed to parse method" ^ Position.here (Position.set_range (Token.range_of src))));
fun read_closure ctxt src0 =
let
--- a/src/Pure/Isar/method.ML Tue Dec 22 21:58:27 2015 +0100
+++ b/src/Pure/Isar/method.ML Wed Dec 23 14:40:18 2015 +0100
@@ -73,6 +73,7 @@
val check_name: Proof.context -> xstring * Position.T -> string
val check_src: Proof.context -> Token.src -> Token.src
val check_text: Proof.context -> text -> text
+ val checked_text: text -> bool
val method_syntax: (Proof.context -> method) context_parser ->
Token.src -> Proof.context -> method
val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
@@ -439,6 +440,10 @@
| check_text _ (Basic m) = Basic m
| check_text ctxt (Combinator (x, y, body)) = Combinator (x, y, map (check_text ctxt) body);
+fun checked_text (Source src) = Token.checked_src src
+ | checked_text (Basic _) = true
+ | checked_text (Combinator (_, _, body)) = forall checked_text body;
+
(* method setup *)