added process_file;

--- a/src/Pure/Isar/outer_syntax.ML	Thu Mar 27 14:41:18 2008 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Thu Mar 27 14:41:19 2008 +0100
@@ -44,6 +44,7 @@
   val scan: string -> OuterLex.token list
   val read: OuterLex.token list -> (string * OuterLex.token list * Toplevel.transition) list
   val parse: Position.T -> string -> Toplevel.transition list
+  val process_file: Path.T -> theory -> theory
   val isar: bool -> unit Toplevel.isar
 end;
 
@@ -257,6 +258,17 @@
   |> Source.exhaust;
 
 
+(* process file *)
+
+fun process_file path thy =
+  let
+    val result = ref thy;
+    val trs = parse (Position.path path) (File.read path);
+    val init = Toplevel.init_theory (K thy) (fn thy' => result := thy') (K ());
+    val _ = Toplevel.excursion (init Toplevel.empty :: trs @ [Toplevel.exit Toplevel.empty]);
+  in ! result end;
+
+
 (* interactive source of toplevel transformers *)
 
 fun isar term =