explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
authorwenzelm
Fri Aug 15 13:39:59 2014 +0200 (2014-08-15)
changeset 57975c657c68a60ab
parent 57974 ba0b6c2338f0
child 57976 bf99106b6672
explicit system message for protocol failure -- show on Syslog panel instead of Raw Output;
more robust crash recovery: warning could crash again;
src/Pure/General/output.ML
src/Pure/Isar/runtime.ML
src/Pure/PIDE/markup.ML
src/Pure/System/isabelle_process.ML
     1.1 --- a/src/Pure/General/output.ML	Wed Aug 13 20:21:04 2014 +0200
     1.2 +++ b/src/Pure/General/output.ML	Fri Aug 15 13:39:59 2014 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4    val urgent_message: string -> unit
     1.5    val error_message': serial * string -> unit
     1.6    val error_message: string -> unit
     1.7 +  val system_message: string -> unit
     1.8    val prompt: string -> unit
     1.9    val status: string -> unit
    1.10    val report: string list -> unit
    1.11 @@ -45,6 +46,7 @@
    1.12    val tracing_fn: (output list -> unit) Unsynchronized.ref
    1.13    val warning_fn: (output list -> unit) Unsynchronized.ref
    1.14    val error_message_fn: (serial * output list -> unit) Unsynchronized.ref
    1.15 +  val system_message_fn: (output list -> unit) Unsynchronized.ref
    1.16    val prompt_fn: (output -> unit) Unsynchronized.ref
    1.17    val status_fn: (output list -> unit) Unsynchronized.ref
    1.18    val report_fn: (output list -> unit) Unsynchronized.ref
    1.19 @@ -101,6 +103,7 @@
    1.20  val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
    1.21  val error_message_fn =
    1.22    Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
    1.23 +val system_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    1.24  val prompt_fn = Unsynchronized.ref physical_stdout;  (*Proof General legacy*)
    1.25  val status_fn = Unsynchronized.ref (fn _: output list => ());
    1.26  val report_fn = Unsynchronized.ref (fn _: output list => ());
    1.27 @@ -115,6 +118,7 @@
    1.28  fun warning s = ! warning_fn [output s];
    1.29  fun error_message' (i, s) = ! error_message_fn (i, [output s]);
    1.30  fun error_message s = error_message' (serial (), s);
    1.31 +fun system_message s = ! system_message_fn [output s];
    1.32  fun prompt s = ! prompt_fn (output s);
    1.33  fun status s = ! status_fn [output s];
    1.34  fun report ss = ! report_fn (map output ss);
     2.1 --- a/src/Pure/Isar/runtime.ML	Wed Aug 13 20:21:04 2014 +0200
     2.2 +++ b/src/Pure/Isar/runtime.ML	Fri Aug 15 13:39:59 2014 +0200
     2.3 @@ -16,6 +16,7 @@
     2.4    val exn_messages: exn -> (serial * string) list
     2.5    val exn_message: exn -> string
     2.6    val exn_error_message: exn -> unit
     2.7 +  val exn_system_message: exn -> unit
     2.8    val exn_trace: (unit -> 'a) -> 'a
     2.9    val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
    2.10    val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
    2.11 @@ -135,6 +136,7 @@
    2.12    | msgs => cat_lines (map snd msgs));
    2.13  
    2.14  val exn_error_message = Output.error_message o exn_message;
    2.15 +val exn_system_message = Output.system_message o exn_message;
    2.16  fun exn_trace e = print_exception_trace exn_message e;
    2.17  
    2.18  
     3.1 --- a/src/Pure/PIDE/markup.ML	Wed Aug 13 20:21:04 2014 +0200
     3.2 +++ b/src/Pure/PIDE/markup.ML	Fri Aug 15 13:39:59 2014 +0200
     3.3 @@ -156,6 +156,7 @@
     3.4    val tracingN: string
     3.5    val warningN: string
     3.6    val errorN: string
     3.7 +  val systemN: string
     3.8    val protocolN: string
     3.9    val legacyN: string val legacy: T
    3.10    val promptN: string val prompt: T
    3.11 @@ -527,6 +528,7 @@
    3.12  val tracingN = "tracing";
    3.13  val warningN = "warning";
    3.14  val errorN = "error";
    3.15 +val systemN = "system";
    3.16  val protocolN = "protocol";
    3.17  
    3.18  val (legacyN, legacy) = markup_elem "legacy";
     4.1 --- a/src/Pure/System/isabelle_process.ML	Wed Aug 13 20:21:04 2014 +0200
     4.2 +++ b/src/Pure/System/isabelle_process.ML	Fri Aug 15 13:39:59 2014 +0200
     4.3 @@ -121,6 +121,7 @@
     4.4      Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
     4.5      Output.error_message_fn :=
     4.6        (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
     4.7 +    Output.system_message_fn := message Markup.systemN [];
     4.8      Output.protocol_message_fn := message Markup.protocolN;
     4.9      Output.urgent_message_fn := ! Output.writeln_fn;
    4.10      Output.prompt_fn := ignore;
    4.11 @@ -137,7 +138,8 @@
    4.12  
    4.13  fun recover crash =
    4.14    (Synchronized.change crashes (cons crash);
    4.15 -    warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
    4.16 +    Output.physical_stderr
    4.17 +      "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
    4.18  
    4.19  fun read_chunk channel len =
    4.20    let
    4.21 @@ -167,10 +169,10 @@
    4.22  fun loop channel =
    4.23    let val continue =
    4.24      (case read_command channel of
    4.25 -      [] => (Output.error_message "Isabelle process: no input"; true)
    4.26 +      [] => (Output.system_message "Isabelle process: no input"; true)
    4.27      | name :: args => (task_context (fn () => run_command name args); true))
    4.28      handle Runtime.TERMINATE => false
    4.29 -      | exn => (Runtime.exn_error_message exn handle crash => recover crash; true);
    4.30 +      | exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
    4.31    in
    4.32      if continue then loop channel
    4.33      else (Future.shutdown (); Execution.reset (); ())