--- a/src/Pure/Isar/outer_syntax.ML Wed Nov 18 10:56:53 1998 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Wed Nov 18 10:59:20 1998 +0100
@@ -10,6 +10,7 @@
val main: unit -> unit
val loop: unit -> unit
val help: unit -> unit
+ val load: string -> unit
end;
signature OUTER_SYNTAX =
@@ -168,6 +169,8 @@
(** the read-eval-print loop **)
+(* main loop *)
+
fun loop () = (Context.reset_context (); Toplevel.loop isar);
fun main () =
@@ -177,6 +180,12 @@
loop ());
+(* load *)
+
+fun load name = Toplevel.excursion (read_file (name ^ ".thy"))
+ handle exn => error (Toplevel.exn_message exn);
+
+
(* help *)
fun help () =