added Isar.toplevel;
authorwenzelm
Sat Jan 14 17:14:17 2006 +0100 (2006-01-14)
changeset 1868438d72231b41d
parent 18683 a8f9c192f6d1
child 18685 725660906cb3
added Isar.toplevel;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Jan 14 17:14:16 2006 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Jan 14 17:14:17 2006 +0100
     1.3 @@ -15,6 +15,7 @@
     1.4        val loop: unit -> unit
     1.5        val sync_main: unit -> unit
     1.6        val sync_loop: unit -> unit
     1.7 +      val toplevel: (unit -> 'a) -> 'a
     1.8      end;
     1.9  end;
    1.10  
    1.11 @@ -271,7 +272,7 @@
    1.12      else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr]
    1.13    end;
    1.14  
    1.15 -fun run_thy name path =
    1.16 +fun run_thy name path = Output.toplevel_errors (fn () =>
    1.17    let
    1.18      val text = Source.of_list (Library.untabify (explode (File.read path)));
    1.19      val _ = Present.init_theory name;
    1.20 @@ -287,7 +288,7 @@
    1.21      IsarOutput.present_thy (#1 (get_lexicons ())) command_tags is_markup trs toks
    1.22      |> Buffer.content
    1.23      |> Present.theory_output name
    1.24 -  end;
    1.25 +  end) ();
    1.26  
    1.27  in
    1.28  
    1.29 @@ -327,6 +328,7 @@
    1.30    fun loop () = gen_loop false false;
    1.31    fun sync_main () = gen_main true true;
    1.32    fun sync_loop () = gen_loop true true;
    1.33 +  val toplevel = Toplevel.program;
    1.34  end;
    1.35  
    1.36