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