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;