more informative failure of protocol commands, with exception trace;
eliminated obsolete Runtime.TERMINATE (left-over from former 'exit' command);
--- a/src/Pure/Concurrent/simple_thread.ML Wed Nov 26 11:43:51 2014 +0100
+++ b/src/Pure/Concurrent/simple_thread.ML Wed Nov 26 14:35:55 2014 +0100
@@ -23,7 +23,7 @@
fun fork interrupts body =
Thread.fork (fn () =>
- print_exception_trace General.exnMessage (fn () =>
+ print_exception_trace General.exnMessage tracing (fn () =>
body () handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
attributes interrupts);
--- a/src/Pure/Isar/runtime.ML Wed Nov 26 11:43:51 2014 +0100
+++ b/src/Pure/Isar/runtime.ML Wed Nov 26 14:35:55 2014 +0100
@@ -7,7 +7,6 @@
signature RUNTIME =
sig
exception UNDEF
- exception TERMINATE
exception EXCURSION_FAIL of exn * string
exception TOPLEVEL_ERROR
val exn_context: Proof.context option -> exn -> exn
@@ -30,7 +29,6 @@
(** exceptions **)
exception UNDEF;
-exception TERMINATE;
exception EXCURSION_FAIL of exn * string;
exception TOPLEVEL_ERROR;
@@ -96,8 +94,7 @@
let
val msg =
(case exn of
- TERMINATE => "Exit"
- | TimeLimit.TimeOut => "Timeout"
+ TimeLimit.TimeOut => "Timeout"
| TOPLEVEL_ERROR => "Error"
| ERROR "" => "Error"
| ERROR msg => msg
@@ -136,7 +133,7 @@
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 e;
+fun exn_trace e = print_exception_trace exn_message tracing e;
@@ -144,8 +141,7 @@
fun debugging opt_context f x =
if ML_Options.exception_trace_enabled opt_context
- then print_exception_trace exn_message (fn () => f x)
- else f x;
+ then exn_trace (fn () => f x) else f x;
fun controlled_execution opt_context f x =
(f |> debugging opt_context |> Future.interruptible_task) x;
--- a/src/Pure/Isar/toplevel.ML Wed Nov 26 11:43:51 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML Wed Nov 26 14:35:55 2014 +0100
@@ -80,7 +80,7 @@
val add_hook: (transition -> state -> state -> unit) -> unit
val get_timing: transition -> Time.time option
val put_timing: Time.time option -> transition -> transition
- val transition: bool -> transition -> state -> (state * (exn * string) option) option
+ val transition: bool -> transition -> state -> state * (exn * string) option
val command_errors: bool -> transition -> state -> Runtime.error list * state option
val command_exception: bool -> transition -> state -> state
val reset_theory: state -> state option
@@ -569,18 +569,12 @@
fun transition int tr st =
let
- val hooks = get_hooks ();
- fun apply_hooks st' = hooks |> List.app (fn f => (try (fn () => f tr st st') (); ()));
-
- val ctxt = try context_of st;
- val res =
- (case app int tr st of
- (_, SOME Runtime.TERMINATE) => NONE
- | (st', SOME (Runtime.EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info)
- | (st', SOME exn) => SOME (st', SOME (Runtime.exn_context ctxt exn, at_command tr))
- | (st', NONE) => SOME (st', NONE));
- val _ = (case res of SOME (st', NONE) => apply_hooks st' | _ => ());
- in res end;
+ val (st', opt_err) = app int tr st;
+ val opt_err' = opt_err |> Option.map
+ (fn Runtime.EXCURSION_FAIL exn_info => exn_info
+ | exn => (Runtime.exn_context (try context_of st) exn, at_command tr));
+ val _ = get_hooks () |> List.app (fn f => (try (fn () => f tr st st') (); ()));
+ in (st', opt_err') end;
end;
@@ -589,16 +583,15 @@
fun command_errors int tr st =
(case transition int tr st of
- SOME (st', NONE) => ([], SOME st')
- | SOME (_, SOME (exn, _)) => (Runtime.exn_messages_ids exn, NONE)
- | NONE => (Runtime.exn_messages_ids Runtime.TERMINATE, NONE));
+ (st', NONE) => ([], SOME st')
+ | (_, SOME (exn, _)) => (Runtime.exn_messages_ids exn, NONE));
fun command_exception int tr st =
(case transition int tr st of
- SOME (st', NONE) => st'
- | SOME (_, SOME (exn, info)) =>
- if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
- | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
+ (st', NONE) => st'
+ | (_, SOME (exn, info)) =>
+ if Exn.is_interrupt exn then reraise exn
+ else raise Runtime.EXCURSION_FAIL (exn, info));
val command = command_exception false;
--- a/src/Pure/ML-Systems/polyml.ML Wed Nov 26 11:43:51 2014 +0100
+++ b/src/Pure/ML-Systems/polyml.ML Wed Nov 26 14:35:55 2014 +0100
@@ -93,7 +93,7 @@
(* ML runtime system *)
-fun print_exception_trace (_: exn -> string) = PolyML.exception_trace;
+fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
val timing = PolyML.timing;
val profiling = PolyML.profiling;
--- a/src/Pure/ML-Systems/smlnj.ML Wed Nov 26 11:43:51 2014 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Wed Nov 26 14:35:55 2014 +0100
@@ -76,7 +76,7 @@
fun profile (n: int) f x = f x;
(*dummy implementation*)
-fun print_exception_trace (_: exn -> string) f = f ();
+fun print_exception_trace (_: exn -> string) (_: string -> unit) f = f ();
(* ML command execution *)
--- a/src/Pure/ML/exn_trace_polyml-5.5.1.ML Wed Nov 26 11:43:51 2014 +0100
+++ b/src/Pure/ML/exn_trace_polyml-5.5.1.ML Wed Nov 26 14:35:55 2014 +0100
@@ -4,12 +4,12 @@
Exception trace for Poly/ML 5.5.1, using regular Isabelle output.
*)
-fun print_exception_trace exn_message e =
+fun print_exception_trace exn_message output e =
PolyML.Exception.traceException
(e, fn (trace, exn) =>
let
val title = "Exception trace - " ^ exn_message exn;
- val _ = tracing (cat_lines (title :: trace));
+ val _ = output (cat_lines (title :: trace));
in reraise exn end);
PolyML.Compiler.reportExhaustiveHandlers := true;
--- a/src/Pure/System/isabelle_process.ML Wed Nov 26 11:43:51 2014 +0100
+++ b/src/Pure/System/isabelle_process.ML Wed Nov 26 14:35:55 2014 +0100
@@ -47,9 +47,8 @@
(case Symtab.lookup (Synchronized.value commands) name of
NONE => error ("Undefined Isabelle protocol command " ^ quote name)
| SOME cmd =>
- (Runtime.debugging NONE cmd args handle exn =>
- error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^
- Runtime.exn_message exn)));
+ (print_exception_trace Runtime.exn_message Output.system_message (fn () => cmd args)
+ handle _ (*sic!*) => error ("Isabelle protocol command failure: " ^ quote name)));
end;
@@ -158,9 +157,8 @@
end;
fun read_command channel =
- (case System_Channel.input_line channel of
- NONE => raise Runtime.TERMINATE
- | SOME line => map (read_chunk channel) (space_explode "," line));
+ System_Channel.input_line channel
+ |> Option.map (fn line => map (read_chunk channel) (space_explode "," line));
fun task_context e =
Future.task_context "Isabelle_Process.loop" (Future.new_group NONE) e ();
@@ -168,12 +166,13 @@
in
fun loop channel =
- let val continue =
- (case read_command channel of
- [] => (Output.system_message "Isabelle process: no input"; true)
- | name :: args => (task_context (fn () => run_command name args); true))
- handle Runtime.TERMINATE => false
- | exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
+ let
+ val continue =
+ (case read_command channel of
+ NONE => false
+ | SOME [] => (Output.system_message "Isabelle process: no input"; true)
+ | SOME (name :: args) => (task_context (fn () => run_command name args); true))
+ handle exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
in
if continue then loop channel
else (Future.shutdown (); Execution.reset (); ())