src/Pure/Isar/method.ML

   val finish_text: text option * bool -> text
   val print_methods: bool -> Proof.context -> unit
   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
   val local_setup: binding -> (Proof.context -> method) context_parser -> string ->
     local_theory -> local_theory

   #1 o Token.check_src ctxt (get_methods o Context.Proof);
 
 fun check_text ctxt (Source src) = Source (check_src ctxt src)
   | 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 *)
 
 fun method_syntax scan src ctxt : method =