# HG changeset patch
# User wenzelm
# Date 1014666708 -3600
# Node ID 1db24da0537bac9bb0dc3a0617efdb9ecc35cb49
# Parent  48fbe245879e90a573c7137dae3c8a80b593cceb
added check_text;

diff -r 48fbe245879e -r 1db24da0537b src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Feb 25 20:51:27 2002 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Feb 25 20:51:48 2002 +0100
@@ -57,6 +57,7 @@
   val print_commands: Toplevel.transition -> Toplevel.transition
   val add_keywords: string list -> unit
   val add_parsers: parser list -> unit
+  val check_text: string * Position.T -> bool -> Toplevel.state -> unit
   val deps_thy: string -> bool -> Path.T -> string list * Path.T list
   val load_thy: string -> bool -> bool -> Path.T -> unit
   val isar: bool -> bool -> Toplevel.isar
@@ -259,6 +260,12 @@
 
 (** read theory **)
 
+(* check_text *)
+
+fun check_text s true state = (IsarOutput.eval_antiquote (#1 (get_lexicons ())) state s; ())
+  | check_text _ false _ = ();
+
+
 (* deps_thy *)
 
 fun deps_thy name ml path =