more informative failure of protocol commands, with exception trace;
authorwenzelm
Wed Nov 26 14:35:55 2014 +0100 (2014-11-26 ago)
changeset 590555a7157b8e870
parent 59054 61b723761dff
child 59056 cbe9563c03d1
more informative failure of protocol commands, with exception trace;
eliminated obsolete Runtime.TERMINATE (left-over from former 'exit' command);
src/Pure/Concurrent/simple_thread.ML
src/Pure/Isar/runtime.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ML/exn_trace_polyml-5.5.1.ML
src/Pure/System/isabelle_process.ML
     1.1 --- a/src/Pure/Concurrent/simple_thread.ML	Wed Nov 26 11:43:51 2014 +0100
     1.2 +++ b/src/Pure/Concurrent/simple_thread.ML	Wed Nov 26 14:35:55 2014 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  
     1.5  fun fork interrupts body =
     1.6    Thread.fork (fn () =>
     1.7 -    print_exception_trace General.exnMessage (fn () =>
     1.8 +    print_exception_trace General.exnMessage tracing (fn () =>
     1.9        body () handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
    1.10      attributes interrupts);
    1.11  
     2.1 --- a/src/Pure/Isar/runtime.ML	Wed Nov 26 11:43:51 2014 +0100
     2.2 +++ b/src/Pure/Isar/runtime.ML	Wed Nov 26 14:35:55 2014 +0100
     2.3 @@ -7,7 +7,6 @@
     2.4  signature RUNTIME =
     2.5  sig
     2.6    exception UNDEF
     2.7 -  exception TERMINATE
     2.8    exception EXCURSION_FAIL of exn * string
     2.9    exception TOPLEVEL_ERROR
    2.10    val exn_context: Proof.context option -> exn -> exn
    2.11 @@ -30,7 +29,6 @@
    2.12  (** exceptions **)
    2.13  
    2.14  exception UNDEF;
    2.15 -exception TERMINATE;
    2.16  exception EXCURSION_FAIL of exn * string;
    2.17  exception TOPLEVEL_ERROR;
    2.18  
    2.19 @@ -96,8 +94,7 @@
    2.20          let
    2.21            val msg =
    2.22              (case exn of
    2.23 -              TERMINATE => "Exit"
    2.24 -            | TimeLimit.TimeOut => "Timeout"
    2.25 +              TimeLimit.TimeOut => "Timeout"
    2.26              | TOPLEVEL_ERROR => "Error"
    2.27              | ERROR "" => "Error"
    2.28              | ERROR msg => msg
    2.29 @@ -136,7 +133,7 @@
    2.30  
    2.31  val exn_error_message = Output.error_message o exn_message;
    2.32  val exn_system_message = Output.system_message o exn_message;
    2.33 -fun exn_trace e = print_exception_trace exn_message e;
    2.34 +fun exn_trace e = print_exception_trace exn_message tracing e;
    2.35  
    2.36  
    2.37  
    2.38 @@ -144,8 +141,7 @@
    2.39  
    2.40  fun debugging opt_context f x =
    2.41    if ML_Options.exception_trace_enabled opt_context
    2.42 -  then print_exception_trace exn_message (fn () => f x)
    2.43 -  else f x;
    2.44 +  then exn_trace (fn () => f x) else f x;
    2.45  
    2.46  fun controlled_execution opt_context f x =
    2.47    (f |> debugging opt_context |> Future.interruptible_task) x;
     3.1 --- a/src/Pure/Isar/toplevel.ML	Wed Nov 26 11:43:51 2014 +0100
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Nov 26 14:35:55 2014 +0100
     3.3 @@ -80,7 +80,7 @@
     3.4    val add_hook: (transition -> state -> state -> unit) -> unit
     3.5    val get_timing: transition -> Time.time option
     3.6    val put_timing: Time.time option -> transition -> transition
     3.7 -  val transition: bool -> transition -> state -> (state * (exn * string) option) option
     3.8 +  val transition: bool -> transition -> state -> state * (exn * string) option
     3.9    val command_errors: bool -> transition -> state -> Runtime.error list * state option
    3.10    val command_exception: bool -> transition -> state -> state
    3.11    val reset_theory: state -> state option
    3.12 @@ -569,18 +569,12 @@
    3.13  
    3.14  fun transition int tr st =
    3.15    let
    3.16 -    val hooks = get_hooks ();
    3.17 -    fun apply_hooks st' = hooks |> List.app (fn f => (try (fn () => f tr st st') (); ()));
    3.18 -
    3.19 -    val ctxt = try context_of st;
    3.20 -    val res =
    3.21 -      (case app int tr st of
    3.22 -        (_, SOME Runtime.TERMINATE) => NONE
    3.23 -      | (st', SOME (Runtime.EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info)
    3.24 -      | (st', SOME exn) => SOME (st', SOME (Runtime.exn_context ctxt exn, at_command tr))
    3.25 -      | (st', NONE) => SOME (st', NONE));
    3.26 -    val _ = (case res of SOME (st', NONE) => apply_hooks st' | _ => ());
    3.27 -  in res end;
    3.28 +    val (st', opt_err) = app int tr st;
    3.29 +    val opt_err' = opt_err |> Option.map
    3.30 +      (fn Runtime.EXCURSION_FAIL exn_info => exn_info
    3.31 +        | exn => (Runtime.exn_context (try context_of st) exn, at_command tr));
    3.32 +    val _ = get_hooks () |> List.app (fn f => (try (fn () => f tr st st') (); ()));
    3.33 +  in (st', opt_err') end;
    3.34  
    3.35  end;
    3.36  
    3.37 @@ -589,16 +583,15 @@
    3.38  
    3.39  fun command_errors int tr st =
    3.40    (case transition int tr st of
    3.41 -    SOME (st', NONE) => ([], SOME st')
    3.42 -  | SOME (_, SOME (exn, _)) => (Runtime.exn_messages_ids exn, NONE)
    3.43 -  | NONE => (Runtime.exn_messages_ids Runtime.TERMINATE, NONE));
    3.44 +    (st', NONE) => ([], SOME st')
    3.45 +  | (_, SOME (exn, _)) => (Runtime.exn_messages_ids exn, NONE));
    3.46  
    3.47  fun command_exception int tr st =
    3.48    (case transition int tr st of
    3.49 -    SOME (st', NONE) => st'
    3.50 -  | SOME (_, SOME (exn, info)) =>
    3.51 -      if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info)
    3.52 -  | NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr));
    3.53 +    (st', NONE) => st'
    3.54 +  | (_, SOME (exn, info)) =>
    3.55 +      if Exn.is_interrupt exn then reraise exn
    3.56 +      else raise Runtime.EXCURSION_FAIL (exn, info));
    3.57  
    3.58  val command = command_exception false;
    3.59  
     4.1 --- a/src/Pure/ML-Systems/polyml.ML	Wed Nov 26 11:43:51 2014 +0100
     4.2 +++ b/src/Pure/ML-Systems/polyml.ML	Wed Nov 26 14:35:55 2014 +0100
     4.3 @@ -93,7 +93,7 @@
     4.4  
     4.5  (* ML runtime system *)
     4.6  
     4.7 -fun print_exception_trace (_: exn -> string) = PolyML.exception_trace;
     4.8 +fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
     4.9  val timing = PolyML.timing;
    4.10  val profiling = PolyML.profiling;
    4.11  
     5.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Nov 26 11:43:51 2014 +0100
     5.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Nov 26 14:35:55 2014 +0100
     5.3 @@ -76,7 +76,7 @@
     5.4  fun profile (n: int) f x = f x;
     5.5  
     5.6  (*dummy implementation*)
     5.7 -fun print_exception_trace (_: exn -> string) f = f ();
     5.8 +fun print_exception_trace (_: exn -> string) (_: string -> unit) f = f ();
     5.9  
    5.10  
    5.11  (* ML command execution *)
     6.1 --- a/src/Pure/ML/exn_trace_polyml-5.5.1.ML	Wed Nov 26 11:43:51 2014 +0100
     6.2 +++ b/src/Pure/ML/exn_trace_polyml-5.5.1.ML	Wed Nov 26 14:35:55 2014 +0100
     6.3 @@ -4,12 +4,12 @@
     6.4  Exception trace for Poly/ML 5.5.1, using regular Isabelle output.
     6.5  *)
     6.6  
     6.7 -fun print_exception_trace exn_message e =
     6.8 +fun print_exception_trace exn_message output e =
     6.9    PolyML.Exception.traceException
    6.10      (e, fn (trace, exn) =>
    6.11        let
    6.12          val title = "Exception trace - " ^ exn_message exn;
    6.13 -        val _ = tracing (cat_lines (title :: trace));
    6.14 +        val _ = output (cat_lines (title :: trace));
    6.15        in reraise exn end);
    6.16  
    6.17  PolyML.Compiler.reportExhaustiveHandlers := true;
     7.1 --- a/src/Pure/System/isabelle_process.ML	Wed Nov 26 11:43:51 2014 +0100
     7.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Nov 26 14:35:55 2014 +0100
     7.3 @@ -47,9 +47,8 @@
     7.4    (case Symtab.lookup (Synchronized.value commands) name of
     7.5      NONE => error ("Undefined Isabelle protocol command " ^ quote name)
     7.6    | SOME cmd =>
     7.7 -      (Runtime.debugging NONE cmd args handle exn =>
     7.8 -        error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^
     7.9 -          Runtime.exn_message exn)));
    7.10 +      (print_exception_trace Runtime.exn_message Output.system_message (fn () => cmd args)
    7.11 +        handle _ (*sic!*) => error ("Isabelle protocol command failure: " ^ quote name)));
    7.12  
    7.13  end;
    7.14  
    7.15 @@ -158,9 +157,8 @@
    7.16    end;
    7.17  
    7.18  fun read_command channel =
    7.19 -  (case System_Channel.input_line channel of
    7.20 -    NONE => raise Runtime.TERMINATE
    7.21 -  | SOME line => map (read_chunk channel) (space_explode "," line));
    7.22 +  System_Channel.input_line channel
    7.23 +  |> Option.map (fn line => map (read_chunk channel) (space_explode "," line));
    7.24  
    7.25  fun task_context e =
    7.26    Future.task_context "Isabelle_Process.loop" (Future.new_group NONE) e ();
    7.27 @@ -168,12 +166,13 @@
    7.28  in
    7.29  
    7.30  fun loop channel =
    7.31 -  let val continue =
    7.32 -    (case read_command channel of
    7.33 -      [] => (Output.system_message "Isabelle process: no input"; true)
    7.34 -    | name :: args => (task_context (fn () => run_command name args); true))
    7.35 -    handle Runtime.TERMINATE => false
    7.36 -      | exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
    7.37 +  let
    7.38 +    val continue =
    7.39 +      (case read_command channel of
    7.40 +        NONE => false
    7.41 +      | SOME [] => (Output.system_message "Isabelle process: no input"; true)
    7.42 +      | SOME (name :: args) => (task_context (fn () => run_command name args); true))
    7.43 +      handle exn => (Runtime.exn_system_message exn handle crash => recover crash; true);
    7.44    in
    7.45      if continue then loop channel
    7.46      else (Future.shutdown (); Execution.reset (); ())