# 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;