src/Pure/System/isabelle_process.ML
changeset 59055 5a7157b8e870
parent 58850 1bb0ad7827b4
child 59056 cbe9563c03d1
     1.1 --- a/src/Pure/System/isabelle_process.ML	Wed Nov 26 11:43:51 2014 +0100
     1.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Nov 26 14:35:55 2014 +0100
     1.3 @@ -47,9 +47,8 @@
     1.4    (case Symtab.lookup (Synchronized.value commands) name of
     1.5      NONE => error ("Undefined Isabelle protocol command " ^ quote name)
     1.6    | SOME cmd =>
     1.7 -      (Runtime.debugging NONE cmd args handle exn =>
     1.8 -        error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^
     1.9 -          Runtime.exn_message exn)));
    1.10 +      (print_exception_trace Runtime.exn_message Output.system_message (fn () => cmd args)
    1.11 +        handle _ (*sic!*) => error ("Isabelle protocol command failure: " ^ quote name)));
    1.12  
    1.13  end;
    1.14  
    1.15 @@ -158,9 +157,8 @@
    1.16    end;
    1.17  
    1.18  fun read_command channel =
    1.19 -  (case System_Channel.input_line channel of
    1.20 -    NONE => raise Runtime.TERMINATE
    1.21 -  | SOME line => map (read_chunk channel) (space_explode "," line));
    1.22 +  System_Channel.input_line channel
    1.23 +  |> Option.map (fn line => map (read_chunk channel) (space_explode "," line));
    1.24  
    1.25  fun task_context e =
    1.26    Future.task_context "Isabelle_Process.loop" (Future.new_group NONE) e ();
    1.27 @@ -168,12 +166,13 @@
    1.28  in
    1.29  
    1.30  fun loop channel =
    1.31 -  let val continue =
    1.32 -    (case read_command channel of
    1.33 -      [] => (Output.system_message "Isabelle process: no input"; true)
    1.34 -    | name :: args => (task_context (fn () => run_command name args); true))
    1.35 -    handle Runtime.TERMINATE => false
    1.36 -      | exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
    1.37 +  let
    1.38 +    val continue =
    1.39 +      (case read_command channel of
    1.40 +        NONE => false
    1.41 +      | SOME [] => (Output.system_message "Isabelle process: no input"; true)
    1.42 +      | SOME (name :: args) => (task_context (fn () => run_command name args); true))
    1.43 +      handle exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
    1.44    in
    1.45      if continue then loop channel
    1.46      else (Future.shutdown (); Execution.reset (); ())