--- a/src/Doc/Implementation/ML.thy Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Doc/Implementation/ML.thy Thu Mar 03 15:23:02 2016 +0100
@@ -1154,7 +1154,7 @@
@{index_ML_exception ERROR: string} \\
@{index_ML_exception Fail: string} \\
@{index_ML Exn.is_interrupt: "exn -> bool"} \\
- @{index_ML reraise: "exn -> 'a"} \\
+ @{index_ML Exn.reraise: "exn -> 'a"} \\
@{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\
\end{mldecls}
@@ -1176,7 +1176,7 @@
concrete exception constructors in user code. Handled interrupts need to be
re-raised promptly!
- \<^descr> @{ML reraise}~\<open>exn\<close> raises exception \<open>exn\<close> while preserving its implicit
+ \<^descr> @{ML Exn.reraise}~\<open>exn\<close> raises exception \<open>exn\<close> while preserving its implicit
position information (if possible, depending on the ML platform).
\<^descr> @{ML Runtime.exn_trace}~@{ML_text "(fn () =>"}~\<open>e\<close>@{ML_text ")"} evaluates
--- a/src/HOL/Matrix_LP/Cplex_tools.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/HOL/Matrix_LP/Cplex_tools.ML Thu Mar 03 15:23:02 2016 +0100
@@ -1158,7 +1158,7 @@
result
end
handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
- | exn => if Exn.is_interrupt exn then reraise exn else raise (Execute answer)
+ | exn => if Exn.is_interrupt exn then Exn.reraise exn else raise (Execute answer)
end
fun solve_cplex prog =
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Thu Mar 03 15:23:02 2016 +0100
@@ -71,11 +71,11 @@
fun catch tag f id (st as {log, ...}: run_args) = (f id st; ())
handle exn =>
- if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; ())
+ if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; ())
fun catch_result tag d f id (st as {log, ...}: run_args) = f id st
handle exn =>
- if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; d)
+ if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; d)
fun register (init, run, done) thy =
let val id = length (Actions.get thy) + 1
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Mar 03 14:03:06 2016 +0100
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Thu Mar 03 15:23:02 2016 +0100
@@ -171,7 +171,7 @@
end
handle TimeLimit.TimeOut => "TIMEOUT"
| NOT_SUPPORTED _ => "UNSUP"
- | exn => if Exn.is_interrupt exn then reraise exn else "UNKNOWN"
+ | exn => if Exn.is_interrupt exn then Exn.reraise exn else "UNKNOWN"
fun check_theory thy =
let
--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy Thu Mar 03 14:03:06 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy Thu Mar 03 15:23:02 2016 +0100
@@ -129,7 +129,7 @@
val t1 = (parse_timed file |> fst)
val t2 = (interpret_timed timeout file thy |> fst)
handle exn => (*FIXME*)
- if Exn.is_interrupt exn then reraise exn
+ if Exn.is_interrupt exn then Exn.reraise exn
else
(warning (" test: file " ^ Path.print file ^
" raised exception: " ^ Runtime.exn_message exn);
--- a/src/HOL/TPTP/TPTP_Test.thy Thu Mar 03 14:03:06 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Test.thy Thu Mar 03 15:23:02 2016 +0100
@@ -60,7 +60,7 @@
(*otherwise report exceptions as warnings*)
handle exn =>
if Exn.is_interrupt exn then
- reraise exn
+ Exn.reraise exn
else
(report ctxt (msg ^ " test: file " ^ Path.print file_name ^
" raised exception: " ^ Runtime.exn_message exn);
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Thu Mar 03 15:23:02 2016 +0100
@@ -778,7 +778,7 @@
Old_Datatype_Aux.check_nonempty descr
handle (exn as Old_Datatype_Aux.Datatype_Empty s) =>
if #strict config then error ("Nonemptiness check failed for datatype " ^ quote s)
- else reraise exn;
+ else Exn.reraise exn;
val _ =
Old_Datatype_Aux.message config
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Mar 03 15:23:02 2016 +0100
@@ -192,7 +192,7 @@
handle
ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
| exn =>
- if Exn.is_interrupt exn then reraise exn
+ if Exn.is_interrupt exn then Exn.reraise exn
else (unknownN, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n"))
val _ =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Mar 03 15:23:02 2016 +0100
@@ -573,7 +573,7 @@
(trace_msg ctxt (fn () => "Unknown fact " ^ quote name ^ " when " ^ when); def)
| exn =>
if Exn.is_interrupt exn then
- reraise exn
+ Exn.reraise exn
else
(trace_msg ctxt (fn () => "Internal error when " ^ when ^ ":\n" ^ Runtime.exn_message exn);
def)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Thu Mar 03 15:23:02 2016 +0100
@@ -123,7 +123,7 @@
SMT_Solver.smt_filter ctxt goal facts i slice_timeout
handle exn =>
if Exn.is_interrupt exn orelse debug then
- reraise exn
+ Exn.reraise exn
else
{outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)),
fact_ids = NONE, atp_proof = K []}
--- a/src/Pure/Concurrent/bash.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/Concurrent/bash.ML Thu Mar 03 15:23:02 2016 +0100
@@ -54,7 +54,7 @@
Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
in Synchronized.change result (K res) end
handle exn =>
- (Synchronized.change result (fn Wait => Signal | res => res); reraise exn)));
+ (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
fun read_pid 0 = NONE
| read_pid count =
@@ -95,7 +95,7 @@
val pid = read_pid 1;
val _ = cleanup ();
in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
- handle exn => (terminate (read_pid 10); cleanup (); reraise exn)
+ handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
end);
end;
--- a/src/Pure/Concurrent/bash_windows.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/Concurrent/bash_windows.ML Thu Mar 03 15:23:02 2016 +0100
@@ -48,7 +48,7 @@
val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
in Synchronized.change result (K res) end
handle exn =>
- (Synchronized.change result (fn Wait => Signal | res => res); reraise exn)));
+ (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
fun read_pid 0 = NONE
| read_pid count =
@@ -93,7 +93,7 @@
val pid = read_pid 1;
val _ = cleanup ();
in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
- handle exn => (terminate (read_pid 10); cleanup (); reraise exn)
+ handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
end);
end;
--- a/src/Pure/Concurrent/future.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/Concurrent/future.ML Thu Mar 03 15:23:02 2016 +0100
@@ -348,7 +348,7 @@
(Multithreading.tracing 1 (fn () => "SCHEDULER: Interrupt");
List.app cancel_later (cancel_all ());
signal work_available; true)
- else reraise exn;
+ else Exn.reraise exn;
fun scheduler_loop () =
(while
@@ -409,8 +409,8 @@
val _ = Single_Assignment.assign result res
handle exn as Fail _ =>
(case Single_Assignment.peek result of
- SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn)
- | _ => reraise exn);
+ SOME (Exn.Exn e) => Exn.reraise (if Exn.is_interrupt e then e else exn)
+ | _ => Exn.reraise exn);
val ok =
(case the (Single_Assignment.peek result) of
Exn.Exn exn =>
@@ -600,7 +600,7 @@
| exn =>
if Exn.is_interrupt exn
then raise Fail "Concurrent attempt to fulfill promise"
- else reraise exn;
+ else Exn.reraise exn;
fun job () =
Multithreading.with_attributes Multithreading.no_interrupts
(fn _ => Exn.release (Exn.capture assign () before abort ()));
--- a/src/Pure/Concurrent/par_exn.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/Concurrent/par_exn.ML Thu Mar 03 15:23:02 2016 +0100
@@ -73,7 +73,7 @@
fun release_first results =
(case get_first plain_exn results of
NONE => release_all results
- | SOME exn => reraise exn);
+ | SOME exn => Exn.reraise exn);
end;
--- a/src/Pure/Concurrent/par_list.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/Concurrent/par_list.ML Thu Mar 03 15:23:02 2016 +0100
@@ -46,7 +46,7 @@
val results =
restore_attributes Future.join_results futures
handle exn =>
- (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
+ (if Exn.is_interrupt exn then Future.cancel_group group else (); Exn.reraise exn);
in results end) ();
fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
--- a/src/Pure/Concurrent/single_assignment.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/Concurrent/single_assignment.ML Thu Mar 03 15:23:02 2016 +0100
@@ -39,7 +39,7 @@
NONE =>
(case Multithreading.sync_wait NONE NONE cond lock of
Exn.Res _ => wait ()
- | Exn.Exn exn => reraise exn)
+ | Exn.Exn exn => Exn.reraise exn)
| SOME x => x);
in wait () end);
--- a/src/Pure/Concurrent/standard_thread.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/Concurrent/standard_thread.ML Thu Mar 03 15:23:02 2016 +0100
@@ -54,9 +54,9 @@
fun fork (params: params) body =
Thread.fork (fn () =>
- print_exception_trace General.exnMessage tracing (fn () =>
+ Exn.trace General.exnMessage tracing (fn () =>
(set_name (#name params); body ())
- handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
+ handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn),
attributes params);
--- a/src/Pure/Concurrent/synchronized.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/Concurrent/synchronized.ML Thu Mar 03 15:23:02 2016 +0100
@@ -49,7 +49,7 @@
(case Multithreading.sync_wait NONE (time_limit x) cond lock of
Exn.Res true => try_change ()
| Exn.Res false => NONE
- | Exn.Exn exn => reraise exn)
+ | Exn.Exn exn => Exn.reraise exn)
| SOME (y, x') =>
uninterruptible (fn _ => fn () =>
(var := x'; ConditionVar.broadcast cond; SOME y)) ())
--- a/src/Pure/General/basics.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/General/basics.ML Thu Mar 03 15:23:02 2016 +0100
@@ -102,7 +102,7 @@
(* partiality *)
fun try f x = SOME (f x)
- handle exn => if Exn.is_interrupt exn then reraise exn else NONE;
+ handle exn => if Exn.is_interrupt exn then Exn.reraise exn else NONE;
fun can f x = is_some (try f x);
--- a/src/Pure/Isar/runtime.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/Isar/runtime.ML Thu Mar 03 15:23:02 2016 +0100
@@ -141,8 +141,8 @@
val exn_error_message = Output.error_message o exn_message;
val exn_system_message = Output.system_message o exn_message;
-fun exn_trace e = print_exception_trace exn_message tracing e;
-fun exn_trace_system e = print_exception_trace exn_message Output.system_message e;
+fun exn_trace e = Exn.trace exn_message tracing e;
+fun exn_trace_system e = Exn.trace exn_message Output.system_message e;
(* exception debugger *)
@@ -189,7 +189,7 @@
fun toplevel_error output_exn f x = f x
handle exn =>
- if Exn.is_interrupt exn then reraise exn
+ if Exn.is_interrupt exn then Exn.reraise exn
else
let
val opt_ctxt =
--- a/src/Pure/Isar/toplevel.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/Isar/toplevel.ML Thu Mar 03 15:23:02 2016 +0100
@@ -594,7 +594,7 @@
(case transition int tr st of
(st', NONE) => st'
| (_, SOME (exn, info)) =>
- if Exn.is_interrupt exn then reraise exn
+ if Exn.is_interrupt exn then Exn.reraise exn
else raise Runtime.EXCURSION_FAIL (exn, info));
val command = command_exception false;
--- a/src/Pure/ML/ml_compiler.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML Thu Mar 03 15:23:02 2016 +0100
@@ -268,7 +268,7 @@
(while not (List.null (! input_buffer)) do
PolyML.compiler (get, parameters) ())
handle exn =>
- if Exn.is_interrupt exn then reraise exn
+ if Exn.is_interrupt exn then Exn.reraise exn
else
let
val exn_msg =
--- a/src/Pure/PIDE/command.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/PIDE/command.ML Thu Mar 03 15:23:02 2016 +0100
@@ -195,7 +195,7 @@
Outer_Syntax.side_comments span |> maps (fn cmt =>
(Thy_Output.output_text st' {markdown = false} (Token.input_of cmt); [])
handle exn =>
- if Exn.is_interrupt exn then reraise exn
+ if Exn.is_interrupt exn then Exn.reraise exn
else Runtime.exn_messages_ids exn)) ();
fun report tr m =
@@ -277,7 +277,7 @@
fun print_error tr opt_context e =
(Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
handle exn =>
- if Exn.is_interrupt exn then reraise exn
+ if Exn.is_interrupt exn then Exn.reraise exn
else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process;
@@ -312,7 +312,7 @@
fun bad_print name args exn =
make_print name args {delay = NONE, pri = 0, persistent = false,
- strict = false, print_fn = fn _ => fn _ => reraise exn};
+ strict = false, print_fn = fn _ => fn _ => Exn.reraise exn};
fun new_print name args get_pr =
let
--- a/src/Pure/PIDE/document.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/PIDE/document.ML Thu Mar 03 15:23:02 2016 +0100
@@ -486,7 +486,7 @@
else NONE
| NONE => NONE)) node ()
else ())
- handle exn => (Output.system_message (Runtime.exn_message exn); reraise exn);
+ handle exn => (Output.system_message (Runtime.exn_message exn); Exn.reraise exn);
val future =
(singleton o Future.forks)
{name = "theory:" ^ name,
--- a/src/Pure/PIDE/protocol.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/PIDE/protocol.ML Thu Mar 03 15:23:02 2016 +0100
@@ -120,7 +120,7 @@
Isabelle_Process.protocol_command "Document.dialog_result"
(fn [serial, result] =>
Active.dialog_result (Markup.parse_int serial) result
- handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn);
+ handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn);
val _ =
Isabelle_Process.protocol_command "ML_Heap.share_common_data"
--- a/src/Pure/RAW/ROOT_polyml.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML Thu Mar 03 15:23:02 2016 +0100
@@ -15,15 +15,7 @@
(* exceptions *)
-fun reraise exn =
- (case PolyML.exceptionLocation exn of
- NONE => raise exn
- | SOME location => PolyML.raiseWithLocation (exn, location));
-
-exception Interrupt = SML90.Interrupt;
-
use "RAW/exn.ML";
-use "RAW/exn_trace.ML";
(* multithreading *)
@@ -83,16 +75,10 @@
(* ML compiler *)
use "RAW/secure.ML";
-
-structure ML_Name_Space =
-struct
- open ML_Name_Space;
- val display_val = ML_Pretty.from_polyml o displayVal;
-end;
-
use "RAW/ml_compiler0.ML";
PolyML.Compiler.reportUnreferencedIds := true;
+PolyML.Compiler.reportExhaustiveHandlers := true;
PolyML.Compiler.printInAlphabeticalOrder := false;
PolyML.Compiler.maxInlineSize := 80;
PolyML.Compiler.prompt1 := "ML> ";
--- a/src/Pure/RAW/exn.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/RAW/exn.ML Thu Mar 03 15:23:02 2016 +0100
@@ -14,6 +14,7 @@
signature EXN =
sig
include BASIC_EXN
+ val reraise: exn -> 'a
datatype 'a result = Res of 'a | Exn of exn
val get_res: 'a result -> 'a option
val get_exn: 'a result -> exn option
@@ -31,11 +32,20 @@
val return_code: exn -> int -> int
val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
exception EXCEPTIONS of exn list
+ val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
end;
structure Exn: EXN =
struct
+(* reraise *)
+
+fun reraise exn =
+ (case PolyML.exceptionLocation exn of
+ NONE => raise exn
+ | SOME location => PolyML.raiseWithLocation (exn, location));
+
+
(* user errors *)
exception ERROR of string;
@@ -75,7 +85,7 @@
(* interrupts *)
-exception Interrupt = Interrupt;
+exception Interrupt = SML90.Interrupt;
fun interrupt () = raise Interrupt;
@@ -105,6 +115,17 @@
exception EXCEPTIONS of exn list;
+
+(* low-level trace *)
+
+fun trace exn_message output e =
+ PolyML.Exception.traceException
+ (e, fn (trace, exn) =>
+ let
+ val title = "Exception trace - " ^ exn_message exn;
+ val () = output (String.concatWith "\n" (title :: trace));
+ in reraise exn end);
+
end;
datatype illegal = Interrupt;
--- a/src/Pure/RAW/exn_trace.ML Thu Mar 03 14:03:06 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* Title: Pure/RAW/exn_trace.ML
- Author: Makarius
-
-Exception trace via ML output, for Poly/ML 5.5.1 or later.
-*)
-
-fun print_exception_trace exn_message output e =
- PolyML.Exception.traceException
- (e, fn (trace, exn) =>
- let
- val title = "Exception trace - " ^ exn_message exn;
- val _ = output (String.concatWith "\n" (title :: trace));
- in reraise exn end);
-
-PolyML.Compiler.reportExhaustiveHandlers := true;
--- a/src/Pure/RAW/ml_compiler0.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/RAW/ml_compiler0.ML Thu Mar 03 15:23:02 2016 +0100
@@ -74,10 +74,10 @@
(while not (List.null (! in_buffer)) do
PolyML.compiler (get, parameters) ())
handle exn =>
- if Exn.is_interrupt exn then reraise exn
+ if Exn.is_interrupt exn then Exn.reraise exn
else
(put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); reraise exn);
+ error (output ()); Exn.reraise exn);
in if verbose then print (output ()) else () end;
fun use_file context {verbose, debug} file =
--- a/src/Pure/ROOT Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/ROOT Thu Mar 03 15:23:02 2016 +0100
@@ -5,7 +5,6 @@
files
"RAW/ROOT_polyml.ML"
"RAW/exn.ML"
- "RAW/exn_trace.ML"
"RAW/fixed_int_dummy.ML"
"RAW/ml_compiler0.ML"
"RAW/ml_debugger.ML"
@@ -23,7 +22,6 @@
files
"RAW/ROOT_polyml.ML"
"RAW/exn.ML"
- "RAW/exn_trace.ML"
"RAW/fixed_int_dummy.ML"
"RAW/ml_compiler0.ML"
"RAW/ml_debugger.ML"
--- a/src/Pure/Syntax/syntax_phases.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Thu Mar 03 15:23:02 2016 +0100
@@ -310,7 +310,7 @@
fun report_result ctxt pos ambig_msgs results =
(case (proper_results results, failed_results results) of
- ([], (reports, exn) :: _) => (Context_Position.reports_text ctxt reports; reraise exn)
+ ([], (reports, exn) :: _) => (Context_Position.reports_text ctxt reports; Exn.reraise exn)
| ([(reports, x)], _) => (Context_Position.reports_text ctxt reports; x)
| _ =>
if null ambig_msgs then
--- a/src/Pure/System/invoke_scala.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/System/invoke_scala.ML Thu Mar 03 15:23:02 2016 +0100
@@ -63,7 +63,7 @@
Isabelle_Process.protocol_command "Invoke_Scala.fulfill"
(fn [id, tag, res] =>
fulfill id tag res
- handle exn => if Exn.is_interrupt exn then () else reraise exn);
+ handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn);
end;
--- a/src/Pure/System/isabelle_process.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/System/isabelle_process.ML Thu Mar 03 15:23:02 2016 +0100
@@ -188,7 +188,7 @@
val init = uninterruptible (fn _ => fn socket =>
let
val _ = SHA1_Samples.test ()
- handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); reraise exn);
+ handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
val _ = Output.physical_stderr Symbol.STX;
val _ = Printer.show_markup_default := true;
--- a/src/Pure/Tools/debugger.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/Tools/debugger.ML Thu Mar 03 15:23:02 2016 +0100
@@ -33,7 +33,7 @@
fun error_wrapper e = e ()
handle exn =>
- if Exn.is_interrupt exn then reraise exn
+ if Exn.is_interrupt exn then Exn.reraise exn
else error_message (Runtime.exn_message exn);
--- a/src/Pure/Tools/simplifier_trace.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/Tools/simplifier_trace.ML Thu Mar 03 15:23:02 2016 +0100
@@ -405,7 +405,7 @@
(case result of
SOME promise => Future.fulfill promise reply
| NONE => ()) (* FIXME handle protocol failure, just like in active.ML (!?) *)
- end handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn)
+ end handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn)
--- a/src/Pure/morphism.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Pure/morphism.ML Thu Mar 03 15:23:02 2016 +0100
@@ -52,7 +52,8 @@
exception MORPHISM of string * exn;
fun app (name, f) x = f x
- handle exn => if Exn.is_interrupt exn then reraise exn else raise MORPHISM (name, exn);
+ handle exn =>
+ if Exn.is_interrupt exn then Exn.reraise exn else raise MORPHISM (name, exn);
fun apply fs = fold_rev app fs;
--- a/src/Tools/try.ML Thu Mar 03 14:03:06 2016 +0100
+++ b/src/Tools/try.ML Thu Mar 03 15:23:02 2016 +0100
@@ -114,7 +114,7 @@
(true, (_, outcome)) => List.app Output.information outcome
| _ => ())
else ()
- end handle exn => if Exn.is_interrupt exn then reraise exn else ()}
+ end handle exn => if Exn.is_interrupt exn then Exn.reraise exn else ()}
else NONE)