--- 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 **)