--- a/src/Pure/Isar/runtime.ML Fri Sep 17 21:50:44 2010 +0200
+++ b/src/Pure/Isar/runtime.ML Fri Sep 17 22:17:57 2010 +0200
@@ -10,6 +10,7 @@
exception TERMINATE
exception EXCURSION_FAIL of exn * string
exception TOPLEVEL_ERROR
+ val debug: bool Unsynchronized.ref
val exn_context: Proof.context option -> exn -> exn
val exn_messages: (exn -> Position.T) -> exn -> string list
val exn_message: (exn -> Position.T) -> exn -> string
@@ -28,6 +29,8 @@
exception EXCURSION_FAIL of exn * string;
exception TOPLEVEL_ERROR;
+val debug = Unsynchronized.ref false;
+
(* exn_context *)
@@ -52,7 +55,7 @@
| _ => cat_lines (("exception " ^ name ^ " raised" ^ pos ^ ":") :: msgs))
end;
- val detailed = ! Output.debugging;
+ val detailed = ! debug;
fun exn_msgs context exn =
if Exn.is_interrupt exn then []
@@ -94,11 +97,10 @@
| msgs => cat_lines msgs);
-
(** controlled execution **)
fun debugging f x =
- if ! Output.debugging then
+ if ! debug then
Exn.release (exception_trace (fn () =>
Exn.Result (f x) handle
exn as UNDEF => Exn.Exn exn