src/Pure/Isar/outer_syntax.ML
changeset 14091 ad6ba9c55190
parent 12943 1db24da0537b
child 14687 e089757b952a
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Jul 04 17:09:26 2003 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Jul 07 17:58:21 2003 +0200
     1.3 @@ -60,7 +60,8 @@
     1.4    val check_text: string * Position.T -> bool -> Toplevel.state -> unit
     1.5    val deps_thy: string -> bool -> Path.T -> string list * Path.T list
     1.6    val load_thy: string -> bool -> bool -> Path.T -> unit
     1.7 -  val isar: bool -> bool -> Toplevel.isar
     1.8 +  val isar: bool -> bool -> unit Toplevel.isar
     1.9 +  val isar_readstring: Position.T -> string -> (string list) Toplevel.isar
    1.10  end;
    1.11  
    1.12  structure OuterSyntax: OUTER_SYNTAX =
    1.13 @@ -257,6 +258,15 @@
    1.14    |> toplevel_source term true get_parser;
    1.15  
    1.16  
    1.17 +(* string source of transformers (for Proof General) *)
    1.18 +
    1.19 +fun isar_readstring pos str =
    1.20 +  Source.of_string str
    1.21 +  |> Symbol.source false
    1.22 +  |> T.source false get_lexicons pos
    1.23 +  |> toplevel_source false true get_parser;
    1.24 +
    1.25 +
    1.26  
    1.27  (** read theory **)
    1.28