src/Pure/System/isabelle_process.ML
changeset 57975 c657c68a60ab
parent 56895 f058120aaad4
child 57979 fc136831d6ca
     1.1 --- a/src/Pure/System/isabelle_process.ML	Wed Aug 13 20:21:04 2014 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Fri Aug 15 13:39:59 2014 +0200
     1.3 @@ -121,6 +121,7 @@
     1.4      Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
     1.5      Output.error_message_fn :=
     1.6        (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
     1.7 +    Output.system_message_fn := message Markup.systemN [];
     1.8      Output.protocol_message_fn := message Markup.protocolN;
     1.9      Output.urgent_message_fn := ! Output.writeln_fn;
    1.10      Output.prompt_fn := ignore;
    1.11 @@ -137,7 +138,8 @@
    1.12  
    1.13  fun recover crash =
    1.14    (Synchronized.change crashes (cons crash);
    1.15 -    warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
    1.16 +    Output.physical_stderr
    1.17 +      "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n");
    1.18  
    1.19  fun read_chunk channel len =
    1.20    let
    1.21 @@ -167,10 +169,10 @@
    1.22  fun loop channel =
    1.23    let val continue =
    1.24      (case read_command channel of
    1.25 -      [] => (Output.error_message "Isabelle process: no input"; true)
    1.26 +      [] => (Output.system_message "Isabelle process: no input"; true)
    1.27      | name :: args => (task_context (fn () => run_command name args); true))
    1.28      handle Runtime.TERMINATE => false
    1.29 -      | exn => (Runtime.exn_error_message exn handle crash => recover crash; true);
    1.30 +      | exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
    1.31    in
    1.32      if continue then loop channel
    1.33      else (Future.shutdown (); Execution.reset (); ())