added check_text;
authorwenzelm
Mon Feb 25 20:51:48 2002 +0100 (2002-02-25)
changeset 129431db24da0537b
parent 12942 48fbe245879e
child 12944 fa6a3ddec27f
added check_text;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Feb 25 20:51:27 2002 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Feb 25 20:51:48 2002 +0100
     1.3 @@ -57,6 +57,7 @@
     1.4    val print_commands: Toplevel.transition -> Toplevel.transition
     1.5    val add_keywords: string list -> unit
     1.6    val add_parsers: parser list -> unit
     1.7 +  val check_text: string * Position.T -> bool -> Toplevel.state -> unit
     1.8    val deps_thy: string -> bool -> Path.T -> string list * Path.T list
     1.9    val load_thy: string -> bool -> bool -> Path.T -> unit
    1.10    val isar: bool -> bool -> Toplevel.isar
    1.11 @@ -259,6 +260,12 @@
    1.12  
    1.13  (** read theory **)
    1.14  
    1.15 +(* check_text *)
    1.16 +
    1.17 +fun check_text s true state = (IsarOutput.eval_antiquote (#1 (get_lexicons ())) state s; ())
    1.18 +  | check_text _ false _ = ();
    1.19 +
    1.20 +
    1.21  (* deps_thy *)
    1.22  
    1.23  fun deps_thy name ml path =