src/Pure/Isar/outer_syntax.ML
changeset 26431 f1c79c00f1e4
parent 26415 1b624d6e9163
child 26600 f11515535c83
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Mar 27 14:41:18 2008 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Mar 27 14:41:19 2008 +0100
     1.3 @@ -44,6 +44,7 @@
     1.4    val scan: string -> OuterLex.token list
     1.5    val read: OuterLex.token list -> (string * OuterLex.token list * Toplevel.transition) list
     1.6    val parse: Position.T -> string -> Toplevel.transition list
     1.7 +  val process_file: Path.T -> theory -> theory
     1.8    val isar: bool -> unit Toplevel.isar
     1.9  end;
    1.10  
    1.11 @@ -257,6 +258,17 @@
    1.12    |> Source.exhaust;
    1.13  
    1.14  
    1.15 +(* process file *)
    1.16 +
    1.17 +fun process_file path thy =
    1.18 +  let
    1.19 +    val result = ref thy;
    1.20 +    val trs = parse (Position.path path) (File.read path);
    1.21 +    val init = Toplevel.init_theory (K thy) (fn thy' => result := thy') (K ());
    1.22 +    val _ = Toplevel.excursion (init Toplevel.empty :: trs @ [Toplevel.exit Toplevel.empty]);
    1.23 +  in ! result end;
    1.24 +
    1.25 +
    1.26  (* interactive source of toplevel transformers *)
    1.27  
    1.28  fun isar term =