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  

     2.1 --- a/src/Pure/Isar/toplevel.ML	Fri Jul 04 17:09:26 2003 +0200
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Jul 07 17:58:21 2003 +0200
     2.3 @@ -67,8 +67,8 @@
     2.4    val get_state: unit -> state
     2.5    val exn: unit -> (exn * string) option
     2.6    val >> : transition -> bool
     2.7 -  type isar
     2.8 -  val loop: isar -> unit
     2.9 +  type 'a isar
    2.10 +  val loop: 'a isar -> unit
    2.11  end;
    2.12  
    2.13  structure Toplevel: TOPLEVEL =
    2.14 @@ -471,10 +471,10 @@
    2.15  
    2.16  (* the Isar source of transitions *)
    2.17  
    2.18 -type isar =
    2.19 +type 'a isar =
    2.20    (transition, (transition option,
    2.21      (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
    2.22 -      Position.T * (Symbol.symbol, (string, unit) Source.source) Source.source)
    2.23 +      Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source)
    2.24            Source.source) Source.source) Source.source) Source.source) Source.source) Source.source;
    2.25  
    2.26