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 (); ())