A patch by david aspinall

--- a/src/Pure/Isar/outer_syntax.ML	Fri Jul 04 17:09:26 2003 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Jul 07 17:58:21 2003 +0200
@@ -60,7 +60,8 @@
   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
+  val isar: bool -> bool -> unit Toplevel.isar
+  val isar_readstring: Position.T -> string -> (string list) Toplevel.isar
 end;
 
 structure OuterSyntax: OUTER_SYNTAX =
@@ -257,6 +258,15 @@
   |> toplevel_source term true get_parser;
 
 
+(* string source of transformers (for Proof General) *)
+
+fun isar_readstring pos str =
+  Source.of_string str
+  |> Symbol.source false
+  |> T.source false get_lexicons pos
+  |> toplevel_source false true get_parser;
+
+
 
 (** read theory **)
 

--- a/src/Pure/Isar/toplevel.ML	Fri Jul 04 17:09:26 2003 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Jul 07 17:58:21 2003 +0200
@@ -67,8 +67,8 @@
   val get_state: unit -> state
   val exn: unit -> (exn * string) option
   val >> : transition -> bool
-  type isar
-  val loop: isar -> unit
+  type 'a isar
+  val loop: 'a isar -> unit
 end;
 
 structure Toplevel: TOPLEVEL =
@@ -471,10 +471,10 @@
 
 (* the Isar source of transitions *)
 
-type isar =
+type 'a isar =
   (transition, (transition option,
     (OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token,
-      Position.T * (Symbol.symbol, (string, unit) Source.source) Source.source)
+      Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source)
           Source.source) Source.source) Source.source) Source.source) Source.source) Source.source;