# HG changeset patch
# User wenzelm
# Date 1185717604 -7200
# Node ID f7483532537bbf38998214f37683c80b2da067bc
# Parent  0eacec17e8e756ab5027620101f1cb7e1e3c4276
added TOPLEVEL_ERROR (simplified version from output.ML);

diff -r 0eacec17e8e7 -r f7483532537b src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Jul 29 16:00:03 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sun Jul 29 16:00:04 2007 +0200
@@ -38,6 +38,7 @@
   val skip_proofs: bool ref
   exception TERMINATE
   exception RESTART
+  exception TOPLEVEL_ERROR
   val exn_message: exn -> string
   val program: (unit -> 'a) -> 'a
   type transition
@@ -237,6 +238,7 @@
 exception RESTART;
 exception EXCURSION_FAIL of exn * string;
 exception FAILURE of state * exn;
+exception TOPLEVEL_ERROR;
 
 
 (* print exceptions *)
@@ -254,7 +256,7 @@
 fun exn_msg _ TERMINATE = "Exit."
   | exn_msg _ RESTART = "Restart."
   | exn_msg _ Interrupt = "Interrupt."
-  | exn_msg _ Output.TOPLEVEL_ERROR = "Error."
+  | exn_msg _ TOPLEVEL_ERROR = "Error."
   | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
   | exn_msg _ (ERROR msg) = msg
   | exn_msg detailed (Exn.EXCEPTIONS (exns, "")) = cat_lines (map (exn_msg detailed) exns)
@@ -303,16 +305,20 @@
   let val y = ref x
   in raise_interrupt (fn () => y := f x) (); ! y end;
 
+fun toplevel_error f x = f x
+  handle exn => (Output.error_msg (exn_message exn); raise TOPLEVEL_ERROR);
+
 in
 
 fun controlled_execution f =
   f
   |> debugging
-  |> interruptible
-  |> setmp Output.do_toplevel_errors false;
+  |> interruptible;
 
 fun program f =
-  Output.ML_errors (fn () => debugging f () handle exn => error (exn_message exn)) ();
+ (f
+  |> debugging
+  |> toplevel_error) ();
 
 end;