# HG changeset patch
# User wenzelm
# Date 1450878018 -3600
# Node ID 35ec3757d3c16230744d81b0d9707331a9fffcc6
# Parent  e9812a95d108826d9498c6ef8805eb702682da8d
check and report source at most once, notably in body of "match" method;

diff -r e9812a95d108 -r 35ec3757d3c1 src/HOL/Eisbach/method_closure.ML
--- 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
diff -r e9812a95d108 -r 35ec3757d3c1 src/Pure/Isar/method.ML
--- 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 *)