# HG changeset patch # User wenzelm # Date 1457014982 -3600 # Node ID 9e2a65912111812025a9fe7f737e09526598db81 # Parent f14f17e656a694c9d32c83da2d8b3fe13fb6d6b7 clarified modules; tuned signature; diff -r f14f17e656a6 -r 9e2a65912111 src/Doc/Implementation/ML.thy --- 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}~\exn\ raises exception \exn\ while preserving its implicit + \<^descr> @{ML Exn.reraise}~\exn\ raises exception \exn\ while preserving its implicit position information (if possible, depending on the ML platform). \<^descr> @{ML Runtime.exn_trace}~@{ML_text "(fn () =>"}~\e\@{ML_text ")"} evaluates diff -r f14f17e656a6 -r 9e2a65912111 src/HOL/Matrix_LP/Cplex_tools.ML --- 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 = diff -r f14f17e656a6 -r 9e2a65912111 src/HOL/Mirabelle/Tools/mirabelle.ML --- 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 diff -r f14f17e656a6 -r 9e2a65912111 src/HOL/Nitpick_Examples/Mono_Nits.thy --- 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 diff -r f14f17e656a6 -r 9e2a65912111 src/HOL/TPTP/TPTP_Interpret_Test.thy --- 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); diff -r f14f17e656a6 -r 9e2a65912111 src/HOL/TPTP/TPTP_Test.thy --- 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); diff -r f14f17e656a6 -r 9e2a65912111 src/HOL/Tools/Old_Datatype/old_datatype.ML --- 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 diff -r f14f17e656a6 -r 9e2a65912111 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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 _ = diff -r f14f17e656a6 -r 9e2a65912111 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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) diff -r f14f17e656a6 -r 9e2a65912111 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML --- 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 []} diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/Concurrent/bash.ML --- 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; diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/Concurrent/bash_windows.ML --- 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; diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/Concurrent/future.ML --- 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 ())); diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/Concurrent/par_exn.ML --- 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; diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/Concurrent/par_list.ML --- 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); diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/Concurrent/single_assignment.ML --- 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); diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/Concurrent/standard_thread.ML --- 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); diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/Concurrent/synchronized.ML --- 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)) ()) diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/General/basics.ML --- 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); diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/Isar/runtime.ML --- 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 = diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/Isar/toplevel.ML --- 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; diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/ML/ml_compiler.ML --- 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 = diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/PIDE/command.ML --- 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 diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/PIDE/document.ML --- 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, diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/PIDE/protocol.ML --- 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" diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/RAW/ROOT_polyml.ML --- 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> "; diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/RAW/exn.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; diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/RAW/exn_trace.ML --- 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; diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/RAW/ml_compiler0.ML --- 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 = diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/ROOT --- 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" diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/Syntax/syntax_phases.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 diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/System/invoke_scala.ML --- 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; diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/System/isabelle_process.ML --- 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; diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/Tools/debugger.ML --- 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); diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/Tools/simplifier_trace.ML --- 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) diff -r f14f17e656a6 -r 9e2a65912111 src/Pure/morphism.ML --- 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; diff -r f14f17e656a6 -r 9e2a65912111 src/Tools/try.ML --- 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)