# HG changeset patch
# User wenzelm
# Date 1408102799 -7200
# Node ID c657c68a60ab64e564063486d2849693fb76962f
# Parent  ba0b6c2338f0a603ba546371eac780e5e60a9233
explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
more robust crash recovery: warning could crash again;

diff -r ba0b6c2338f0 -r c657c68a60ab src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Wed Aug 13 20:21:04 2014 +0200
+++ b/src/Pure/General/output.ML	Fri Aug 15 13:39:59 2014 +0200
@@ -29,6 +29,7 @@
   val urgent_message: string -> unit
   val error_message': serial * string -> unit
   val error_message: string -> unit
+  val system_message: string -> unit
   val prompt: string -> unit
   val status: string -> unit
   val report: string list -> unit
@@ -45,6 +46,7 @@
   val tracing_fn: (output list -> unit) Unsynchronized.ref
   val warning_fn: (output list -> unit) Unsynchronized.ref
   val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
+  val system_message_fn: (output list -> unit) Unsynchronized.ref
   val prompt_fn: (output -> unit) Unsynchronized.ref
   val status_fn: (output list -> unit) Unsynchronized.ref
   val report_fn: (output list -> unit) Unsynchronized.ref
@@ -101,6 +103,7 @@
 val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
 val error_message_fn =
   Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
+val system_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
 val prompt_fn = Unsynchronized.ref physical_stdout;  (*Proof General legacy*)
 val status_fn = Unsynchronized.ref (fn _: output list => ());
 val report_fn = Unsynchronized.ref (fn _: output list => ());
@@ -115,6 +118,7 @@
 fun warning s = ! warning_fn [output s];
 fun error_message' (i, s) = ! error_message_fn (i, [output s]);
 fun error_message s = error_message' (serial (), s);
+fun system_message s = ! system_message_fn [output s];
 fun prompt s = ! prompt_fn (output s);
 fun status s = ! status_fn [output s];
 fun report ss = ! report_fn (map output ss);
diff -r ba0b6c2338f0 -r c657c68a60ab src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Wed Aug 13 20:21:04 2014 +0200
+++ b/src/Pure/Isar/runtime.ML	Fri Aug 15 13:39:59 2014 +0200
@@ -16,6 +16,7 @@
   val exn_messages: exn -> (serial * string) list
   val exn_message: exn -> string
   val exn_error_message: exn -> unit
+  val exn_system_message: exn -> unit
   val exn_trace: (unit -> 'a) -> 'a
   val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
   val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
@@ -135,6 +136,7 @@
   | msgs => cat_lines (map snd msgs));
 
 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;
 
 
diff -r ba0b6c2338f0 -r c657c68a60ab src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Aug 13 20:21:04 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Aug 15 13:39:59 2014 +0200
@@ -156,6 +156,7 @@
   val tracingN: string
   val warningN: string
   val errorN: string
+  val systemN: string
   val protocolN: string
   val legacyN: string val legacy: T
   val promptN: string val prompt: T
@@ -527,6 +528,7 @@
 val tracingN = "tracing";
 val warningN = "warning";
 val errorN = "error";
+val systemN = "system";
 val protocolN = "protocol";
 
 val (legacyN, legacy) = markup_elem "legacy";
diff -r ba0b6c2338f0 -r c657c68a60ab src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Aug 13 20:21:04 2014 +0200
+++ b/src/Pure/System/isabelle_process.ML	Fri Aug 15 13:39:59 2014 +0200
@@ -121,6 +121,7 @@
     Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
     Output.error_message_fn :=
       (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
+    Output.system_message_fn := message Markup.systemN [];
     Output.protocol_message_fn := message Markup.protocolN;
     Output.urgent_message_fn := ! Output.writeln_fn;
     Output.prompt_fn := ignore;
@@ -137,7 +138,8 @@
 
 fun recover crash =
   (Synchronized.change crashes (cons crash);
-    warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
+    Output.physical_stderr
+      "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
 
 fun read_chunk channel len =
   let
@@ -167,10 +169,10 @@
 fun loop channel =
   let val continue =
     (case read_command channel of
-      [] => (Output.error_message "Isabelle process: no input"; true)
+      [] => (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_error_message exn handle crash => recover crash; true);
+      | exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
   in
     if continue then loop channel
     else (Future.shutdown (); Execution.reset (); ())