clarified modules;
authorwenzelm
Thu Mar 03 15:23:02 2016 +0100 (2016-03-03)
changeset 625059e2a65912111
parent 62504 f14f17e656a6
child 62506 860cd901ab43
clarified modules;
tuned signature;
src/Doc/Implementation/ML.thy
src/HOL/Matrix_LP/Cplex_tools.ML
src/HOL/Mirabelle/Tools/mirabelle.ML
src/HOL/Nitpick_Examples/Mono_Nits.thy
src/HOL/TPTP/TPTP_Interpret_Test.thy
src/HOL/TPTP/TPTP_Test.thy
src/HOL/Tools/Old_Datatype/old_datatype.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
src/Pure/Concurrent/bash.ML
src/Pure/Concurrent/bash_windows.ML
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/par_exn.ML
src/Pure/Concurrent/par_list.ML
src/Pure/Concurrent/single_assignment.ML
src/Pure/Concurrent/standard_thread.ML
src/Pure/Concurrent/synchronized.ML
src/Pure/General/basics.ML
src/Pure/Isar/runtime.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML/ml_compiler.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/protocol.ML
src/Pure/RAW/ROOT_polyml.ML
src/Pure/RAW/exn.ML
src/Pure/RAW/exn_trace.ML
src/Pure/RAW/ml_compiler0.ML
src/Pure/ROOT
src/Pure/Syntax/syntax_phases.ML
src/Pure/System/invoke_scala.ML
src/Pure/System/isabelle_process.ML
src/Pure/Tools/debugger.ML
src/Pure/Tools/simplifier_trace.ML
src/Pure/morphism.ML
src/Tools/try.ML
     1.1 --- a/src/Doc/Implementation/ML.thy	Thu Mar 03 14:03:06 2016 +0100
     1.2 +++ b/src/Doc/Implementation/ML.thy	Thu Mar 03 15:23:02 2016 +0100
     1.3 @@ -1154,7 +1154,7 @@
     1.4    @{index_ML_exception ERROR: string} \\
     1.5    @{index_ML_exception Fail: string} \\
     1.6    @{index_ML Exn.is_interrupt: "exn -> bool"} \\
     1.7 -  @{index_ML reraise: "exn -> 'a"} \\
     1.8 +  @{index_ML Exn.reraise: "exn -> 'a"} \\
     1.9    @{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\
    1.10    \end{mldecls}
    1.11  
    1.12 @@ -1176,7 +1176,7 @@
    1.13    concrete exception constructors in user code. Handled interrupts need to be
    1.14    re-raised promptly!
    1.15  
    1.16 -  \<^descr> @{ML reraise}~\<open>exn\<close> raises exception \<open>exn\<close> while preserving its implicit
    1.17 +  \<^descr> @{ML Exn.reraise}~\<open>exn\<close> raises exception \<open>exn\<close> while preserving its implicit
    1.18    position information (if possible, depending on the ML platform).
    1.19  
    1.20    \<^descr> @{ML Runtime.exn_trace}~@{ML_text "(fn () =>"}~\<open>e\<close>@{ML_text ")"} evaluates
     2.1 --- a/src/HOL/Matrix_LP/Cplex_tools.ML	Thu Mar 03 14:03:06 2016 +0100
     2.2 +++ b/src/HOL/Matrix_LP/Cplex_tools.ML	Thu Mar 03 15:23:02 2016 +0100
     2.3 @@ -1158,7 +1158,7 @@
     2.4          result
     2.5      end
     2.6      handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer))
     2.7 -         | exn => if Exn.is_interrupt exn then reraise exn else raise (Execute answer)
     2.8 +         | exn => if Exn.is_interrupt exn then Exn.reraise exn else raise (Execute answer)
     2.9      end
    2.10  
    2.11  fun solve_cplex prog =
     3.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Mar 03 14:03:06 2016 +0100
     3.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Mar 03 15:23:02 2016 +0100
     3.3 @@ -71,11 +71,11 @@
     3.4  
     3.5  fun catch tag f id (st as {log, ...}: run_args) = (f id st; ())
     3.6    handle exn =>
     3.7 -    if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; ())
     3.8 +    if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; ())
     3.9  
    3.10  fun catch_result tag d f id (st as {log, ...}: run_args) = f id st
    3.11    handle exn =>
    3.12 -    if Exn.is_interrupt exn then reraise exn else (log_exn log tag id exn; d)
    3.13 +    if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; d)
    3.14  
    3.15  fun register (init, run, done) thy =
    3.16    let val id = length (Actions.get thy) + 1
     4.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Mar 03 14:03:06 2016 +0100
     4.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Mar 03 15:23:02 2016 +0100
     4.3 @@ -171,7 +171,7 @@
     4.4    end
     4.5    handle TimeLimit.TimeOut => "TIMEOUT"
     4.6         | NOT_SUPPORTED _ => "UNSUP"
     4.7 -       | exn => if Exn.is_interrupt exn then reraise exn else "UNKNOWN"
     4.8 +       | exn => if Exn.is_interrupt exn then Exn.reraise exn else "UNKNOWN"
     4.9  
    4.10  fun check_theory thy =
    4.11    let
     5.1 --- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Thu Mar 03 14:03:06 2016 +0100
     5.2 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Thu Mar 03 15:23:02 2016 +0100
     5.3 @@ -129,7 +129,7 @@
     5.4        val t1 = (parse_timed file |> fst)
     5.5        val t2 = (interpret_timed timeout file thy |> fst)
     5.6          handle exn => (*FIXME*)
     5.7 -          if Exn.is_interrupt exn then reraise exn
     5.8 +          if Exn.is_interrupt exn then Exn.reraise exn
     5.9            else
    5.10              (warning (" test: file " ^ Path.print file ^
    5.11               " raised exception: " ^ Runtime.exn_message exn);
     6.1 --- a/src/HOL/TPTP/TPTP_Test.thy	Thu Mar 03 14:03:06 2016 +0100
     6.2 +++ b/src/HOL/TPTP/TPTP_Test.thy	Thu Mar 03 15:23:02 2016 +0100
     6.3 @@ -60,7 +60,7 @@
     6.4       (*otherwise report exceptions as warnings*)
     6.5       handle exn =>
     6.6         if Exn.is_interrupt exn then
     6.7 -         reraise exn
     6.8 +         Exn.reraise exn
     6.9         else
    6.10           (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
    6.11            " raised exception: " ^ Runtime.exn_message exn);
     7.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Thu Mar 03 14:03:06 2016 +0100
     7.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Thu Mar 03 15:23:02 2016 +0100
     7.3 @@ -778,7 +778,7 @@
     7.4        Old_Datatype_Aux.check_nonempty descr
     7.5          handle (exn as Old_Datatype_Aux.Datatype_Empty s) =>
     7.6            if #strict config then error ("Nonemptiness check failed for datatype " ^ quote s)
     7.7 -          else reraise exn;
     7.8 +          else Exn.reraise exn;
     7.9  
    7.10      val _ =
    7.11        Old_Datatype_Aux.message config
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Mar 03 14:03:06 2016 +0100
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Mar 03 15:23:02 2016 +0100
     8.3 @@ -192,7 +192,7 @@
     8.4               handle
     8.5                 ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
     8.6               | exn =>
     8.7 -               if Exn.is_interrupt exn then reraise exn
     8.8 +               if Exn.is_interrupt exn then Exn.reraise exn
     8.9                 else (unknownN, fn () => "Internal error:\n" ^ Runtime.exn_message exn ^ "\n"))
    8.10  
    8.11          val _ =
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Mar 03 14:03:06 2016 +0100
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Mar 03 15:23:02 2016 +0100
     9.3 @@ -573,7 +573,7 @@
     9.4      (trace_msg ctxt (fn () => "Unknown fact " ^ quote name ^ " when " ^ when); def)
     9.5    | exn =>
     9.6      if Exn.is_interrupt exn then
     9.7 -      reraise exn
     9.8 +      Exn.reraise exn
     9.9      else
    9.10        (trace_msg ctxt (fn () => "Internal error when " ^ when ^ ":\n" ^ Runtime.exn_message exn);
    9.11         def)
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Mar 03 14:03:06 2016 +0100
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Mar 03 15:23:02 2016 +0100
    10.3 @@ -123,7 +123,7 @@
    10.4            SMT_Solver.smt_filter ctxt goal facts i slice_timeout
    10.5            handle exn =>
    10.6              if Exn.is_interrupt exn orelse debug then
    10.7 -              reraise exn
    10.8 +              Exn.reraise exn
    10.9              else
   10.10                {outcome = SOME (SMT_Failure.Other_Failure (Runtime.exn_message exn)),
   10.11                 fact_ids = NONE, atp_proof = K []}
    11.1 --- a/src/Pure/Concurrent/bash.ML	Thu Mar 03 14:03:06 2016 +0100
    11.2 +++ b/src/Pure/Concurrent/bash.ML	Thu Mar 03 15:23:02 2016 +0100
    11.3 @@ -54,7 +54,7 @@
    11.4                    Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
    11.5            in Synchronized.change result (K res) end
    11.6            handle exn =>
    11.7 -            (Synchronized.change result (fn Wait => Signal | res => res); reraise exn)));
    11.8 +            (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
    11.9  
   11.10      fun read_pid 0 = NONE
   11.11        | read_pid count =
   11.12 @@ -95,7 +95,7 @@
   11.13        val pid = read_pid 1;
   11.14        val _ = cleanup ();
   11.15      in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
   11.16 -    handle exn => (terminate (read_pid 10); cleanup (); reraise exn)
   11.17 +    handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
   11.18    end);
   11.19  
   11.20  end;
    12.1 --- a/src/Pure/Concurrent/bash_windows.ML	Thu Mar 03 14:03:06 2016 +0100
    12.2 +++ b/src/Pure/Concurrent/bash_windows.ML	Thu Mar 03 15:23:02 2016 +0100
    12.3 @@ -48,7 +48,7 @@
    12.4              val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
    12.5            in Synchronized.change result (K res) end
    12.6            handle exn =>
    12.7 -            (Synchronized.change result (fn Wait => Signal | res => res); reraise exn)));
    12.8 +            (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
    12.9  
   12.10      fun read_pid 0 = NONE
   12.11        | read_pid count =
   12.12 @@ -93,7 +93,7 @@
   12.13        val pid = read_pid 1;
   12.14        val _ = cleanup ();
   12.15      in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
   12.16 -    handle exn => (terminate (read_pid 10); cleanup (); reraise exn)
   12.17 +    handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
   12.18    end);
   12.19  
   12.20  end;
    13.1 --- a/src/Pure/Concurrent/future.ML	Thu Mar 03 14:03:06 2016 +0100
    13.2 +++ b/src/Pure/Concurrent/future.ML	Thu Mar 03 15:23:02 2016 +0100
    13.3 @@ -348,7 +348,7 @@
    13.4       (Multithreading.tracing 1 (fn () => "SCHEDULER: Interrupt");
    13.5        List.app cancel_later (cancel_all ());
    13.6        signal work_available; true)
    13.7 -    else reraise exn;
    13.8 +    else Exn.reraise exn;
    13.9  
   13.10  fun scheduler_loop () =
   13.11   (while
   13.12 @@ -409,8 +409,8 @@
   13.13      val _ = Single_Assignment.assign result res
   13.14        handle exn as Fail _ =>
   13.15          (case Single_Assignment.peek result of
   13.16 -          SOME (Exn.Exn e) => reraise (if Exn.is_interrupt e then e else exn)
   13.17 -        | _ => reraise exn);
   13.18 +          SOME (Exn.Exn e) => Exn.reraise (if Exn.is_interrupt e then e else exn)
   13.19 +        | _ => Exn.reraise exn);
   13.20      val ok =
   13.21        (case the (Single_Assignment.peek result) of
   13.22          Exn.Exn exn =>
   13.23 @@ -600,7 +600,7 @@
   13.24          | exn =>
   13.25              if Exn.is_interrupt exn
   13.26              then raise Fail "Concurrent attempt to fulfill promise"
   13.27 -            else reraise exn;
   13.28 +            else Exn.reraise exn;
   13.29      fun job () =
   13.30        Multithreading.with_attributes Multithreading.no_interrupts
   13.31          (fn _ => Exn.release (Exn.capture assign () before abort ()));
    14.1 --- a/src/Pure/Concurrent/par_exn.ML	Thu Mar 03 14:03:06 2016 +0100
    14.2 +++ b/src/Pure/Concurrent/par_exn.ML	Thu Mar 03 15:23:02 2016 +0100
    14.3 @@ -73,7 +73,7 @@
    14.4  fun release_first results =
    14.5    (case get_first plain_exn results of
    14.6      NONE => release_all results
    14.7 -  | SOME exn => reraise exn);
    14.8 +  | SOME exn => Exn.reraise exn);
    14.9  
   14.10  end;
   14.11  
    15.1 --- a/src/Pure/Concurrent/par_list.ML	Thu Mar 03 14:03:06 2016 +0100
    15.2 +++ b/src/Pure/Concurrent/par_list.ML	Thu Mar 03 15:23:02 2016 +0100
    15.3 @@ -46,7 +46,7 @@
    15.4          val results =
    15.5            restore_attributes Future.join_results futures
    15.6              handle exn =>
    15.7 -              (if Exn.is_interrupt exn then Future.cancel_group group else (); reraise exn);
    15.8 +              (if Exn.is_interrupt exn then Future.cancel_group group else (); Exn.reraise exn);
    15.9        in results end) ();
   15.10  
   15.11  fun map_name name f xs = Par_Exn.release_first (managed_results name f xs);
    16.1 --- a/src/Pure/Concurrent/single_assignment.ML	Thu Mar 03 14:03:06 2016 +0100
    16.2 +++ b/src/Pure/Concurrent/single_assignment.ML	Thu Mar 03 15:23:02 2016 +0100
    16.3 @@ -39,7 +39,7 @@
    16.4            NONE =>
    16.5              (case Multithreading.sync_wait NONE NONE cond lock of
    16.6                Exn.Res _ => wait ()
    16.7 -            | Exn.Exn exn => reraise exn)
    16.8 +            | Exn.Exn exn => Exn.reraise exn)
    16.9          | SOME x => x);
   16.10      in wait () end);
   16.11  
    17.1 --- a/src/Pure/Concurrent/standard_thread.ML	Thu Mar 03 14:03:06 2016 +0100
    17.2 +++ b/src/Pure/Concurrent/standard_thread.ML	Thu Mar 03 15:23:02 2016 +0100
    17.3 @@ -54,9 +54,9 @@
    17.4  
    17.5  fun fork (params: params) body =
    17.6    Thread.fork (fn () =>
    17.7 -    print_exception_trace General.exnMessage tracing (fn () =>
    17.8 +    Exn.trace General.exnMessage tracing (fn () =>
    17.9        (set_name (#name params); body ())
   17.10 -        handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
   17.11 +        handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn),
   17.12      attributes params);
   17.13  
   17.14  
    18.1 --- a/src/Pure/Concurrent/synchronized.ML	Thu Mar 03 14:03:06 2016 +0100
    18.2 +++ b/src/Pure/Concurrent/synchronized.ML	Thu Mar 03 15:23:02 2016 +0100
    18.3 @@ -49,7 +49,7 @@
    18.4                (case Multithreading.sync_wait NONE (time_limit x) cond lock of
    18.5                  Exn.Res true => try_change ()
    18.6                | Exn.Res false => NONE
    18.7 -              | Exn.Exn exn => reraise exn)
    18.8 +              | Exn.Exn exn => Exn.reraise exn)
    18.9            | SOME (y, x') =>
   18.10                uninterruptible (fn _ => fn () =>
   18.11                  (var := x'; ConditionVar.broadcast cond; SOME y)) ())
    19.1 --- a/src/Pure/General/basics.ML	Thu Mar 03 14:03:06 2016 +0100
    19.2 +++ b/src/Pure/General/basics.ML	Thu Mar 03 15:23:02 2016 +0100
    19.3 @@ -102,7 +102,7 @@
    19.4  (* partiality *)
    19.5  
    19.6  fun try f x = SOME (f x)
    19.7 -  handle exn => if Exn.is_interrupt exn then reraise exn else NONE;
    19.8 +  handle exn => if Exn.is_interrupt exn then Exn.reraise exn else NONE;
    19.9  
   19.10  fun can f x = is_some (try f x);
   19.11  
    20.1 --- a/src/Pure/Isar/runtime.ML	Thu Mar 03 14:03:06 2016 +0100
    20.2 +++ b/src/Pure/Isar/runtime.ML	Thu Mar 03 15:23:02 2016 +0100
    20.3 @@ -141,8 +141,8 @@
    20.4  
    20.5  val exn_error_message = Output.error_message o exn_message;
    20.6  val exn_system_message = Output.system_message o exn_message;
    20.7 -fun exn_trace e = print_exception_trace exn_message tracing e;
    20.8 -fun exn_trace_system e = print_exception_trace exn_message Output.system_message e;
    20.9 +fun exn_trace e = Exn.trace exn_message tracing e;
   20.10 +fun exn_trace_system e = Exn.trace exn_message Output.system_message e;
   20.11  
   20.12  
   20.13  (* exception debugger *)
   20.14 @@ -189,7 +189,7 @@
   20.15  
   20.16  fun toplevel_error output_exn f x = f x
   20.17    handle exn =>
   20.18 -    if Exn.is_interrupt exn then reraise exn
   20.19 +    if Exn.is_interrupt exn then Exn.reraise exn
   20.20      else
   20.21        let
   20.22          val opt_ctxt =
    21.1 --- a/src/Pure/Isar/toplevel.ML	Thu Mar 03 14:03:06 2016 +0100
    21.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Mar 03 15:23:02 2016 +0100
    21.3 @@ -594,7 +594,7 @@
    21.4    (case transition int tr st of
    21.5      (st', NONE) => st'
    21.6    | (_, SOME (exn, info)) =>
    21.7 -      if Exn.is_interrupt exn then reraise exn
    21.8 +      if Exn.is_interrupt exn then Exn.reraise exn
    21.9        else raise Runtime.EXCURSION_FAIL (exn, info));
   21.10  
   21.11  val command = command_exception false;
    22.1 --- a/src/Pure/ML/ml_compiler.ML	Thu Mar 03 14:03:06 2016 +0100
    22.2 +++ b/src/Pure/ML/ml_compiler.ML	Thu Mar 03 15:23:02 2016 +0100
    22.3 @@ -268,7 +268,7 @@
    22.4        (while not (List.null (! input_buffer)) do
    22.5          PolyML.compiler (get, parameters) ())
    22.6        handle exn =>
    22.7 -        if Exn.is_interrupt exn then reraise exn
    22.8 +        if Exn.is_interrupt exn then Exn.reraise exn
    22.9          else
   22.10            let
   22.11              val exn_msg =
    23.1 --- a/src/Pure/PIDE/command.ML	Thu Mar 03 14:03:06 2016 +0100
    23.2 +++ b/src/Pure/PIDE/command.ML	Thu Mar 03 15:23:02 2016 +0100
    23.3 @@ -195,7 +195,7 @@
    23.4        Outer_Syntax.side_comments span |> maps (fn cmt =>
    23.5          (Thy_Output.output_text st' {markdown = false} (Token.input_of cmt); [])
    23.6            handle exn =>
    23.7 -            if Exn.is_interrupt exn then reraise exn
    23.8 +            if Exn.is_interrupt exn then Exn.reraise exn
    23.9              else Runtime.exn_messages_ids exn)) ();
   23.10  
   23.11  fun report tr m =
   23.12 @@ -277,7 +277,7 @@
   23.13  fun print_error tr opt_context e =
   23.14    (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
   23.15      handle exn =>
   23.16 -      if Exn.is_interrupt exn then reraise exn
   23.17 +      if Exn.is_interrupt exn then Exn.reraise exn
   23.18        else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
   23.19  
   23.20  fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process;
   23.21 @@ -312,7 +312,7 @@
   23.22  
   23.23      fun bad_print name args exn =
   23.24        make_print name args {delay = NONE, pri = 0, persistent = false,
   23.25 -        strict = false, print_fn = fn _ => fn _ => reraise exn};
   23.26 +        strict = false, print_fn = fn _ => fn _ => Exn.reraise exn};
   23.27  
   23.28      fun new_print name args get_pr =
   23.29        let
    24.1 --- a/src/Pure/PIDE/document.ML	Thu Mar 03 14:03:06 2016 +0100
    24.2 +++ b/src/Pure/PIDE/document.ML	Thu Mar 03 15:23:02 2016 +0100
    24.3 @@ -486,7 +486,7 @@
    24.4                            else NONE
    24.5                        | NONE => NONE)) node ()
    24.6                     else ())
    24.7 -                   handle exn => (Output.system_message (Runtime.exn_message exn); reraise exn);
    24.8 +                   handle exn => (Output.system_message (Runtime.exn_message exn); Exn.reraise exn);
    24.9                  val future =
   24.10                    (singleton o Future.forks)
   24.11                     {name = "theory:" ^ name,
    25.1 --- a/src/Pure/PIDE/protocol.ML	Thu Mar 03 14:03:06 2016 +0100
    25.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Mar 03 15:23:02 2016 +0100
    25.3 @@ -120,7 +120,7 @@
    25.4    Isabelle_Process.protocol_command "Document.dialog_result"
    25.5      (fn [serial, result] =>
    25.6        Active.dialog_result (Markup.parse_int serial) result
    25.7 -        handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn);
    25.8 +        handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn);
    25.9  
   25.10  val _ =
   25.11    Isabelle_Process.protocol_command "ML_Heap.share_common_data"
    26.1 --- a/src/Pure/RAW/ROOT_polyml.ML	Thu Mar 03 14:03:06 2016 +0100
    26.2 +++ b/src/Pure/RAW/ROOT_polyml.ML	Thu Mar 03 15:23:02 2016 +0100
    26.3 @@ -15,15 +15,7 @@
    26.4  
    26.5  (* exceptions *)
    26.6  
    26.7 -fun reraise exn =
    26.8 -  (case PolyML.exceptionLocation exn of
    26.9 -    NONE => raise exn
   26.10 -  | SOME location => PolyML.raiseWithLocation (exn, location));
   26.11 -
   26.12 -exception Interrupt = SML90.Interrupt;
   26.13 -
   26.14  use "RAW/exn.ML";
   26.15 -use "RAW/exn_trace.ML";
   26.16  
   26.17  
   26.18  (* multithreading *)
   26.19 @@ -83,16 +75,10 @@
   26.20  (* ML compiler *)
   26.21  
   26.22  use "RAW/secure.ML";
   26.23 -
   26.24 -structure ML_Name_Space =
   26.25 -struct
   26.26 -  open ML_Name_Space;
   26.27 -  val display_val = ML_Pretty.from_polyml o displayVal;
   26.28 -end;
   26.29 -
   26.30  use "RAW/ml_compiler0.ML";
   26.31  
   26.32  PolyML.Compiler.reportUnreferencedIds := true;
   26.33 +PolyML.Compiler.reportExhaustiveHandlers := true;
   26.34  PolyML.Compiler.printInAlphabeticalOrder := false;
   26.35  PolyML.Compiler.maxInlineSize := 80;
   26.36  PolyML.Compiler.prompt1 := "ML> ";
    27.1 --- a/src/Pure/RAW/exn.ML	Thu Mar 03 14:03:06 2016 +0100
    27.2 +++ b/src/Pure/RAW/exn.ML	Thu Mar 03 15:23:02 2016 +0100
    27.3 @@ -14,6 +14,7 @@
    27.4  signature EXN =
    27.5  sig
    27.6    include BASIC_EXN
    27.7 +  val reraise: exn -> 'a
    27.8    datatype 'a result = Res of 'a | Exn of exn
    27.9    val get_res: 'a result -> 'a option
   27.10    val get_exn: 'a result -> exn option
   27.11 @@ -31,11 +32,20 @@
   27.12    val return_code: exn -> int -> int
   27.13    val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
   27.14    exception EXCEPTIONS of exn list
   27.15 +  val trace: (exn -> string) -> (string -> unit) -> (unit -> 'a) -> 'a
   27.16  end;
   27.17  
   27.18  structure Exn: EXN =
   27.19  struct
   27.20  
   27.21 +(* reraise *)
   27.22 +
   27.23 +fun reraise exn =
   27.24 +  (case PolyML.exceptionLocation exn of
   27.25 +    NONE => raise exn
   27.26 +  | SOME location => PolyML.raiseWithLocation (exn, location));
   27.27 +
   27.28 +
   27.29  (* user errors *)
   27.30  
   27.31  exception ERROR of string;
   27.32 @@ -75,7 +85,7 @@
   27.33  
   27.34  (* interrupts *)
   27.35  
   27.36 -exception Interrupt = Interrupt;
   27.37 +exception Interrupt = SML90.Interrupt;
   27.38  
   27.39  fun interrupt () = raise Interrupt;
   27.40  
   27.41 @@ -105,6 +115,17 @@
   27.42  
   27.43  exception EXCEPTIONS of exn list;
   27.44  
   27.45 +
   27.46 +(* low-level trace *)
   27.47 +
   27.48 +fun trace exn_message output e =
   27.49 +  PolyML.Exception.traceException
   27.50 +    (e, fn (trace, exn) =>
   27.51 +      let
   27.52 +        val title = "Exception trace - " ^ exn_message exn;
   27.53 +        val () = output (String.concatWith "\n" (title :: trace));
   27.54 +      in reraise exn end);
   27.55 +
   27.56  end;
   27.57  
   27.58  datatype illegal = Interrupt;
    28.1 --- a/src/Pure/RAW/exn_trace.ML	Thu Mar 03 14:03:06 2016 +0100
    28.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    28.3 @@ -1,15 +0,0 @@
    28.4 -(*  Title:      Pure/RAW/exn_trace.ML
    28.5 -    Author:     Makarius
    28.6 -
    28.7 -Exception trace via ML output, for Poly/ML 5.5.1 or later.
    28.8 -*)
    28.9 -
   28.10 -fun print_exception_trace exn_message output e =
   28.11 -  PolyML.Exception.traceException
   28.12 -    (e, fn (trace, exn) =>
   28.13 -      let
   28.14 -        val title = "Exception trace - " ^ exn_message exn;
   28.15 -        val _ = output (String.concatWith "\n" (title :: trace));
   28.16 -      in reraise exn end);
   28.17 -
   28.18 -PolyML.Compiler.reportExhaustiveHandlers := true;
    29.1 --- a/src/Pure/RAW/ml_compiler0.ML	Thu Mar 03 14:03:06 2016 +0100
    29.2 +++ b/src/Pure/RAW/ml_compiler0.ML	Thu Mar 03 15:23:02 2016 +0100
    29.3 @@ -74,10 +74,10 @@
    29.4        (while not (List.null (! in_buffer)) do
    29.5          PolyML.compiler (get, parameters) ())
    29.6        handle exn =>
    29.7 -        if Exn.is_interrupt exn then reraise exn
    29.8 +        if Exn.is_interrupt exn then Exn.reraise exn
    29.9          else
   29.10           (put ("Exception- " ^ General.exnMessage exn ^ " raised");
   29.11 -          error (output ()); reraise exn);
   29.12 +          error (output ()); Exn.reraise exn);
   29.13    in if verbose then print (output ()) else () end;
   29.14  
   29.15  fun use_file context {verbose, debug} file =
    30.1 --- a/src/Pure/ROOT	Thu Mar 03 14:03:06 2016 +0100
    30.2 +++ b/src/Pure/ROOT	Thu Mar 03 15:23:02 2016 +0100
    30.3 @@ -5,7 +5,6 @@
    30.4    files
    30.5      "RAW/ROOT_polyml.ML"
    30.6      "RAW/exn.ML"
    30.7 -    "RAW/exn_trace.ML"
    30.8      "RAW/fixed_int_dummy.ML"
    30.9      "RAW/ml_compiler0.ML"
   30.10      "RAW/ml_debugger.ML"
   30.11 @@ -23,7 +22,6 @@
   30.12    files
   30.13      "RAW/ROOT_polyml.ML"
   30.14      "RAW/exn.ML"
   30.15 -    "RAW/exn_trace.ML"
   30.16      "RAW/fixed_int_dummy.ML"
   30.17      "RAW/ml_compiler0.ML"
   30.18      "RAW/ml_debugger.ML"
    31.1 --- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 03 14:03:06 2016 +0100
    31.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 03 15:23:02 2016 +0100
    31.3 @@ -310,7 +310,7 @@
    31.4  
    31.5  fun report_result ctxt pos ambig_msgs results =
    31.6    (case (proper_results results, failed_results results) of
    31.7 -    ([], (reports, exn) :: _) => (Context_Position.reports_text ctxt reports; reraise exn)
    31.8 +    ([], (reports, exn) :: _) => (Context_Position.reports_text ctxt reports; Exn.reraise exn)
    31.9    | ([(reports, x)], _) => (Context_Position.reports_text ctxt reports; x)
   31.10    | _ =>
   31.11        if null ambig_msgs then
    32.1 --- a/src/Pure/System/invoke_scala.ML	Thu Mar 03 14:03:06 2016 +0100
    32.2 +++ b/src/Pure/System/invoke_scala.ML	Thu Mar 03 15:23:02 2016 +0100
    32.3 @@ -63,7 +63,7 @@
    32.4    Isabelle_Process.protocol_command "Invoke_Scala.fulfill"
    32.5      (fn [id, tag, res] =>
    32.6        fulfill id tag res
    32.7 -        handle exn => if Exn.is_interrupt exn then () else reraise exn);
    32.8 +        handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn);
    32.9  
   32.10  end;
   32.11  
    33.1 --- a/src/Pure/System/isabelle_process.ML	Thu Mar 03 14:03:06 2016 +0100
    33.2 +++ b/src/Pure/System/isabelle_process.ML	Thu Mar 03 15:23:02 2016 +0100
    33.3 @@ -188,7 +188,7 @@
    33.4  val init = uninterruptible (fn _ => fn socket =>
    33.5    let
    33.6      val _ = SHA1_Samples.test ()
    33.7 -      handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); reraise exn);
    33.8 +      handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
    33.9      val _ = Output.physical_stderr Symbol.STX;
   33.10  
   33.11      val _ = Printer.show_markup_default := true;
    34.1 --- a/src/Pure/Tools/debugger.ML	Thu Mar 03 14:03:06 2016 +0100
    34.2 +++ b/src/Pure/Tools/debugger.ML	Thu Mar 03 15:23:02 2016 +0100
    34.3 @@ -33,7 +33,7 @@
    34.4  
    34.5  fun error_wrapper e = e ()
    34.6    handle exn =>
    34.7 -    if Exn.is_interrupt exn then reraise exn
    34.8 +    if Exn.is_interrupt exn then Exn.reraise exn
    34.9      else error_message (Runtime.exn_message exn);
   34.10  
   34.11  
    35.1 --- a/src/Pure/Tools/simplifier_trace.ML	Thu Mar 03 14:03:06 2016 +0100
    35.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Thu Mar 03 15:23:02 2016 +0100
    35.3 @@ -405,7 +405,7 @@
    35.4          (case result of
    35.5            SOME promise => Future.fulfill promise reply
    35.6          | NONE => ()) (* FIXME handle protocol failure, just like in active.ML (!?) *)
    35.7 -      end handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn)
    35.8 +      end handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn)
    35.9  
   35.10  
   35.11  
    36.1 --- a/src/Pure/morphism.ML	Thu Mar 03 14:03:06 2016 +0100
    36.2 +++ b/src/Pure/morphism.ML	Thu Mar 03 15:23:02 2016 +0100
    36.3 @@ -52,7 +52,8 @@
    36.4  exception MORPHISM of string * exn;
    36.5  
    36.6  fun app (name, f) x = f x
    36.7 -  handle exn => if Exn.is_interrupt exn then reraise exn else raise MORPHISM (name, exn);
    36.8 +  handle exn =>
    36.9 +    if Exn.is_interrupt exn then Exn.reraise exn else raise MORPHISM (name, exn);
   36.10  
   36.11  fun apply fs = fold_rev app fs;
   36.12  
    37.1 --- a/src/Tools/try.ML	Thu Mar 03 14:03:06 2016 +0100
    37.2 +++ b/src/Tools/try.ML	Thu Mar 03 15:23:02 2016 +0100
    37.3 @@ -114,7 +114,7 @@
    37.4                    (true, (_, outcome)) => List.app Output.information outcome
    37.5                  | _ => ())
    37.6                else ()
    37.7 -            end handle exn => if Exn.is_interrupt exn then reraise exn else ()}
    37.8 +            end handle exn => if Exn.is_interrupt exn then Exn.reraise exn else ()}
    37.9        else NONE)
   37.10  
   37.11