# HG changeset patch
# User wenzelm
# Date 1206625279 -3600
# Node ID f1c79c00f1e475f601ae847f2cf847c9afb4c899
# Parent  8ddb2e7c5a1e993c2802270c025a843e0e3a0c9d
added process_file;

diff -r 8ddb2e7c5a1e -r f1c79c00f1e4 src/Pure/Isar/outer_syntax.ML
--- 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 =