# HG changeset patch
# User wenzelm
# Date 1395936760 -3600
# Node ID 4cc3f4db3447fc9f50ce194e00e7a12bbc08b64e
# Parent  c63ab52630086d9d118c3abd0e2bd3348fb2e200
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;

diff -r c63ab5263008 -r 4cc3f4db3447 NEWS
--- a/NEWS	Thu Mar 27 13:00:40 2014 +0100
+++ b/NEWS	Thu Mar 27 17:12:40 2014 +0100
@@ -541,6 +541,9 @@
 
 *** ML ***
 
+* Moved ML_Compiler.exn_trace and other operations on exceptions to
+structure Runtime.  Minor INCOMPATIBILITY.
+
 * Discontinued old Toplevel.debug in favour of system option
 "ML_exception_trace", which may be also declared within the context via
 "declare [[ML_exception_trace = true]]".  Minor INCOMPATIBILITY.
diff -r c63ab5263008 -r 4cc3f4db3447 src/Doc/IsarImplementation/ML.thy
--- a/src/Doc/IsarImplementation/ML.thy	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Doc/IsarImplementation/ML.thy	Thu Mar 27 17:12:40 2014 +0100
@@ -1163,7 +1163,7 @@
   @{index_ML_exception Fail: string} \\
   @{index_ML Exn.is_interrupt: "exn -> bool"} \\
   @{index_ML reraise: "exn -> 'a"} \\
-  @{index_ML ML_Compiler.exn_trace: "(unit -> 'a) -> 'a"} \\
+  @{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\
   \end{mldecls}
 
   \begin{description}
@@ -1191,12 +1191,12 @@
   while preserving its implicit position information (if possible,
   depending on the ML platform).
 
-  \item @{ML ML_Compiler.exn_trace}~@{ML_text "(fn () =>"}~@{text
+  \item @{ML Runtime.exn_trace}~@{ML_text "(fn () =>"}~@{text
   "e"}@{ML_text ")"} evaluates expression @{text "e"} while printing
   a full trace of its stack of nested exceptions (if possible,
   depending on the ML platform).
 
-  Inserting @{ML ML_Compiler.exn_trace} into ML code temporarily is
+  Inserting @{ML Runtime.exn_trace} into ML code temporarily is
   useful for debugging, but not suitable for production code.
 
   \end{description}
diff -r c63ab5263008 -r 4cc3f4db3447 src/HOL/TPTP/TPTP_Interpret_Test.thy
--- a/src/HOL/TPTP/TPTP_Interpret_Test.thy	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Interpret_Test.thy	Thu Mar 27 17:12:40 2014 +0100
@@ -132,7 +132,7 @@
           if Exn.is_interrupt exn then reraise exn
           else
             (warning (" test: file " ^ Path.print file ^
-             " raised exception: " ^ ML_Compiler.exn_message exn);
+             " raised exception: " ^ Runtime.exn_message exn);
              {gc = Time.zeroTime, cpu = Time.zeroTime, elapsed = Time.zeroTime})
       val to_real = Time.toReal
       val diff_elapsed =
diff -r c63ab5263008 -r 4cc3f4db3447 src/HOL/TPTP/TPTP_Test.thy
--- a/src/HOL/TPTP/TPTP_Test.thy	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Test.thy	Thu Mar 27 17:12:40 2014 +0100
@@ -63,7 +63,7 @@
          reraise exn
        else
          (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
-          " raised exception: " ^ ML_Compiler.exn_message exn);
+          " raised exception: " ^ Runtime.exn_message exn);
           default_val)
     end
 
diff -r c63ab5263008 -r 4cc3f4db3447 src/HOL/Tools/Sledgehammer/async_manager.ML
--- a/src/HOL/Tools/Sledgehammer/async_manager.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -130,7 +130,7 @@
 fun check_thread_manager () = Synchronized.change global_state
   (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
     if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
-    else let val manager = SOME (Toplevel.thread false (fn () =>
+    else let val manager = SOME (Runtime.thread false (fn () =>
       let
         fun time_limit timeout_heap =
           (case try Thread_Heap.min timeout_heap of
@@ -183,7 +183,7 @@
 
 
 fun thread tool birth_time death_time desc f =
-  (Toplevel.thread true
+  (Runtime.thread true
        (fn () =>
            let
              val self = Thread.self ()
diff -r c63ab5263008 -r 4cc3f4db3447 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -157,7 +157,7 @@
                       reraise exn
                     else
                       (unknownN, fn () => "Internal error:\n" ^
-                                          ML_Compiler.exn_message exn ^ "\n"))
+                                          Runtime.exn_message exn ^ "\n"))
         val _ =
           (* The "expect" argument is deliberately ignored if the prover is
              missing so that the "Metis_Examples" can be processed on any
diff -r c63ab5263008 -r 4cc3f4db3447 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -337,7 +337,7 @@
          else
            (trace_msg ctxt (fn () =>
                 "Internal error when " ^ when ^ ":\n" ^
-                ML_Compiler.exn_message exn); def)
+                Runtime.exn_message exn); def)
 
 fun graph_info G =
   string_of_int (length (Graph.keys G)) ^ " node(s), " ^
diff -r c63ab5263008 -r 4cc3f4db3447 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -159,7 +159,7 @@
           |> (fn {outcome, used_facts} => (outcome, used_facts))
           handle exn =>
             if Exn.is_interrupt exn then reraise exn
-            else (ML_Compiler.exn_message exn |> SMT_Failure.Other_Failure |> SOME, [])
+            else (Runtime.exn_message exn |> SMT_Failure.Other_Failure |> SOME, [])
 
         val death = Timer.checkRealTimer timer
         val outcome0 = if is_none outcome0 then SOME outcome else outcome0
diff -r c63ab5263008 -r 4cc3f4db3447 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -160,7 +160,7 @@
             if Exn.is_interrupt exn orelse debug then
               reraise exn
             else
-              {outcome = SOME (SMT2_Failure.Other_Failure (ML_Compiler.exn_message exn)),
+              {outcome = SOME (SMT2_Failure.Other_Failure (Runtime.exn_message exn)),
                rewrite_rules = [], conjecture_id = ~1, helper_ids = [], fact_ids = [],
                z3_proof = []}
 
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -457,9 +457,9 @@
   register_config Name_Space.names_long_raw #>
   register_config Name_Space.names_short_raw #>
   register_config Name_Space.names_unique_raw #>
-  register_config ML_Context.source_trace_raw #>
-  register_config ML_Compiler.print_depth_raw #>
-  register_config Runtime.exception_trace_raw #>
+  register_config ML_Options.source_trace_raw #>
+  register_config ML_Options.exception_trace_raw #>
+  register_config ML_Options.print_depth_raw #>
   register_config Proof_Context.show_abbrevs_raw #>
   register_config Goal_Display.goals_limit_raw #>
   register_config Goal_Display.show_main_goal_raw #>
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/Isar/runtime.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -11,16 +11,17 @@
   exception EXCURSION_FAIL of exn * string
   exception TOPLEVEL_ERROR
   val exn_context: Proof.context option -> exn -> exn
-  type exn_info = {exn_position: exn -> Position.T, pretty_exn: exn -> Pretty.T}
   type error = ((serial * string) * string option)
-  val exn_messages_ids: exn_info -> exn -> error list
-  val exn_messages: exn_info -> exn -> (serial * string) list
-  val exn_message: exn_info -> exn -> string
-  val exception_trace_raw: Config.raw
-  val exception_trace: bool Config.T
-  val debugging: (exn -> string) -> Context.generic option -> ('a -> 'b) -> 'a -> 'b
-  val controlled_execution: (exn -> string) -> Context.generic option -> ('a -> 'b) -> 'a -> 'b
+  val exn_messages_ids: exn -> error list
+  val exn_messages: exn -> (serial * string) list
+  val exn_message: exn -> string
+  val exn_error_message: exn -> unit
+  val exn_trace: (unit -> 'a) -> 'a
+  val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
+  val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
   val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
+  val toplevel_program: (unit -> 'a) -> 'a
+  val thread: bool -> (unit -> unit) -> Thread.thread
 end;
 
 structure Runtime: RUNTIME =
@@ -44,7 +45,6 @@
 
 (* exn_message *)
 
-type exn_info = {exn_position: exn -> Position.T, pretty_exn: exn -> Pretty.T};
 type error = ((serial * string) * string option);
 
 local
@@ -75,10 +75,10 @@
 
 in
 
-fun exn_messages_ids {exn_position, pretty_exn} e =
+fun exn_messages_ids e =
   let
     fun raised exn name msgs =
-      let val pos = Position.here (exn_position exn) in
+      let val pos = Position.here (Exn_Output.position exn) in
         (case msgs of
           [] => "exception " ^ name ^ " raised" ^ pos
         | [msg] => "exception " ^ name ^ " raised" ^ pos ^ ": " ^ msg
@@ -117,7 +117,7 @@
             | THM (msg, i, thms) =>
                 raised exn ("THM " ^ string_of_int i)
                   (msg :: robust_context context Display.string_of_thm thms)
-            | _ => raised exn (robust (Pretty.string_of o pretty_exn) exn) []);
+            | _ => raised exn (robust (Pretty.string_of o Exn_Output.pretty) exn) []);
         in [((i, msg), id)] end)
       and sorted_msgs context exn =
         sort_distinct (int_ord o pairself (fst o fst)) (maps exn_msgs (flatten context exn));
@@ -126,30 +126,27 @@
 
 end;
 
-fun exn_messages exn_info exn = map #1 (exn_messages_ids exn_info exn);
+fun exn_messages exn = map #1 (exn_messages_ids exn);
 
-fun exn_message exn_info exn =
-  (case exn_messages exn_info exn of
+fun exn_message exn =
+  (case exn_messages exn of
     [] => "Interrupt"
   | msgs => cat_lines (map snd msgs));
 
+val exn_error_message = Output.error_message o exn_message;
+fun exn_trace e = print_exception_trace exn_message e;
+
+
 
 (** controlled execution **)
 
-val exception_trace_raw = Config.declare_option "ML_exception_trace";
-val exception_trace = Config.bool exception_trace_raw;
-
-fun exception_trace_enabled NONE =
-      (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false)
-  | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace;
-
-fun debugging exn_message opt_context f x =
-  if exception_trace_enabled opt_context
+fun debugging opt_context f x =
+  if ML_Options.exception_trace_enabled opt_context
   then print_exception_trace exn_message (fn () => f x)
   else f x;
 
-fun controlled_execution exn_message opt_context f x =
-  (f |> debugging exn_message opt_context |> Future.interruptible_task) x;
+fun controlled_execution opt_context f x =
+  (f |> debugging opt_context |> Future.interruptible_task) x;
 
 fun toplevel_error output_exn f x = f x
   handle exn =>
@@ -163,5 +160,17 @@
         val _ = output_exn (exn_context opt_ctxt exn);
       in raise TOPLEVEL_ERROR end;
 
+fun toplevel_program body =
+  (body |> controlled_execution NONE |> toplevel_error exn_error_message) ();
+
+(*Proof General legacy*)
+fun thread interrupts body =
+  Thread.fork
+    (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
+        |> debugging NONE
+        |> toplevel_error
+          (fn exn => Output.urgent_message ("## INTERNAL ERROR ##\n" ^ exn_message exn))),
+      Simple_Thread.attributes interrupts);
+
 end;
 
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -29,10 +29,6 @@
   val interact: bool Unsynchronized.ref
   val timing: bool Unsynchronized.ref
   val profiling: int Unsynchronized.ref
-  val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
-  val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
-  val program: (unit -> 'a) -> 'a
-  val thread: bool -> (unit -> unit) -> Thread.thread
   type transition
   val empty: transition
   val print_of: transition -> bool
@@ -232,26 +228,6 @@
 val profiling = Unsynchronized.ref 0;
 
 
-(* controlled execution *)
-
-fun debugging arg = Runtime.debugging ML_Compiler.exn_message arg;
-fun controlled_execution arg = Runtime.controlled_execution ML_Compiler.exn_message arg;
-
-fun program body =
- (body
-  |> controlled_execution NONE
-  |> Runtime.toplevel_error ML_Compiler.exn_error_message) ();
-
-fun thread interrupts body =
-  Thread.fork
-    (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
-        |> debugging NONE
-        |> Runtime.toplevel_error
-          (fn exn =>
-            Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
-      Simple_Thread.attributes interrupts);
-
-
 (* node transactions -- maintaining stable checkpoints *)
 
 exception FAILURE of state * exn;
@@ -275,7 +251,7 @@
 
     val (result, err) =
       cont_node
-      |> controlled_execution (SOME context) f
+      |> Runtime.controlled_execution (SOME context) f
       |> state_error NONE
       handle exn => state_error (SOME exn) cont_node;
   in
@@ -304,11 +280,11 @@
 local
 
 fun apply_tr _ (Init f) (State (NONE, _)) =
-      State (SOME (Theory (Context.Theory (controlled_execution NONE f ()), NONE)), NONE)
+      State (SOME (Theory (Context.Theory (Runtime.controlled_execution NONE f ()), NONE)), NONE)
   | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
       exit_transaction state
   | apply_tr int (Keep f) state =
-      controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
+      Runtime.controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
   | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
       apply_transaction (fn x => f int x) g state
   | apply_tr _ _ _ = raise UNDEF;
@@ -649,8 +625,8 @@
 fun command_errors int tr st =
   (case transition int tr st of
     SOME (st', NONE) => ([], SOME st')
-  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE)
-  | NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE));
+  | SOME (_, SOME (exn, _)) => (Runtime.exn_messages_ids exn, NONE)
+  | NONE => (Runtime.exn_messages_ids Runtime.TERMINATE, NONE));
 
 fun command_exception int tr st =
   (case transition int tr st of
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -175,5 +175,5 @@
     ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
 
 val ml_make_string =
-  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Compiler.get_print_depth ())))))";
+  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Options.get_print_depth ())))))";
 
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/ML/exn_output.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/exn_output.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -0,0 +1,20 @@
+(*  Title:      Pure/ML/exn_output.ML
+    Author:     Makarius
+
+Auxiliary operations for exception output -- generic version.
+*)
+
+signature EXN_OUTPUT =
+sig
+  val position: exn -> Position.T
+  val pretty: exn -> Pretty.T
+end
+
+structure Exn_Output: EXN_OUTPUT =
+struct
+
+fun position (_: exn) = Position.none
+val pretty = Pretty.str o General.exnMessage;
+
+end;
+
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/ML/exn_output_polyml.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/exn_output_polyml.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -0,0 +1,19 @@
+(*  Title:      Pure/ML/exn_output_polyml.ML
+    Author:     Makarius
+
+Auxiliary operations for exception output -- Poly/ML version.
+*)
+
+structure Exn_Output: EXN_OUTPUT =
+struct
+
+fun position exn =
+  (case PolyML.exceptionLocation exn of
+    NONE => Position.none
+  | SOME loc => Exn_Properties.position_of loc);
+
+fun pretty (exn: exn) =
+  Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ())));
+
+end;
+
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/ML/exn_properties_polyml.ML
--- a/src/Pure/ML/exn_properties_polyml.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/ML/exn_properties_polyml.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -6,7 +6,7 @@
 
 signature EXN_PROPERTIES =
 sig
-  val of_location: PolyML.location -> Properties.T
+  val position_of: PolyML.location -> Position.T
   val get: exn -> Properties.T
   val update: Properties.entry list -> exn -> exn
 end;
@@ -14,23 +14,35 @@
 structure Exn_Properties: EXN_PROPERTIES =
 struct
 
-fun of_location (loc: PolyML.location) =
+(* source locations *)
+
+fun props_of (loc: PolyML.location) =
   (case YXML.parse_body (#file loc) of
     [] => []
   | [XML.Text file] => [(Markup.fileN, file)]
   | body => XML.Decode.properties body);
 
+fun position_of loc =
+  Position.make
+   {line = #startLine loc,
+    offset = #startPosition loc,
+    end_offset = #endPosition loc,
+    props = props_of loc};
+
+
+(* exception properties *)
+
 fun get exn =
   (case PolyML.exceptionLocation exn of
     NONE => []
-  | SOME loc => of_location loc);
+  | SOME loc => props_of loc);
 
 fun update entries exn =
   let
     val loc =
       the_default {file = "", startLine = 0, endLine = 0, startPosition = 0, endPosition = 0}
         (PolyML.exceptionLocation exn);
-    val props = of_location loc;
+    val props = props_of loc;
     val props' = fold Properties.put entries props;
   in
     if props = props' then exn
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -1,19 +1,11 @@
 (*  Title:      Pure/ML/ml_compiler.ML
     Author:     Makarius
 
-Runtime compilation -- generic version.
+Runtime compilation and evaluation -- generic version.
 *)
 
 signature ML_COMPILER =
 sig
-  val exn_messages_ids: exn -> Runtime.error list
-  val exn_messages: exn -> (serial * string) list
-  val exn_message: exn -> string
-  val exn_error_message: exn -> unit
-  val exn_trace: (unit -> 'a) -> 'a
-  val print_depth_raw: Config.raw
-  val print_depth: int Config.T
-  val get_print_depth: unit -> int
   type flags = {SML: bool, verbose: bool}
   val eval: flags -> Position.T -> ML_Lex.token list -> unit
 end
@@ -21,34 +13,6 @@
 structure ML_Compiler: ML_COMPILER =
 struct
 
-(* exceptions *)
-
-val exn_info =
- {exn_position = fn _: exn => Position.none,
-  pretty_exn = Pretty.str o General.exnMessage};
-
-val exn_messages_ids = Runtime.exn_messages_ids exn_info;
-val exn_messages = Runtime.exn_messages exn_info;
-val exn_message = Runtime.exn_message exn_info;
-
-val exn_error_message = Output.error_message o exn_message;
-fun exn_trace e = print_exception_trace exn_message e;
-
-
-(* print depth *)
-
-val print_depth_raw =
-  Config.declare "ML_print_depth" (fn _ => Config.Int (get_default_print_depth ()));
-val print_depth = Config.int print_depth_raw;
-
-fun get_print_depth () =
-  (case Context.thread_data () of
-    NONE => get_default_print_depth ()
-  | SOME context => Config.get_generic context print_depth);
-
-
-(* eval *)
-
 type flags = {SML: bool, verbose: bool};
 
 fun eval {SML, verbose} pos toks =
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/ML/ml_compiler_polyml.ML
     Author:     Makarius
 
-Advanced runtime compilation for Poly/ML.
+Runtime compilation and evaluation -- Poly/ML version.
 *)
 
 structure ML_Compiler: ML_COMPILER =
@@ -10,40 +10,6 @@
 open ML_Compiler;
 
 
-(* source locations *)
-
-fun position_of (loc: PolyML.location) =
-  let
-    val {startLine = line, startPosition = offset, endPosition = end_offset, ...} = loc;
-    val props = Exn_Properties.of_location loc;
-  in
-    Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
-  end;
-
-
-(* exn_info *)
-
-fun exn_position exn =
-  (case PolyML.exceptionLocation exn of
-    NONE => Position.none
-  | SOME loc => position_of loc);
-
-fun pretty_exn (exn: exn) =
-  Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, get_print_depth ())));
-
-val exn_info = {exn_position = exn_position, pretty_exn = pretty_exn};
-
-
-(* exn_message *)
-
-val exn_messages_ids = Runtime.exn_messages_ids exn_info;
-val exn_messages = Runtime.exn_messages exn_info;
-val exn_message = Runtime.exn_message exn_info;
-
-val exn_error_message = Output.error_message o exn_message;
-fun exn_trace e = print_exception_trace exn_message e;
-
-
 (* parse trees *)
 
 fun report_parse_tree depth space =
@@ -54,14 +20,15 @@
       | _ => Position.reported_text);
 
     fun reported_entity kind loc decl =
-      reported_text (position_of loc)
-        (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
+      reported_text (Exn_Properties.position_of loc)
+        (Markup.entityN,
+          (Markup.kindN, kind) :: Position.def_properties_of (Exn_Properties.position_of decl)) "";
 
     fun reported loc (PolyML.PTtype types) =
           cons
             (PolyML.NameSpace.displayTypeExpression (types, depth, space)
               |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
-              |> reported_text (position_of loc) Markup.ML_typing)
+              |> reported_text (Exn_Properties.position_of loc) Markup.ML_typing)
       | reported loc (PolyML.PTdeclaredAt decl) =
           cons (reported_entity Markup.ML_defN loc decl)
       | reported loc (PolyML.PTopenedAt decl) =
@@ -122,7 +89,7 @@
 
     fun message {message = msg, hard, location = loc, context = _} =
       let
-        val pos = position_of loc;
+        val pos = Exn_Properties.position_of loc;
         val txt =
           (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
           Pretty.string_of (Pretty.from_ML (pretty_ml msg));
@@ -131,7 +98,7 @@
 
     (* results *)
 
-    val depth = get_print_depth ();
+    val depth = ML_Options.get_print_depth ();
 
     fun apply_result {fixes, types, signatures, structures, functors, values} =
       let
@@ -172,8 +139,8 @@
       | SOME code =>
           apply_result
             ((code
-              |> Runtime.debugging exn_message opt_context
-              |> Runtime.toplevel_error (err o exn_message)) ())));
+              |> Runtime.debugging opt_context
+              |> Runtime.toplevel_error (err o Runtime.exn_message)) ())));
 
 
     (* compiler invocation *)
@@ -185,7 +152,7 @@
       PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
       PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
       PolyML.Compiler.CPFileName location_props,
-      PolyML.Compiler.CPPrintDepth get_print_depth,
+      PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
       PolyML.Compiler.CPCompilerResultFun result_fun,
       PolyML.Compiler.CPPrintInAlphabeticalOrder false];
     val _ =
@@ -199,7 +166,7 @@
               (case exn of
                 STATIC_ERRORS () => ""
               | Runtime.TOPLEVEL_ERROR => ""
-              | _ => "Exception- " ^ Pretty.string_of (pretty_exn exn) ^ " raised");
+              | _ => "Exception- " ^ Pretty.string_of (Exn_Output.pretty exn) ^ " raised");
             val _ = output_warnings ();
             val _ = output_writeln ();
           in raise_error exn_msg end;
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -17,8 +17,6 @@
   val add_antiquotation: binding -> (Args.src -> Proof.context -> decl * Proof.context) ->
     theory -> theory
   val print_antiquotations: Proof.context -> unit
-  val source_trace_raw: Config.raw
-  val source_trace: bool Config.T
   val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
     Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
   val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
@@ -137,9 +135,6 @@
         in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
   in ((ml_env @ end_env, ml_body), opt_ctxt') end;
 
-val source_trace_raw = Config.declare "ML_source_trace" (fn _ => Config.Bool false);
-val source_trace = Config.bool source_trace_raw;
-
 fun eval flags pos ants =
   let
     val non_verbose = {SML = #SML flags, verbose = false};
@@ -149,7 +144,7 @@
     val _ =
       (case Option.map Context.proof_of env_ctxt of
         SOME ctxt =>
-          if Config.get ctxt source_trace andalso Context_Position.is_visible ctxt
+          if Config.get ctxt ML_Options.source_trace andalso Context_Position.is_visible ctxt
           then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
           else ()
       | NONE => ());
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/ML/ml_options.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_options.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -0,0 +1,49 @@
+(*  Title:      Pure/ML/ml_options.ML
+    Author:     Makarius
+
+ML configuration options.
+*)
+
+signature ML_OPTIONS =
+sig
+  val source_trace_raw: Config.raw
+  val source_trace: bool Config.T
+  val exception_trace_raw: Config.raw
+  val exception_trace: bool Config.T
+  val exception_trace_enabled: Context.generic option -> bool
+  val print_depth_raw: Config.raw
+  val print_depth: int Config.T
+  val get_print_depth: unit -> int
+end;
+
+structure ML_Options: ML_OPTIONS =
+struct
+
+(* source trace *)
+
+val source_trace_raw = Config.declare "ML_source_trace" (fn _ => Config.Bool false);
+val source_trace = Config.bool source_trace_raw;
+
+
+(* exception trace *)
+
+val exception_trace_raw = Config.declare_option "ML_exception_trace";
+val exception_trace = Config.bool exception_trace_raw;
+
+fun exception_trace_enabled NONE =
+      (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false)
+  | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace;
+
+
+(* print depth *)
+
+val print_depth_raw =
+  Config.declare "ML_print_depth" (fn _ => Config.Int (get_default_print_depth ()));
+val print_depth = Config.int print_depth_raw;
+
+fun get_print_depth () =
+  (case Context.thread_data () of
+    NONE => get_default_print_depth ()
+  | SOME context => Config.get_generic context print_depth);
+
+end;
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/PIDE/command.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -196,7 +196,7 @@
         (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
           handle exn =>
             if Exn.is_interrupt exn then reraise exn
-            else ML_Compiler.exn_messages_ids exn)) ();
+            else Runtime.exn_messages_ids exn)) ();
 
 fun report tr m =
   Toplevel.setmp_thread_position tr (fn () => Output.report (Markup.markup_only m)) ();
@@ -276,10 +276,10 @@
   Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
 
 fun print_error tr opt_context e =
-  (Toplevel.setmp_thread_position tr o Toplevel.controlled_execution opt_context) e ()
+  (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
     handle exn =>
       if Exn.is_interrupt exn then reraise exn
-      else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
+      else List.app (Future.error_msg (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
 
 fun print_finished (Print {print_process, ...}) = memo_finished print_process;
 
@@ -319,7 +319,7 @@
       let
         val params = {command_name = command_name, args = args, exec_id = eval_exec_id eval};
       in
-        (case Exn.capture (Toplevel.controlled_execution NONE get_pr) params of
+        (case Exn.capture (Runtime.controlled_execution NONE get_pr) params of
           Exn.Res NONE => NONE
         | Exn.Res (SOME pr) => SOME (make_print name args pr)
         | Exn.Exn exn => SOME (bad_print name args exn))
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/PIDE/execution.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -125,7 +125,7 @@
                     status task [Markup.finished];
                     Output.report (Markup.markup_only Markup.bad);
                     if exec_id = 0 then ()
-                    else List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn))
+                    else List.app (Future.error_msg pos) (Runtime.exn_messages_ids exn))
                 | Exn.Res _ =>
                     status task [Markup.finished])
             in Exn.release result end);
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/PIDE/query_operation.ML
--- a/src/Pure/PIDE/query_operation.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/PIDE/query_operation.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -24,7 +24,7 @@
               fun status m = result (Markup.markup_only m);
               fun output_result s = result (Markup.markup (Markup.writelnN, []) s);
               fun toplevel_error exn =
-                result (Markup.markup (Markup.errorN, []) (ML_Compiler.exn_message exn));
+                result (Markup.markup (Markup.errorN, []) (Runtime.exn_message exn));
 
               val _ = status Markup.running;
               fun run () = f {state = state, args = args, output_result = output_result};
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/ROOT	Thu Mar 27 17:12:40 2014 +0100
@@ -139,6 +139,8 @@
     "Isar/token.ML"
     "Isar/toplevel.ML"
     "Isar/typedecl.ML"
+    "ML/exn_output.ML"
+    "ML/exn_output_polyml.ML"
     "ML/exn_properties_dummy.ML"
     "ML/exn_properties_polyml.ML"
     "ML/exn_trace_polyml-5.5.1.ML"
@@ -150,6 +152,7 @@
     "ML/ml_env.ML"
     "ML/ml_lex.ML"
     "ML/ml_parse.ML"
+    "ML/ml_options.ML"
     "ML/ml_statistics_dummy.ML"
     "ML/ml_statistics_polyml-5.5.0.ML"
     "ML/ml_syntax.ML"
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/ROOT.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -69,6 +69,7 @@
 
 use "PIDE/xml.ML";
 use "PIDE/yxml.ML";
+use "PIDE/document_id.ML";
 
 use "General/change_table.ML";
 use "General/graph.ML";
@@ -193,16 +194,18 @@
 
 (* Isar -- Intelligible Semi-Automated Reasoning *)
 
-(*ML support*)
+(*ML support and global execution*)
 use "ML/ml_syntax.ML";
 use "ML/ml_env.ML";
+use "ML/ml_options.ML";
+use "ML/exn_output.ML";
+if ML_System.is_polyml then use "ML/exn_output_polyml.ML" else ();
+use "ML/ml_options.ML";
 use "Isar/runtime.ML";
+use "PIDE/execution.ML";
 use "ML/ml_compiler.ML";
 if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
 
-(*global execution*)
-use "PIDE/document_id.ML";
-use "PIDE/execution.ML";
 use "skip_proof.ML";
 use "goal.ML";
 
@@ -346,7 +349,7 @@
 (* the Pure theory *)
 
 use "pure_syn.ML";
-Toplevel.program (fn () => Thy_Info.use_thy ("Pure", Position.none));
+Runtime.toplevel_program (fn () => Thy_Info.use_thy ("Pure", Position.none));
 Context.set_thread_data NONE;
 structure Pure = struct val thy = Thy_Info.get_theory "Pure" end;
 
@@ -355,7 +358,8 @@
 
 (* ML toplevel commands *)
 
-fun use_thys args = Toplevel.program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
+fun use_thys args =
+  Runtime.toplevel_program (fn () => Thy_Info.use_thys (map (rpair Position.none) args));
 val use_thy = use_thys o single;
 
 val cd = File.cd o Path.explode;
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/System/command_line.ML
--- a/src/Pure/System/command_line.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/System/command_line.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -19,7 +19,7 @@
       restore_attributes body () handle exn =>
         let
           val _ =
-            ML_Compiler.exn_error_message exn
+            Runtime.exn_error_message exn
               handle _ => Output.error_message "Exception raised, but failed to print details!";
         in if Exn.is_interrupt exn then 130 else 1 end;
     in if rc = 0 then () else exit rc end) ();
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/System/isabelle_process.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -48,9 +48,9 @@
   (case Symtab.lookup (Synchronized.value commands) name of
     NONE => error ("Undefined Isabelle protocol command " ^ quote name)
   | SOME cmd =>
-      (Toplevel.debugging NONE cmd args handle exn =>
+      (Runtime.debugging NONE cmd args handle exn =>
         error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^
-          ML_Compiler.exn_message exn)));
+          Runtime.exn_message exn)));
 
 end;
 
@@ -170,7 +170,7 @@
       [] => (Output.error_message "Isabelle process: no input"; true)
     | name :: args => (task_context (fn () => run_command name args); true))
     handle Runtime.TERMINATE => false
-      | exn => (ML_Compiler.exn_error_message exn handle crash => recover crash; true);
+      | exn => (Runtime.exn_error_message exn handle crash => recover crash; true);
   in
     if continue then loop channel
     else (Future.shutdown (); Execution.reset (); ())
diff -r c63ab5263008 -r 4cc3f4db3447 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Pure/System/isar.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -97,7 +97,7 @@
   | SOME (_, SOME exn_info) =>
      (set_exn (SOME exn_info);
       Toplevel.setmp_thread_position tr
-        ML_Compiler.exn_error_message (Runtime.EXCURSION_FAIL exn_info);
+        Runtime.exn_error_message (Runtime.EXCURSION_FAIL exn_info);
       true)
   | SOME (st', NONE) =>
       let
@@ -144,7 +144,7 @@
       NONE => if secure then quit () else ()
     | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
     handle exn =>
-      (ML_Compiler.exn_error_message exn
+      (Runtime.exn_error_message exn
         handle crash =>
           (Synchronized.change crashes (cons crash);
             warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
diff -r c63ab5263008 -r 4cc3f4db3447 src/Tools/WWW_Find/scgi_server.ML
--- a/src/Tools/WWW_Find/scgi_server.ML	Thu Mar 27 13:00:40 2014 +0100
+++ b/src/Tools/WWW_Find/scgi_server.ML	Thu Mar 27 17:12:40 2014 +0100
@@ -53,7 +53,7 @@
              ConditionVar.wait (thread_wait, thread_wait_mutex));
        add_thread
          (Thread.fork   (* FIXME avoid low-level Poly/ML thread primitives *)
-            (fn () => ML_Compiler.exn_trace threadf,
+            (fn () => Runtime.exn_trace threadf,
              [Thread.EnableBroadcastInterrupt true,
               Thread.InterruptState
               Thread.InterruptAsynchOnce])))