clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
authorwenzelm
Thu Mar 27 17:12:40 2014 +0100 (2014-03-27)
changeset 563034cc3f4db3447
parent 56302 c63ab5263008
child 56304 40274e4f5ebf
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
NEWS
src/Doc/IsarImplementation/ML.thy
src/HOL/TPTP/TPTP_Interpret_Test.thy
src/HOL/TPTP/TPTP_Test.thy
src/HOL/Tools/Sledgehammer/async_manager.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/runtime.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML/exn_output.ML
src/Pure/ML/exn_output_polyml.ML
src/Pure/ML/exn_properties_polyml.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_options.ML
src/Pure/PIDE/command.ML
src/Pure/PIDE/execution.ML
src/Pure/PIDE/query_operation.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/command_line.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/isar.ML
src/Tools/WWW_Find/scgi_server.ML
     1.1 --- a/NEWS	Thu Mar 27 13:00:40 2014 +0100
     1.2 +++ b/NEWS	Thu Mar 27 17:12:40 2014 +0100
     1.3 @@ -541,6 +541,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Moved ML_Compiler.exn_trace and other operations on exceptions to
     1.8 +structure Runtime.  Minor INCOMPATIBILITY.
     1.9 +
    1.10  * Discontinued old Toplevel.debug in favour of system option
    1.11  "ML_exception_trace", which may be also declared within the context via
    1.12  "declare [[ML_exception_trace = true]]".  Minor INCOMPATIBILITY.
     2.1 --- a/src/Doc/IsarImplementation/ML.thy	Thu Mar 27 13:00:40 2014 +0100
     2.2 +++ b/src/Doc/IsarImplementation/ML.thy	Thu Mar 27 17:12:40 2014 +0100
     2.3 @@ -1163,7 +1163,7 @@
     2.4    @{index_ML_exception Fail: string} \\
     2.5    @{index_ML Exn.is_interrupt: "exn -> bool"} \\
     2.6    @{index_ML reraise: "exn -> 'a"} \\
     2.7 -  @{index_ML ML_Compiler.exn_trace: "(unit -> 'a) -> 'a"} \\
     2.8 +  @{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\
     2.9    \end{mldecls}
    2.10  
    2.11    \begin{description}
    2.12 @@ -1191,12 +1191,12 @@
    2.13    while preserving its implicit position information (if possible,
    2.14    depending on the ML platform).
    2.15  
    2.16 -  \item @{ML ML_Compiler.exn_trace}~@{ML_text "(fn () =>"}~@{text
    2.17 +  \item @{ML Runtime.exn_trace}~@{ML_text "(fn () =>"}~@{text
    2.18    "e"}@{ML_text ")"} evaluates expression @{text "e"} while printing
    2.19    a full trace of its stack of nested exceptions (if possible,
    2.20    depending on the ML platform).
    2.21  
    2.22 -  Inserting @{ML ML_Compiler.exn_trace} into ML code temporarily is
    2.23 +  Inserting @{ML Runtime.exn_trace} into ML code temporarily is
    2.24    useful for debugging, but not suitable for production code.
    2.25  
    2.26    \end{description}
     3.1 --- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Thu Mar 27 13:00:40 2014 +0100
     3.2 +++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Thu Mar 27 17:12:40 2014 +0100
     3.3 @@ -132,7 +132,7 @@
     3.4            if Exn.is_interrupt exn then reraise exn
     3.5            else
     3.6              (warning (" test: file " ^ Path.print file ^
     3.7 -             " raised exception: " ^ ML_Compiler.exn_message exn);
     3.8 +             " raised exception: " ^ Runtime.exn_message exn);
     3.9               {gc = Time.zeroTime, cpu = Time.zeroTime, elapsed = Time.zeroTime})
    3.10        val to_real = Time.toReal
    3.11        val diff_elapsed =
     4.1 --- a/src/HOL/TPTP/TPTP_Test.thy	Thu Mar 27 13:00:40 2014 +0100
     4.2 +++ b/src/HOL/TPTP/TPTP_Test.thy	Thu Mar 27 17:12:40 2014 +0100
     4.3 @@ -63,7 +63,7 @@
     4.4           reraise exn
     4.5         else
     4.6           (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
     4.7 -          " raised exception: " ^ ML_Compiler.exn_message exn);
     4.8 +          " raised exception: " ^ Runtime.exn_message exn);
     4.9            default_val)
    4.10      end
    4.11  
     5.1 --- a/src/HOL/Tools/Sledgehammer/async_manager.ML	Thu Mar 27 13:00:40 2014 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML	Thu Mar 27 17:12:40 2014 +0100
     5.3 @@ -130,7 +130,7 @@
     5.4  fun check_thread_manager () = Synchronized.change global_state
     5.5    (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
     5.6      if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
     5.7 -    else let val manager = SOME (Toplevel.thread false (fn () =>
     5.8 +    else let val manager = SOME (Runtime.thread false (fn () =>
     5.9        let
    5.10          fun time_limit timeout_heap =
    5.11            (case try Thread_Heap.min timeout_heap of
    5.12 @@ -183,7 +183,7 @@
    5.13  
    5.14  
    5.15  fun thread tool birth_time death_time desc f =
    5.16 -  (Toplevel.thread true
    5.17 +  (Runtime.thread true
    5.18         (fn () =>
    5.19             let
    5.20               val self = Thread.self ()
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Mar 27 13:00:40 2014 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Mar 27 17:12:40 2014 +0100
     6.3 @@ -157,7 +157,7 @@
     6.4                        reraise exn
     6.5                      else
     6.6                        (unknownN, fn () => "Internal error:\n" ^
     6.7 -                                          ML_Compiler.exn_message exn ^ "\n"))
     6.8 +                                          Runtime.exn_message exn ^ "\n"))
     6.9          val _ =
    6.10            (* The "expect" argument is deliberately ignored if the prover is
    6.11               missing so that the "Metis_Examples" can be processed on any
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Mar 27 13:00:40 2014 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Mar 27 17:12:40 2014 +0100
     7.3 @@ -337,7 +337,7 @@
     7.4           else
     7.5             (trace_msg ctxt (fn () =>
     7.6                  "Internal error when " ^ when ^ ":\n" ^
     7.7 -                ML_Compiler.exn_message exn); def)
     7.8 +                Runtime.exn_message exn); def)
     7.9  
    7.10  fun graph_info G =
    7.11    string_of_int (length (Graph.keys G)) ^ " node(s), " ^
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Mar 27 13:00:40 2014 +0100
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Mar 27 17:12:40 2014 +0100
     8.3 @@ -159,7 +159,7 @@
     8.4            |> (fn {outcome, used_facts} => (outcome, used_facts))
     8.5            handle exn =>
     8.6              if Exn.is_interrupt exn then reraise exn
     8.7 -            else (ML_Compiler.exn_message exn |> SMT_Failure.Other_Failure |> SOME, [])
     8.8 +            else (Runtime.exn_message exn |> SMT_Failure.Other_Failure |> SOME, [])
     8.9  
    8.10          val death = Timer.checkRealTimer timer
    8.11          val outcome0 = if is_none outcome0 then SOME outcome else outcome0
     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Mar 27 13:00:40 2014 +0100
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Mar 27 17:12:40 2014 +0100
     9.3 @@ -160,7 +160,7 @@
     9.4              if Exn.is_interrupt exn orelse debug then
     9.5                reraise exn
     9.6              else
     9.7 -              {outcome = SOME (SMT2_Failure.Other_Failure (ML_Compiler.exn_message exn)),
     9.8 +              {outcome = SOME (SMT2_Failure.Other_Failure (Runtime.exn_message exn)),
     9.9                 rewrite_rules = [], conjecture_id = ~1, helper_ids = [], fact_ids = [],
    9.10                 z3_proof = []}
    9.11  
    10.1 --- a/src/Pure/Isar/attrib.ML	Thu Mar 27 13:00:40 2014 +0100
    10.2 +++ b/src/Pure/Isar/attrib.ML	Thu Mar 27 17:12:40 2014 +0100
    10.3 @@ -457,9 +457,9 @@
    10.4    register_config Name_Space.names_long_raw #>
    10.5    register_config Name_Space.names_short_raw #>
    10.6    register_config Name_Space.names_unique_raw #>
    10.7 -  register_config ML_Context.source_trace_raw #>
    10.8 -  register_config ML_Compiler.print_depth_raw #>
    10.9 -  register_config Runtime.exception_trace_raw #>
   10.10 +  register_config ML_Options.source_trace_raw #>
   10.11 +  register_config ML_Options.exception_trace_raw #>
   10.12 +  register_config ML_Options.print_depth_raw #>
   10.13    register_config Proof_Context.show_abbrevs_raw #>
   10.14    register_config Goal_Display.goals_limit_raw #>
   10.15    register_config Goal_Display.show_main_goal_raw #>
    11.1 --- a/src/Pure/Isar/runtime.ML	Thu Mar 27 13:00:40 2014 +0100
    11.2 +++ b/src/Pure/Isar/runtime.ML	Thu Mar 27 17:12:40 2014 +0100
    11.3 @@ -11,16 +11,17 @@
    11.4    exception EXCURSION_FAIL of exn * string
    11.5    exception TOPLEVEL_ERROR
    11.6    val exn_context: Proof.context option -> exn -> exn
    11.7 -  type exn_info = {exn_position: exn -> Position.T, pretty_exn: exn -> Pretty.T}
    11.8    type error = ((serial * string) * string option)
    11.9 -  val exn_messages_ids: exn_info -> exn -> error list
   11.10 -  val exn_messages: exn_info -> exn -> (serial * string) list
   11.11 -  val exn_message: exn_info -> exn -> string
   11.12 -  val exception_trace_raw: Config.raw
   11.13 -  val exception_trace: bool Config.T
   11.14 -  val debugging: (exn -> string) -> Context.generic option -> ('a -> 'b) -> 'a -> 'b
   11.15 -  val controlled_execution: (exn -> string) -> Context.generic option -> ('a -> 'b) -> 'a -> 'b
   11.16 +  val exn_messages_ids: exn -> error list
   11.17 +  val exn_messages: exn -> (serial * string) list
   11.18 +  val exn_message: exn -> string
   11.19 +  val exn_error_message: exn -> unit
   11.20 +  val exn_trace: (unit -> 'a) -> 'a
   11.21 +  val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
   11.22 +  val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
   11.23    val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
   11.24 +  val toplevel_program: (unit -> 'a) -> 'a
   11.25 +  val thread: bool -> (unit -> unit) -> Thread.thread
   11.26  end;
   11.27  
   11.28  structure Runtime: RUNTIME =
   11.29 @@ -44,7 +45,6 @@
   11.30  
   11.31  (* exn_message *)
   11.32  
   11.33 -type exn_info = {exn_position: exn -> Position.T, pretty_exn: exn -> Pretty.T};
   11.34  type error = ((serial * string) * string option);
   11.35  
   11.36  local
   11.37 @@ -75,10 +75,10 @@
   11.38  
   11.39  in
   11.40  
   11.41 -fun exn_messages_ids {exn_position, pretty_exn} e =
   11.42 +fun exn_messages_ids e =
   11.43    let
   11.44      fun raised exn name msgs =
   11.45 -      let val pos = Position.here (exn_position exn) in
   11.46 +      let val pos = Position.here (Exn_Output.position exn) in
   11.47          (case msgs of
   11.48            [] => "exception " ^ name ^ " raised" ^ pos
   11.49          | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
   11.50 @@ -117,7 +117,7 @@
   11.51              | THM (msg, i, thms) =>
   11.52                  raised exn ("THM " ^ string_of_int i)
   11.53                    (msg :: robust_context context Display.string_of_thm thms)
   11.54 -            | _ => raised exn (robust (Pretty.string_of o pretty_exn) exn) []);
   11.55 +            | _ => raised exn (robust (Pretty.string_of o Exn_Output.pretty) exn) []);
   11.56          in [((i, msg), id)] end)
   11.57        and sorted_msgs context exn =
   11.58          sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
   11.59 @@ -126,30 +126,27 @@
   11.60  
   11.61  end;
   11.62  
   11.63 -fun exn_messages exn_info exn = map #1 (exn_messages_ids exn_info exn);
   11.64 +fun exn_messages exn = map #1 (exn_messages_ids exn);
   11.65  
   11.66 -fun exn_message exn_info exn =
   11.67 -  (case exn_messages exn_info exn of
   11.68 +fun exn_message exn =
   11.69 +  (case exn_messages exn of
   11.70      [] => "Interrupt"
   11.71    | msgs => cat_lines (map snd msgs));
   11.72  
   11.73 +val exn_error_message = Output.error_message o exn_message;
   11.74 +fun exn_trace e = print_exception_trace exn_message e;
   11.75 +
   11.76 +
   11.77  
   11.78  (** controlled execution **)
   11.79  
   11.80 -val exception_trace_raw = Config.declare_option "ML_exception_trace";
   11.81 -val exception_trace = Config.bool exception_trace_raw;
   11.82 -
   11.83 -fun exception_trace_enabled NONE =
   11.84 -      (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false)
   11.85 -  | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace;
   11.86 -
   11.87 -fun debugging exn_message opt_context f x =
   11.88 -  if exception_trace_enabled opt_context
   11.89 +fun debugging opt_context f x =
   11.90 +  if ML_Options.exception_trace_enabled opt_context
   11.91    then print_exception_trace exn_message (fn () => f x)
   11.92    else f x;
   11.93  
   11.94 -fun controlled_execution exn_message opt_context f x =
   11.95 -  (f |> debugging exn_message opt_context |> Future.interruptible_task) x;
   11.96 +fun controlled_execution opt_context f x =
   11.97 +  (f |> debugging opt_context |> Future.interruptible_task) x;
   11.98  
   11.99  fun toplevel_error output_exn f x = f x
  11.100    handle exn =>
  11.101 @@ -163,5 +160,17 @@
  11.102          val _ = output_exn (exn_context opt_ctxt exn);
  11.103        in raise TOPLEVEL_ERROR end;
  11.104  
  11.105 +fun toplevel_program body =
  11.106 +  (body |> controlled_execution NONE |> toplevel_error exn_error_message) ();
  11.107 +
  11.108 +(*Proof General legacy*)
  11.109 +fun thread interrupts body =
  11.110 +  Thread.fork
  11.111 +    (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
  11.112 +        |> debugging NONE
  11.113 +        |> toplevel_error
  11.114 +          (fn exn => Output.urgent_message ("## INTERNAL ERROR ##\n" ^ exn_message exn))),
  11.115 +      Simple_Thread.attributes interrupts);
  11.116 +
  11.117  end;
  11.118  
    12.1 --- a/src/Pure/Isar/toplevel.ML	Thu Mar 27 13:00:40 2014 +0100
    12.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Mar 27 17:12:40 2014 +0100
    12.3 @@ -29,10 +29,6 @@
    12.4    val interact: bool Unsynchronized.ref
    12.5    val timing: bool Unsynchronized.ref
    12.6    val profiling: int Unsynchronized.ref
    12.7 -  val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
    12.8 -  val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
    12.9 -  val program: (unit -> 'a) -> 'a
   12.10 -  val thread: bool -> (unit -> unit) -> Thread.thread
   12.11    type transition
   12.12    val empty: transition
   12.13    val print_of: transition -> bool
   12.14 @@ -232,26 +228,6 @@
   12.15  val profiling = Unsynchronized.ref 0;
   12.16  
   12.17  
   12.18 -(* controlled execution *)
   12.19 -
   12.20 -fun debugging arg = Runtime.debugging ML_Compiler.exn_message arg;
   12.21 -fun controlled_execution arg = Runtime.controlled_execution ML_Compiler.exn_message arg;
   12.22 -
   12.23 -fun program body =
   12.24 - (body
   12.25 -  |> controlled_execution NONE
   12.26 -  |> Runtime.toplevel_error ML_Compiler.exn_error_message) ();
   12.27 -
   12.28 -fun thread interrupts body =
   12.29 -  Thread.fork
   12.30 -    (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
   12.31 -        |> debugging NONE
   12.32 -        |> Runtime.toplevel_error
   12.33 -          (fn exn =>
   12.34 -            Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
   12.35 -      Simple_Thread.attributes interrupts);
   12.36 -
   12.37 -
   12.38  (* node transactions -- maintaining stable checkpoints *)
   12.39  
   12.40  exception FAILURE of state * exn;
   12.41 @@ -275,7 +251,7 @@
   12.42  
   12.43      val (result, err) =
   12.44        cont_node
   12.45 -      |> controlled_execution (SOME context) f
   12.46 +      |> Runtime.controlled_execution (SOME context) f
   12.47        |> state_error NONE
   12.48        handle exn => state_error (SOME exn) cont_node;
   12.49    in
   12.50 @@ -304,11 +280,11 @@
   12.51  local
   12.52  
   12.53  fun apply_tr _ (Init f) (State (NONE, _)) =
   12.54 -      State (SOME (Theory (Context.Theory (controlled_execution NONE f ()), NONE)), NONE)
   12.55 +      State (SOME (Theory (Context.Theory (Runtime.controlled_execution NONE f ()), NONE)), NONE)
   12.56    | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
   12.57        exit_transaction state
   12.58    | apply_tr int (Keep f) state =
   12.59 -      controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
   12.60 +      Runtime.controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
   12.61    | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
   12.62        apply_transaction (fn x => f int x) g state
   12.63    | apply_tr _ _ _ = raise UNDEF;
   12.64 @@ -649,8 +625,8 @@
   12.65  fun command_errors int tr st =
   12.66    (case transition int tr st of
   12.67      SOME (st', NONE) => ([], SOME st')
   12.68 -  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE)
   12.69 -  | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE));
   12.70 +  | SOME (_, SOME (exn, _)) => (Runtime.exn_messages_ids exn, NONE)
   12.71 +  | NONE => (Runtime.exn_messages_ids Runtime.TERMINATE, NONE));
   12.72  
   12.73  fun command_exception int tr st =
   12.74    (case transition int tr st of
    13.1 --- a/src/Pure/ML-Systems/polyml.ML	Thu Mar 27 13:00:40 2014 +0100
    13.2 +++ b/src/Pure/ML-Systems/polyml.ML	Thu Mar 27 17:12:40 2014 +0100
    13.3 @@ -175,5 +175,5 @@
    13.4      ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
    13.5  
    13.6  val ml_make_string =
    13.7 -  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Compiler.get_print_depth ())))))";
    13.8 +  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Options.get_print_depth ())))))";
    13.9  
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/Pure/ML/exn_output.ML	Thu Mar 27 17:12:40 2014 +0100
    14.3 @@ -0,0 +1,20 @@
    14.4 +(*  Title:      Pure/ML/exn_output.ML
    14.5 +    Author:     Makarius
    14.6 +
    14.7 +Auxiliary operations for exception output -- generic version.
    14.8 +*)
    14.9 +
   14.10 +signature EXN_OUTPUT =
   14.11 +sig
   14.12 +  val position: exn -> Position.T
   14.13 +  val pretty: exn -> Pretty.T
   14.14 +end
   14.15 +
   14.16 +structure Exn_Output: EXN_OUTPUT =
   14.17 +struct
   14.18 +
   14.19 +fun position (_: exn) = Position.none
   14.20 +val pretty = Pretty.str o General.exnMessage;
   14.21 +
   14.22 +end;
   14.23 +
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/Pure/ML/exn_output_polyml.ML	Thu Mar 27 17:12:40 2014 +0100
    15.3 @@ -0,0 +1,19 @@
    15.4 +(*  Title:      Pure/ML/exn_output_polyml.ML
    15.5 +    Author:     Makarius
    15.6 +
    15.7 +Auxiliary operations for exception output -- Poly/ML version.
    15.8 +*)
    15.9 +
   15.10 +structure Exn_Output: EXN_OUTPUT =
   15.11 +struct
   15.12 +
   15.13 +fun position exn =
   15.14 +  (case PolyML.exceptionLocation exn of
   15.15 +    NONE => Position.none
   15.16 +  | SOME loc => Exn_Properties.position_of loc);
   15.17 +
   15.18 +fun pretty (exn: exn) =
   15.19 +  Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ())));
   15.20 +
   15.21 +end;
   15.22 +
    16.1 --- a/src/Pure/ML/exn_properties_polyml.ML	Thu Mar 27 13:00:40 2014 +0100
    16.2 +++ b/src/Pure/ML/exn_properties_polyml.ML	Thu Mar 27 17:12:40 2014 +0100
    16.3 @@ -6,7 +6,7 @@
    16.4  
    16.5  signature EXN_PROPERTIES =
    16.6  sig
    16.7 -  val of_location: PolyML.location -> Properties.T
    16.8 +  val position_of: PolyML.location -> Position.T
    16.9    val get: exn -> Properties.T
   16.10    val update: Properties.entry list -> exn -> exn
   16.11  end;
   16.12 @@ -14,23 +14,35 @@
   16.13  structure Exn_Properties: EXN_PROPERTIES =
   16.14  struct
   16.15  
   16.16 -fun of_location (loc: PolyML.location) =
   16.17 +(* source locations *)
   16.18 +
   16.19 +fun props_of (loc: PolyML.location) =
   16.20    (case YXML.parse_body (#file loc) of
   16.21      [] => []
   16.22    | [XML.Text file] => [(Markup.fileN, file)]
   16.23    | body => XML.Decode.properties body);
   16.24  
   16.25 +fun position_of loc =
   16.26 +  Position.make
   16.27 +   {line = #startLine loc,
   16.28 +    offset = #startPosition loc,
   16.29 +    end_offset = #endPosition loc,
   16.30 +    props = props_of loc};
   16.31 +
   16.32 +
   16.33 +(* exception properties *)
   16.34 +
   16.35  fun get exn =
   16.36    (case PolyML.exceptionLocation exn of
   16.37      NONE => []
   16.38 -  | SOME loc => of_location loc);
   16.39 +  | SOME loc => props_of loc);
   16.40  
   16.41  fun update entries exn =
   16.42    let
   16.43      val loc =
   16.44        the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
   16.45          (PolyML.exceptionLocation exn);
   16.46 -    val props = of_location loc;
   16.47 +    val props = props_of loc;
   16.48      val props' = fold Properties.put entries props;
   16.49    in
   16.50      if props = props' then exn
    17.1 --- a/src/Pure/ML/ml_compiler.ML	Thu Mar 27 13:00:40 2014 +0100
    17.2 +++ b/src/Pure/ML/ml_compiler.ML	Thu Mar 27 17:12:40 2014 +0100
    17.3 @@ -1,19 +1,11 @@
    17.4  (*  Title:      Pure/ML/ml_compiler.ML
    17.5      Author:     Makarius
    17.6  
    17.7 -Runtime compilation -- generic version.
    17.8 +Runtime compilation and evaluation -- generic version.
    17.9  *)
   17.10  
   17.11  signature ML_COMPILER =
   17.12  sig
   17.13 -  val exn_messages_ids: exn -> Runtime.error list
   17.14 -  val exn_messages: exn -> (serial * string) list
   17.15 -  val exn_message: exn -> string
   17.16 -  val exn_error_message: exn -> unit
   17.17 -  val exn_trace: (unit -> 'a) -> 'a
   17.18 -  val print_depth_raw: Config.raw
   17.19 -  val print_depth: int Config.T
   17.20 -  val get_print_depth: unit -> int
   17.21    type flags = {SML: bool, verbose: bool}
   17.22    val eval: flags -> Position.T -> ML_Lex.token list -> unit
   17.23  end
   17.24 @@ -21,34 +13,6 @@
   17.25  structure ML_Compiler: ML_COMPILER =
   17.26  struct
   17.27  
   17.28 -(* exceptions *)
   17.29 -
   17.30 -val exn_info =
   17.31 - {exn_position = fn _: exn => Position.none,
   17.32 -  pretty_exn = Pretty.str o General.exnMessage};
   17.33 -
   17.34 -val exn_messages_ids = Runtime.exn_messages_ids exn_info;
   17.35 -val exn_messages = Runtime.exn_messages exn_info;
   17.36 -val exn_message = Runtime.exn_message exn_info;
   17.37 -
   17.38 -val exn_error_message = Output.error_message o exn_message;
   17.39 -fun exn_trace e = print_exception_trace exn_message e;
   17.40 -
   17.41 -
   17.42 -(* print depth *)
   17.43 -
   17.44 -val print_depth_raw =
   17.45 -  Config.declare "ML_print_depth" (fn _ => Config.Int (get_default_print_depth ()));
   17.46 -val print_depth = Config.int print_depth_raw;
   17.47 -
   17.48 -fun get_print_depth () =
   17.49 -  (case Context.thread_data () of
   17.50 -    NONE => get_default_print_depth ()
   17.51 -  | SOME context => Config.get_generic context print_depth);
   17.52 -
   17.53 -
   17.54 -(* eval *)
   17.55 -
   17.56  type flags = {SML: bool, verbose: bool};
   17.57  
   17.58  fun eval {SML, verbose} pos toks =
    18.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Mar 27 13:00:40 2014 +0100
    18.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Thu Mar 27 17:12:40 2014 +0100
    18.3 @@ -1,7 +1,7 @@
    18.4  (*  Title:      Pure/ML/ml_compiler_polyml.ML
    18.5      Author:     Makarius
    18.6  
    18.7 -Advanced runtime compilation for Poly/ML.
    18.8 +Runtime compilation and evaluation -- Poly/ML version.
    18.9  *)
   18.10  
   18.11  structure ML_Compiler: ML_COMPILER =
   18.12 @@ -10,40 +10,6 @@
   18.13  open ML_Compiler;
   18.14  
   18.15  
   18.16 -(* source locations *)
   18.17 -
   18.18 -fun position_of (loc: PolyML.location) =
   18.19 -  let
   18.20 -    val {startLine = line, startPosition = offset, endPosition = end_offset, ...} = loc;
   18.21 -    val props = Exn_Properties.of_location loc;
   18.22 -  in
   18.23 -    Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
   18.24 -  end;
   18.25 -
   18.26 -
   18.27 -(* exn_info *)
   18.28 -
   18.29 -fun exn_position exn =
   18.30 -  (case PolyML.exceptionLocation exn of
   18.31 -    NONE => Position.none
   18.32 -  | SOME loc => position_of loc);
   18.33 -
   18.34 -fun pretty_exn (exn: exn) =
   18.35 -  Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, get_print_depth ())));
   18.36 -
   18.37 -val exn_info = {exn_position = exn_position, pretty_exn = pretty_exn};
   18.38 -
   18.39 -
   18.40 -(* exn_message *)
   18.41 -
   18.42 -val exn_messages_ids = Runtime.exn_messages_ids exn_info;
   18.43 -val exn_messages = Runtime.exn_messages exn_info;
   18.44 -val exn_message = Runtime.exn_message exn_info;
   18.45 -
   18.46 -val exn_error_message = Output.error_message o exn_message;
   18.47 -fun exn_trace e = print_exception_trace exn_message e;
   18.48 -
   18.49 -
   18.50  (* parse trees *)
   18.51  
   18.52  fun report_parse_tree depth space =
   18.53 @@ -54,14 +20,15 @@
   18.54        | _ => Position.reported_text);
   18.55  
   18.56      fun reported_entity kind loc decl =
   18.57 -      reported_text (position_of loc)
   18.58 -        (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
   18.59 +      reported_text (Exn_Properties.position_of loc)
   18.60 +        (Markup.entityN,
   18.61 +          (Markup.kindN, kind) :: Position.def_properties_of (Exn_Properties.position_of decl)) "";
   18.62  
   18.63      fun reported loc (PolyML.PTtype types) =
   18.64            cons
   18.65              (PolyML.NameSpace.displayTypeExpression (types, depth, space)
   18.66                |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
   18.67 -              |> reported_text (position_of loc) Markup.ML_typing)
   18.68 +              |> reported_text (Exn_Properties.position_of loc) Markup.ML_typing)
   18.69        | reported loc (PolyML.PTdeclaredAt decl) =
   18.70            cons (reported_entity Markup.ML_defN loc decl)
   18.71        | reported loc (PolyML.PTopenedAt decl) =
   18.72 @@ -122,7 +89,7 @@
   18.73  
   18.74      fun message {message = msg, hard, location = loc, context = _} =
   18.75        let
   18.76 -        val pos = position_of loc;
   18.77 +        val pos = Exn_Properties.position_of loc;
   18.78          val txt =
   18.79            (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
   18.80            Pretty.string_of (Pretty.from_ML (pretty_ml msg));
   18.81 @@ -131,7 +98,7 @@
   18.82  
   18.83      (* results *)
   18.84  
   18.85 -    val depth = get_print_depth ();
   18.86 +    val depth = ML_Options.get_print_depth ();
   18.87  
   18.88      fun apply_result {fixes, types, signatures, structures, functors, values} =
   18.89        let
   18.90 @@ -172,8 +139,8 @@
   18.91        | SOME code =>
   18.92            apply_result
   18.93              ((code
   18.94 -              |> Runtime.debugging exn_message opt_context
   18.95 -              |> Runtime.toplevel_error (err o exn_message)) ())));
   18.96 +              |> Runtime.debugging opt_context
   18.97 +              |> Runtime.toplevel_error (err o Runtime.exn_message)) ())));
   18.98  
   18.99  
  18.100      (* compiler invocation *)
  18.101 @@ -185,7 +152,7 @@
  18.102        PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
  18.103        PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
  18.104        PolyML.Compiler.CPFileName location_props,
  18.105 -      PolyML.Compiler.CPPrintDepth get_print_depth,
  18.106 +      PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
  18.107        PolyML.Compiler.CPCompilerResultFun result_fun,
  18.108        PolyML.Compiler.CPPrintInAlphabeticalOrder false];
  18.109      val _ =
  18.110 @@ -199,7 +166,7 @@
  18.111                (case exn of
  18.112                  STATIC_ERRORS () => ""
  18.113                | Runtime.TOPLEVEL_ERROR => ""
  18.114 -              | _ => "Exception- " ^ Pretty.string_of (pretty_exn exn) ^ " raised");
  18.115 +              | _ => "Exception- " ^ Pretty.string_of (Exn_Output.pretty exn) ^ " raised");
  18.116              val _ = output_warnings ();
  18.117              val _ = output_writeln ();
  18.118            in raise_error exn_msg end;
    19.1 --- a/src/Pure/ML/ml_context.ML	Thu Mar 27 13:00:40 2014 +0100
    19.2 +++ b/src/Pure/ML/ml_context.ML	Thu Mar 27 17:12:40 2014 +0100
    19.3 @@ -17,8 +17,6 @@
    19.4    val add_antiquotation: binding -> (Args.src -> Proof.context -> decl * Proof.context) ->
    19.5      theory -> theory
    19.6    val print_antiquotations: Proof.context -> unit
    19.7 -  val source_trace_raw: Config.raw
    19.8 -  val source_trace: bool Config.T
    19.9    val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
   19.10      Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
   19.11    val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
   19.12 @@ -137,9 +135,6 @@
   19.13          in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
   19.14    in ((ml_env @ end_env, ml_body), opt_ctxt') end;
   19.15  
   19.16 -val source_trace_raw = Config.declare "ML_source_trace" (fn _ => Config.Bool false);
   19.17 -val source_trace = Config.bool source_trace_raw;
   19.18 -
   19.19  fun eval flags pos ants =
   19.20    let
   19.21      val non_verbose = {SML = #SML flags, verbose = false};
   19.22 @@ -149,7 +144,7 @@
   19.23      val _ =
   19.24        (case Option.map Context.proof_of env_ctxt of
   19.25          SOME ctxt =>
   19.26 -          if Config.get ctxt source_trace andalso Context_Position.is_visible ctxt
   19.27 +          if Config.get ctxt ML_Options.source_trace andalso Context_Position.is_visible ctxt
   19.28            then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
   19.29            else ()
   19.30        | NONE => ());
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/Pure/ML/ml_options.ML	Thu Mar 27 17:12:40 2014 +0100
    20.3 @@ -0,0 +1,49 @@
    20.4 +(*  Title:      Pure/ML/ml_options.ML
    20.5 +    Author:     Makarius
    20.6 +
    20.7 +ML configuration options.
    20.8 +*)
    20.9 +
   20.10 +signature ML_OPTIONS =
   20.11 +sig
   20.12 +  val source_trace_raw: Config.raw
   20.13 +  val source_trace: bool Config.T
   20.14 +  val exception_trace_raw: Config.raw
   20.15 +  val exception_trace: bool Config.T
   20.16 +  val exception_trace_enabled: Context.generic option -> bool
   20.17 +  val print_depth_raw: Config.raw
   20.18 +  val print_depth: int Config.T
   20.19 +  val get_print_depth: unit -> int
   20.20 +end;
   20.21 +
   20.22 +structure ML_Options: ML_OPTIONS =
   20.23 +struct
   20.24 +
   20.25 +(* source trace *)
   20.26 +
   20.27 +val source_trace_raw = Config.declare "ML_source_trace" (fn _ => Config.Bool false);
   20.28 +val source_trace = Config.bool source_trace_raw;
   20.29 +
   20.30 +
   20.31 +(* exception trace *)
   20.32 +
   20.33 +val exception_trace_raw = Config.declare_option "ML_exception_trace";
   20.34 +val exception_trace = Config.bool exception_trace_raw;
   20.35 +
   20.36 +fun exception_trace_enabled NONE =
   20.37 +      (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false)
   20.38 +  | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace;
   20.39 +
   20.40 +
   20.41 +(* print depth *)
   20.42 +
   20.43 +val print_depth_raw =
   20.44 +  Config.declare "ML_print_depth" (fn _ => Config.Int (get_default_print_depth ()));
   20.45 +val print_depth = Config.int print_depth_raw;
   20.46 +
   20.47 +fun get_print_depth () =
   20.48 +  (case Context.thread_data () of
   20.49 +    NONE => get_default_print_depth ()
   20.50 +  | SOME context => Config.get_generic context print_depth);
   20.51 +
   20.52 +end;
    21.1 --- a/src/Pure/PIDE/command.ML	Thu Mar 27 13:00:40 2014 +0100
    21.2 +++ b/src/Pure/PIDE/command.ML	Thu Mar 27 17:12:40 2014 +0100
    21.3 @@ -196,7 +196,7 @@
    21.4          (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
    21.5            handle exn =>
    21.6              if Exn.is_interrupt exn then reraise exn
    21.7 -            else ML_Compiler.exn_messages_ids exn)) ();
    21.8 +            else Runtime.exn_messages_ids exn)) ();
    21.9  
   21.10  fun report tr m =
   21.11    Toplevel.setmp_thread_position tr (fn () => Output.report (Markup.markup_only m)) ();
   21.12 @@ -276,10 +276,10 @@
   21.13    Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
   21.14  
   21.15  fun print_error tr opt_context e =
   21.16 -  (Toplevel.setmp_thread_position tr o Toplevel.controlled_execution opt_context) e ()
   21.17 +  (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
   21.18      handle exn =>
   21.19        if Exn.is_interrupt exn then reraise exn
   21.20 -      else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
   21.21 +      else List.app (Future.error_msg (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
   21.22  
   21.23  fun print_finished (Print {print_process, ...}) = memo_finished print_process;
   21.24  
   21.25 @@ -319,7 +319,7 @@
   21.26        let
   21.27          val params = {command_name = command_name, args = args, exec_id = eval_exec_id eval};
   21.28        in
   21.29 -        (case Exn.capture (Toplevel.controlled_execution NONE get_pr) params of
   21.30 +        (case Exn.capture (Runtime.controlled_execution NONE get_pr) params of
   21.31            Exn.Res NONE => NONE
   21.32          | Exn.Res (SOME pr) => SOME (make_print name args pr)
   21.33          | Exn.Exn exn => SOME (bad_print name args exn))
    22.1 --- a/src/Pure/PIDE/execution.ML	Thu Mar 27 13:00:40 2014 +0100
    22.2 +++ b/src/Pure/PIDE/execution.ML	Thu Mar 27 17:12:40 2014 +0100
    22.3 @@ -125,7 +125,7 @@
    22.4                      status task [Markup.finished];
    22.5                      Output.report (Markup.markup_only Markup.bad);
    22.6                      if exec_id = 0 then ()
    22.7 -                    else List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn))
    22.8 +                    else List.app (Future.error_msg pos) (Runtime.exn_messages_ids exn))
    22.9                  | Exn.Res _ =>
   22.10                      status task [Markup.finished])
   22.11              in Exn.release result end);
    23.1 --- a/src/Pure/PIDE/query_operation.ML	Thu Mar 27 13:00:40 2014 +0100
    23.2 +++ b/src/Pure/PIDE/query_operation.ML	Thu Mar 27 17:12:40 2014 +0100
    23.3 @@ -24,7 +24,7 @@
    23.4                fun status m = result (Markup.markup_only m);
    23.5                fun output_result s = result (Markup.markup (Markup.writelnN, []) s);
    23.6                fun toplevel_error exn =
    23.7 -                result (Markup.markup (Markup.errorN, []) (ML_Compiler.exn_message exn));
    23.8 +                result (Markup.markup (Markup.errorN, []) (Runtime.exn_message exn));
    23.9  
   23.10                val _ = status Markup.running;
   23.11                fun run () = f {state = state, args = args, output_result = output_result};
    24.1 --- a/src/Pure/ROOT	Thu Mar 27 13:00:40 2014 +0100
    24.2 +++ b/src/Pure/ROOT	Thu Mar 27 17:12:40 2014 +0100
    24.3 @@ -139,6 +139,8 @@
    24.4      "Isar/token.ML"
    24.5      "Isar/toplevel.ML"
    24.6      "Isar/typedecl.ML"
    24.7 +    "ML/exn_output.ML"
    24.8 +    "ML/exn_output_polyml.ML"
    24.9      "ML/exn_properties_dummy.ML"
   24.10      "ML/exn_properties_polyml.ML"
   24.11      "ML/exn_trace_polyml-5.5.1.ML"
   24.12 @@ -150,6 +152,7 @@
   24.13      "ML/ml_env.ML"
   24.14      "ML/ml_lex.ML"
   24.15      "ML/ml_parse.ML"
   24.16 +    "ML/ml_options.ML"
   24.17      "ML/ml_statistics_dummy.ML"
   24.18      "ML/ml_statistics_polyml-5.5.0.ML"
   24.19      "ML/ml_syntax.ML"
    25.1 --- a/src/Pure/ROOT.ML	Thu Mar 27 13:00:40 2014 +0100
    25.2 +++ b/src/Pure/ROOT.ML	Thu Mar 27 17:12:40 2014 +0100
    25.3 @@ -69,6 +69,7 @@
    25.4  
    25.5  use "PIDE/xml.ML";
    25.6  use "PIDE/yxml.ML";
    25.7 +use "PIDE/document_id.ML";
    25.8  
    25.9  use "General/change_table.ML";
   25.10  use "General/graph.ML";
   25.11 @@ -193,16 +194,18 @@
   25.12  
   25.13  (* Isar -- Intelligible Semi-Automated Reasoning *)
   25.14  
   25.15 -(*ML support*)
   25.16 +(*ML support and global execution*)
   25.17  use "ML/ml_syntax.ML";
   25.18  use "ML/ml_env.ML";
   25.19 +use "ML/ml_options.ML";
   25.20 +use "ML/exn_output.ML";
   25.21 +if ML_System.is_polyml then use "ML/exn_output_polyml.ML" else ();
   25.22 +use "ML/ml_options.ML";
   25.23  use "Isar/runtime.ML";
   25.24 +use "PIDE/execution.ML";
   25.25  use "ML/ml_compiler.ML";
   25.26  if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
   25.27  
   25.28 -(*global execution*)
   25.29 -use "PIDE/document_id.ML";
   25.30 -use "PIDE/execution.ML";
   25.31  use "skip_proof.ML";
   25.32  use "goal.ML";
   25.33  
   25.34 @@ -346,7 +349,7 @@
   25.35  (* the Pure theory *)
   25.36  
   25.37  use "pure_syn.ML";
   25.38 -Toplevel.program (fn () => Thy_Info.use_thy ("Pure", Position.none));
   25.39 +Runtime.toplevel_program (fn () => Thy_Info.use_thy ("Pure", Position.none));
   25.40  Context.set_thread_data NONE;
   25.41  structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
   25.42  
   25.43 @@ -355,7 +358,8 @@
   25.44  
   25.45  (* ML toplevel commands *)
   25.46  
   25.47 -fun use_thys args = Toplevel.program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
   25.48 +fun use_thys args =
   25.49 +  Runtime.toplevel_program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
   25.50  val use_thy = use_thys o single;
   25.51  
   25.52  val cd = File.cd o Path.explode;
    26.1 --- a/src/Pure/System/command_line.ML	Thu Mar 27 13:00:40 2014 +0100
    26.2 +++ b/src/Pure/System/command_line.ML	Thu Mar 27 17:12:40 2014 +0100
    26.3 @@ -19,7 +19,7 @@
    26.4        restore_attributes body () handle exn =>
    26.5          let
    26.6            val _ =
    26.7 -            ML_Compiler.exn_error_message exn
    26.8 +            Runtime.exn_error_message exn
    26.9                handle _ => Output.error_message "Exception raised, but failed to print details!";
   26.10          in if Exn.is_interrupt exn then 130 else 1 end;
   26.11      in if rc = 0 then () else exit rc end) ();
    27.1 --- a/src/Pure/System/isabelle_process.ML	Thu Mar 27 13:00:40 2014 +0100
    27.2 +++ b/src/Pure/System/isabelle_process.ML	Thu Mar 27 17:12:40 2014 +0100
    27.3 @@ -48,9 +48,9 @@
    27.4    (case Symtab.lookup (Synchronized.value commands) name of
    27.5      NONE => error ("Undefined Isabelle protocol command " ^ quote name)
    27.6    | SOME cmd =>
    27.7 -      (Toplevel.debugging NONE cmd args handle exn =>
    27.8 +      (Runtime.debugging NONE cmd args handle exn =>
    27.9          error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^
   27.10 -          ML_Compiler.exn_message exn)));
   27.11 +          Runtime.exn_message exn)));
   27.12  
   27.13  end;
   27.14  
   27.15 @@ -170,7 +170,7 @@
   27.16        [] => (Output.error_message "Isabelle process: no input"; true)
   27.17      | name :: args => (task_context (fn () => run_command name args); true))
   27.18      handle Runtime.TERMINATE => false
   27.19 -      | exn => (ML_Compiler.exn_error_message exn handle crash => recover crash; true);
   27.20 +      | exn => (Runtime.exn_error_message exn handle crash => recover crash; true);
   27.21    in
   27.22      if continue then loop channel
   27.23      else (Future.shutdown (); Execution.reset (); ())
    28.1 --- a/src/Pure/System/isar.ML	Thu Mar 27 13:00:40 2014 +0100
    28.2 +++ b/src/Pure/System/isar.ML	Thu Mar 27 17:12:40 2014 +0100
    28.3 @@ -97,7 +97,7 @@
    28.4    | SOME (_, SOME exn_info) =>
    28.5       (set_exn (SOME exn_info);
    28.6        Toplevel.setmp_thread_position tr
    28.7 -        ML_Compiler.exn_error_message (Runtime.EXCURSION_FAIL exn_info);
    28.8 +        Runtime.exn_error_message (Runtime.EXCURSION_FAIL exn_info);
    28.9        true)
   28.10    | SOME (st', NONE) =>
   28.11        let
   28.12 @@ -144,7 +144,7 @@
   28.13        NONE => if secure then quit () else ()
   28.14      | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
   28.15      handle exn =>
   28.16 -      (ML_Compiler.exn_error_message exn
   28.17 +      (Runtime.exn_error_message exn
   28.18          handle crash =>
   28.19            (Synchronized.change crashes (cons crash);
   28.20              warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
    29.1 --- a/src/Tools/WWW_Find/scgi_server.ML	Thu Mar 27 13:00:40 2014 +0100
    29.2 +++ b/src/Tools/WWW_Find/scgi_server.ML	Thu Mar 27 17:12:40 2014 +0100
    29.3 @@ -53,7 +53,7 @@
    29.4               ConditionVar.wait (thread_wait, thread_wait_mutex));
    29.5         add_thread
    29.6           (Thread.fork   (* FIXME avoid low-level Poly/ML thread primitives *)
    29.7 -            (fn () => ML_Compiler.exn_trace threadf,
    29.8 +            (fn () => Runtime.exn_trace threadf,
    29.9               [Thread.EnableBroadcastInterrupt true,
   29.10                Thread.InterruptState
   29.11                Thread.InterruptAsynchOnce])))