# HG changeset patch
# User wenzelm
# Date 911383160 -3600
# Node ID 5a8c731b15328b90619bbcc9619f2d7312120d8c
# Parent  85d62ecb950d763ad986902fe78bde879be0ef33
load;

diff -r 85d62ecb950d -r 5a8c731b1532 src/Pure/Isar/outer_syntax.ML
--- 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 () =