# HG changeset patch
# User wenzelm
# Date 1395680721 -3600
# Node ID 2ba733f6e54849fc23502e3a2d744236f24d9a44
# Parent  284dd3c35a52c6c4a1edfc79d4c6dabba358ce2c# Parent  2a091015a89651715e10bb4b2c94e2dfe481f34e
merged;

diff -r 2a091015a896 -r 2ba733f6e548 NEWS
--- a/NEWS	Thu Mar 20 17:55:33 2014 -0700
+++ b/NEWS	Mon Mar 24 18:05:21 2014 +0100
@@ -34,6 +34,10 @@
 exception.  Potential INCOMPATIBILITY for non-conformant tactical
 proof tools.
 
+* Discontinued old Toplevel.debug in favour of system option
+"exception_trace", which may be also declared within the context via
+"declare [[exception_trace = true]]".  Minor INCOMPATIBILITY.
+
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
diff -r 2a091015a896 -r 2ba733f6e548 etc/options
--- a/etc/options	Thu Mar 20 17:55:33 2014 -0700
+++ b/etc/options	Mon Mar 24 18:05:21 2014 +0100
@@ -97,6 +97,9 @@
 option process_output_limit : int = 100
   -- "build process output limit in million characters (0 = unlimited)"
 
+public option exception_trace : bool = false
+  -- "exception trace for toplevel command execution"
+
 
 section "Editor Reactivity"
 
diff -r 2a091015a896 -r 2ba733f6e548 src/Doc/IsarImplementation/Integration.thy
--- a/src/Doc/IsarImplementation/Integration.thy	Thu Mar 20 17:55:33 2014 -0700
+++ b/src/Doc/IsarImplementation/Integration.thy	Mon Mar 24 18:05:21 2014 +0100
@@ -52,7 +52,6 @@
   @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
   @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
   @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
-  @{index_ML Toplevel.debug: "bool Unsynchronized.ref"} \\
   @{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\
   @{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\
   \end{mldecls}
@@ -79,9 +78,6 @@
   \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
   state if available, otherwise raises @{ML Toplevel.UNDEF}.
 
-  \item @{ML "Toplevel.debug := true"} enables exception trace of the
-  ML runtime system.
-
   \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
   information for each Isar command being executed.
 
diff -r 2a091015a896 -r 2ba733f6e548 src/HOL/Import/HOL_Light_Maps.thy
--- a/src/HOL/Import/HOL_Light_Maps.thy	Thu Mar 20 17:55:33 2014 -0700
+++ b/src/HOL/Import/HOL_Light_Maps.thy	Mon Mar 24 18:05:21 2014 +0100
@@ -97,11 +97,11 @@
   "curry = (\<lambda>(f\<Colon>'A \<times> 'B \<Rightarrow> 'C) x y. f (x, y))"
   using curry_def .
 
-lemma [import_const ONE_ONE : Fun.inj]:
+lemma [import_const ONE_ONE : inj]:
   "inj = (\<lambda>(f\<Colon>'A \<Rightarrow> 'B). \<forall>x1 x2. f x1 = f x2 \<longrightarrow> x1 = x2)"
   by (auto simp add: fun_eq_iff inj_on_def)
 
-lemma [import_const ONTO : Fun.surj]:
+lemma [import_const ONTO : surj]:
   "surj = (\<lambda>(f\<Colon>'A \<Rightarrow> 'B). \<forall>y. \<exists>x. y = f x)"
   by (auto simp add: fun_eq_iff)
 
@@ -109,9 +109,9 @@
   by (rule_tac x="Suc_Rep" in exI)
      (metis Suc_Rep_inject' injI Suc_Rep_not_Zero_Rep surjD)
 
-import_type_map num : Nat.nat
-import_const_map "_0" : Groups.zero_class.zero
-import_const_map SUC : Nat.Suc
+import_type_map num : nat
+import_const_map "_0" : zero_class.zero
+import_const_map SUC : Suc
 
 lemma NOT_SUC: "\<forall>n. Suc n \<noteq> 0"
   by simp
@@ -141,35 +141,35 @@
 
 definition [simp]: "pred n = n - 1"
 
-lemma PRE[import_const PRE : HOL_Light_Maps.pred]:
+lemma PRE[import_const PRE : pred]:
   "pred (id (0\<Colon>nat)) = id (0\<Colon>nat) \<and> (\<forall>n\<Colon>nat. pred (Suc n) = n)"
   by simp
 
-lemma ADD[import_const "+" : Groups.plus_class.plus]:
+lemma ADD[import_const "+" : plus]:
   "(\<forall>n :: nat. (id 0) + n = n) \<and> (\<forall>m n. (Suc m) + n = Suc (m + n))"
   by simp
 
-lemma MULT[import_const "*" : Groups.times_class.times]:
+lemma MULT[import_const "*" : times]:
   "(\<forall>n :: nat. (id 0) * n = id 0) \<and> (\<forall>m n. (Suc m) * n = (m * n) + n)"
   by simp
 
-lemma EXP[import_const EXP : Power.power_class.power]:
+lemma EXP[import_const EXP : power]:
   "(\<forall>m. m ^ (id 0) = id (bit1 0)) \<and> (\<forall>(m :: nat) n. m ^ (Suc n) = m * (m ^ n))"
   by simp
 
-lemma LE[import_const "<=" : Orderings.ord_class.less_eq]:
+lemma LE[import_const "<=" : less_eq]:
   "(\<forall>m :: nat. m \<le> (id 0) = (m = id 0)) \<and> (\<forall>m n. m \<le> (Suc n) = (m = Suc n \<or> m \<le> n))"
   by auto
 
-lemma LT[import_const "<" : Orderings.ord_class.less]:
+lemma LT[import_const "<" : less]:
   "(\<forall>m :: nat. m < (id 0) = False) \<and> (\<forall>m n. m < (Suc n) = (m = n \<or> m < n))"
   by auto
 
-lemma DEF_GE[import_const ">=" : "Orderings.ord_class.greater_eq"]:
+lemma DEF_GE[import_const ">=" : greater_eq]:
   "(op \<ge>) = (\<lambda>x y :: nat. y \<le> x)"
   by simp
 
-lemma DEF_GT[import_const ">" : "Orderings.ord_class.greater"]:
+lemma DEF_GT[import_const ">" : greater]:
   "(op >) = (\<lambda>x y :: nat. y < x)"
   by simp
 
@@ -181,28 +181,28 @@
   "min = (\<lambda>x y :: nat. if x \<le> y then x else y)"
   by (auto simp add: min.absorb_iff1 fun_eq_iff)
 
-lemma EVEN[import_const "EVEN" : "Parity.even_odd_class.even"]:
+lemma EVEN[import_const "EVEN" : even]:
   "even (id 0\<Colon>nat) = True \<and> (\<forall>n. even (Suc n) = (\<not> even n))"
   by simp
 
-lemma SUB[import_const "-" : "Groups.minus_class.minus"]:
+lemma SUB[import_const "-" : minus]:
   "(\<forall>m\<Colon>nat. m - (id 0) = m) \<and> (\<forall>m n. m - (Suc n) = pred (m - n))"
   by simp
 
-lemma FACT[import_const "FACT" : "Fact.fact_class.fact"]:
+lemma FACT[import_const "FACT" : fact]:
   "fact (id 0) = id (bit1 0) \<and> (\<forall>n. fact (Suc n) = Suc n * fact n)"
   by simp
 
-import_const_map MOD : Divides.div_class.mod
-import_const_map DIV : Divides.div_class.div
+import_const_map MOD : mod
+import_const_map DIV : div
 
 lemma DIVISION_0:
   "\<forall>m n\<Colon>nat. if n = id 0 then m div n = id 0 \<and> m mod n = m else m = m div n * n + m mod n \<and> m mod n < n"
   by simp
 
 lemmas [import_type sum "_dest_sum" "_mk_sum"] = type_definition_sum[where 'a="'A" and 'b="'B"]
-import_const_map INL : Sum_Type.Inl
-import_const_map INR : Sum_Type.Inr
+import_const_map INL : Inl
+import_const_map INR : Inr
 
 lemma sum_INDUCT:
   "\<forall>P. (\<forall>a :: 'A. P (Inl a)) \<and> (\<forall>a :: 'B. P (Inr a)) \<longrightarrow> (\<forall>x. P x)"
@@ -212,17 +212,17 @@
   "\<forall>Inl' Inr'. \<exists>fn. (\<forall>a :: 'A. fn (Inl a) = (Inl' a :: 'Z)) \<and> (\<forall>a :: 'B. fn (Inr a) = Inr' a)"
   by (intro allI, rule_tac x="case_sum Inl' Inr'" in exI) auto
 
-lemma OUTL[import_const "OUTL" : "Sum_Type.projl"]:
+lemma OUTL[import_const "OUTL" : projl]:
   "Sum_Type.projl (Inl x) = x"
   by simp
 
-lemma OUTR[import_const "OUTR" : "Sum_Type.projr"]:
+lemma OUTR[import_const "OUTR" : projr]:
   "Sum_Type.projr (Inr y) = y"
   by simp
 
-import_type_map list : List.list
-import_const_map NIL : List.list.Nil
-import_const_map CONS : List.list.Cons
+import_type_map list : list
+import_const_map NIL : Nil
+import_const_map CONS : Cons
 
 lemma list_INDUCT:
   "\<forall>P\<Colon>'A list \<Rightarrow> bool. P [] \<and> (\<forall>a0 a1. P a1 \<longrightarrow> P (a0 # a1)) \<longrightarrow> (\<forall>x. P x)"
@@ -232,41 +232,41 @@
  "\<forall>nil' cons'. \<exists>fn\<Colon>'A list \<Rightarrow> 'Z. fn [] = nil' \<and> (\<forall>(a0\<Colon>'A) a1\<Colon>'A list. fn (a0 # a1) = cons' a0 a1 (fn a1))"
   by (intro allI, rule_tac x="rec_list nil' cons'" in exI) auto
 
-lemma HD[import_const HD : List.list.hd]:
+lemma HD[import_const HD : hd]:
   "hd ((h\<Colon>'A) # t) = h"
   by simp
 
-lemma TL[import_const TL : List.list.tl]:
+lemma TL[import_const TL : tl]:
   "tl ((h\<Colon>'A) # t) = t"
   by simp
 
-lemma APPEND[import_const APPEND : List.append]:
+lemma APPEND[import_const APPEND : append]:
   "(\<forall>l\<Colon>'A list. [] @ l = l) \<and> (\<forall>(h\<Colon>'A) t l. (h # t) @ l = h # t @ l)"
   by simp
 
-lemma REVERSE[import_const REVERSE : List.rev]:
+lemma REVERSE[import_const REVERSE : rev]:
   "rev [] = ([] :: 'A list) \<and> rev ((x\<Colon>'A) # l) = rev l @ [x]"
   by simp
 
-lemma LENGTH[import_const LENGTH : List.length]:
+lemma LENGTH[import_const LENGTH : length]:
   "length ([] :: 'A list) = id 0 \<and> (\<forall>(h\<Colon>'A) t. length (h # t) = Suc (length t))"
   by simp
 
-lemma MAP[import_const MAP : List.list.map]:
+lemma MAP[import_const MAP : map]:
   "(\<forall>f\<Colon>'A \<Rightarrow> 'B. map f [] = []) \<and>
        (\<forall>(f\<Colon>'A \<Rightarrow> 'B) h t. map f (h # t) = f h # map f t)"
   by simp
 
-lemma LAST[import_const LAST : List.last]:
+lemma LAST[import_const LAST : last]:
   "last ((h\<Colon>'A) # t) = (if t = [] then h else last t)"
   by simp
 
-lemma BUTLAST[import_const BUTLAST : List.butlast]:
+lemma BUTLAST[import_const BUTLAST : butlast]:
     "butlast [] = ([] :: 't18337 list) \<and>
      butlast ((h :: 't18337) # t) = (if t = [] then [] else h # butlast t)"
   by simp
 
-lemma REPLICATE[import_const REPLICATE : List.replicate]:
+lemma REPLICATE[import_const REPLICATE : replicate]:
   "replicate (id (0\<Colon>nat)) (x\<Colon>'t18358) = [] \<and>
    replicate (Suc n) x = x # replicate n x"
   by simp
@@ -275,38 +275,38 @@
   "List.null ([]\<Colon>'t18373 list) = True \<and> List.null ((h\<Colon>'t18373) # t) = False"
   unfolding null_def by simp
 
-lemma ALL[import_const ALL : List.list_all]:
+lemma ALL[import_const ALL : list_all]:
   "list_all (P\<Colon>'t18393 \<Rightarrow> bool) [] = True \<and>
   list_all P (h # t) = (P h \<and> list_all P t)"
   by simp
 
-lemma EX[import_const EX : List.list_ex]:
+lemma EX[import_const EX : list_ex]:
   "list_ex (P\<Colon>'t18414 \<Rightarrow> bool) [] = False \<and>
   list_ex P (h # t) = (P h \<or> list_ex P t)"
   by simp
 
-lemma ITLIST[import_const ITLIST : List.foldr]:
+lemma ITLIST[import_const ITLIST : foldr]:
   "foldr (f\<Colon>'t18437 \<Rightarrow> 't18436 \<Rightarrow> 't18436) [] b = b \<and>
   foldr f (h # t) b = f h (foldr f t b)"
   by simp
 
-lemma ALL2_DEF[import_const ALL2 : List.list.list_all2]:
+lemma ALL2_DEF[import_const ALL2 : list_all2]:
   "list_all2 (P\<Colon>'t18495 \<Rightarrow> 't18502 \<Rightarrow> bool) [] (l2\<Colon>'t18502 list) = (l2 = []) \<and>
   list_all2 P ((h1\<Colon>'t18495) # (t1\<Colon>'t18495 list)) l2 =
   (if l2 = [] then False else P h1 (hd l2) \<and> list_all2 P t1 (tl l2))"
   by simp (induct_tac l2, simp_all)
 
-lemma FILTER[import_const FILTER : List.filter]:
+lemma FILTER[import_const FILTER : filter]:
   "filter (P\<Colon>'t18680 \<Rightarrow> bool) [] = [] \<and>
   filter P ((h\<Colon>'t18680) # t) = (if P h then h # filter P t else filter P t)"
   by simp
 
-lemma ZIP[import_const ZIP : List.zip]:
+lemma ZIP[import_const ZIP : zip]:
  "zip [] [] = ([] :: ('t18824 \<times> 't18825) list) \<and>
   zip ((h1\<Colon>'t18849) # t1) ((h2\<Colon>'t18850) # t2) = (h1, h2) # zip t1 t2"
   by simp
 
-lemma WF[import_const WF : Wellfounded.wfP]:
+lemma WF[import_const WF : wfP]:
   "\<forall>u. wfP u \<longleftrightarrow> (\<forall>P. (\<exists>x :: 'A. P x) \<longrightarrow> (\<exists>x. P x \<and> (\<forall>y. u y x \<longrightarrow> \<not> P y)))"
 proof (intro allI iffI impI wfI_min[to_pred], elim exE wfE_min[to_pred])
   fix x :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and xa :: "'a" and Q
diff -r 2a091015a896 -r 2ba733f6e548 src/HOL/Import/import_data.ML
--- a/src/HOL/Import/import_data.ML	Thu Mar 20 17:55:33 2014 -0700
+++ b/src/HOL/Import/import_data.ML	Mon Mar 24 18:05:21 2014 +0100
@@ -13,7 +13,9 @@
   val get_typ_def : string -> theory -> thm option
 
   val add_const_map : string -> string -> theory -> theory
+  val add_const_map_cmd : string -> string -> theory -> theory
   val add_typ_map : string -> string -> theory -> theory
+  val add_typ_map_cmd : string -> string -> theory -> theory
   val add_const_def : string -> thm -> string option -> theory -> theory
   val add_typ_def : string -> string -> string -> thm -> theory -> theory
 end
@@ -49,11 +51,23 @@
     {const_map = (Symtab.update (s1, s2) const_map), ty_map = ty_map,
      const_def = const_def, ty_def = ty_def}) thy
 
+fun add_const_map_cmd s1 raw_s2 thy =
+  let
+    val ctxt = Proof_Context.init_global thy
+    val Const (s2, _) = Proof_Context.read_const {proper = true, strict = false} ctxt raw_s2
+  in add_const_map s1 s2 thy end
+
 fun add_typ_map s1 s2 thy =
   Data.map (fn {const_map, ty_map, const_def, ty_def} =>
     {const_map = const_map, ty_map = (Symtab.update (s1, s2) ty_map),
      const_def = const_def, ty_def = ty_def}) thy
 
+fun add_typ_map_cmd s1 raw_s2 thy =
+  let
+    val ctxt = Proof_Context.init_global thy
+    val Type (s2, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt raw_s2
+  in add_typ_map s1 s2 thy end
+
 fun add_const_def s th name_opt thy =
   let
     val th = Thm.legacy_freezeT th
@@ -89,7 +103,8 @@
 
 val _ = Theory.setup
   (Attrib.setup @{binding import_const}
-    (Scan.lift (Parse.name -- Scan.option (@{keyword ":"} |-- Parse.xname)) >>
+    (Scan.lift Parse.name --
+      Scan.option (Scan.lift @{keyword ":"} |-- Args.const {proper = true, strict = false}) >>
       (fn (s1, s2) => Thm.declaration_attribute
         (fn th => Context.mapping (add_const_def s1 th s2) I)))
   "declare a theorem as an equality that maps the given constant")
@@ -104,14 +119,14 @@
 val _ =
   Outer_Syntax.command @{command_spec "import_type_map"}
     "map external type name to existing Isabelle/HOL type name"
-    ((Parse.name --| @{keyword ":"}) -- Parse.xname >>
-      (fn (ty_name1, ty_name2) => Toplevel.theory (add_typ_map ty_name1 ty_name2)))
+    ((Parse.name --| @{keyword ":"}) -- Parse.type_const >>
+      (fn (ty_name1, ty_name2) => Toplevel.theory (add_typ_map_cmd ty_name1 ty_name2)))
 
 val _ =
   Outer_Syntax.command @{command_spec "import_const_map"}
     "map external const name to existing Isabelle/HOL const name"
-    ((Parse.name --| @{keyword ":"}) -- Parse.xname >>
-      (fn (cname1, cname2) => Toplevel.theory (add_const_map cname1 cname2)))
+    ((Parse.name --| @{keyword ":"}) -- Parse.const >>
+      (fn (cname1, cname2) => Toplevel.theory (add_const_map_cmd cname1 cname2)))
 
 (* Initial type and constant maps, for types and constants that are not
    defined, which means their definitions do not appear in the proof dump *)
diff -r 2a091015a896 -r 2ba733f6e548 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Thu Mar 20 17:55:33 2014 -0700
+++ b/src/HOL/Import/import_rule.ML	Mon Mar 24 18:05:21 2014 +0100
@@ -172,10 +172,11 @@
   let
     val rhs = term_of rhs
     val typ = type_of rhs
-    val thy1 = Sign.add_consts [(Binding.name constname, typ, NoSyn)] thy
-    val eq = Logic.mk_equals (Const (Sign.intern_const thy1 constname, typ), rhs)
+    val constbinding = Binding.name constname
+    val thy1 = Sign.add_consts [(constbinding, typ, NoSyn)] thy
+    val eq = Logic.mk_equals (Const (Sign.full_name thy1 constbinding, typ), rhs)
     val (thms, thy2) = Global_Theory.add_defs false
-      [((Binding.suffix_name "_hldef" (Binding.name constname), eq), [])] thy1
+      [((Binding.suffix_name "_hldef" constbinding, eq), [])] thy1
     val def_thm = freezeT (hd thms)
   in
     (meta_eq_to_obj_eq def_thm, thy2)
diff -r 2a091015a896 -r 2ba733f6e548 src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Thu Mar 20 17:55:33 2014 -0700
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Mon Mar 24 18:05:21 2014 +0100
@@ -285,7 +285,7 @@
 
 type tptp_problem = tptp_line list
 
-fun debug f x = if !Runtime.debug then (f x; ()) else ()
+fun debug f x = if Options.default_bool @{option exception_trace} then (f x; ()) else ()
 
 fun nameof_tff_atom_type (Atom_type str) = str
   | nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
diff -r 2a091015a896 -r 2ba733f6e548 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Thu Mar 20 17:55:33 2014 -0700
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Mon Mar 24 18:05:21 2014 +0100
@@ -42,7 +42,7 @@
 ML {*
   if test_all @{context} then ()
   else
-    (Toplevel.debug := true;
+    (Options.default_put_bool @{option exception_trace} true;
      PolyML.print_depth 200;
      PolyML.Compiler.maxInlineSize := 0)
 *}
diff -r 2a091015a896 -r 2ba733f6e548 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Thu Mar 20 17:55:33 2014 -0700
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Mon Mar 24 18:05:21 2014 +0100
@@ -11,9 +11,9 @@
 imports TPTP_Test TPTP_Proof_Reconstruction
 begin
 
+declare [[exception_trace]]
 ML {*
 print_depth 200;
-Toplevel.debug := true;
 PolyML.Compiler.maxInlineSize := 0;
 (* FIXME doesn't work with Isabelle?
    PolyML.Compiler.debug := true *)
diff -r 2a091015a896 -r 2ba733f6e548 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Mar 20 17:55:33 2014 -0700
+++ b/src/Pure/Isar/attrib.ML	Mon Mar 24 18:05:21 2014 +0100
@@ -458,6 +458,7 @@
   register_config Name_Space.names_short_raw #>
   register_config Name_Space.names_unique_raw #>
   register_config ML_Context.trace_raw #>
+  register_config Runtime.exception_trace_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 2a091015a896 -r 2ba733f6e548 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Thu Mar 20 17:55:33 2014 -0700
+++ b/src/Pure/Isar/runtime.ML	Mon Mar 24 18:05:21 2014 +0100
@@ -10,15 +10,16 @@
   exception TERMINATE
   exception EXCURSION_FAIL of exn * string
   exception TOPLEVEL_ERROR
-  val debug: bool Unsynchronized.ref
   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 debugging: (exn -> string) -> ('a -> 'b) -> 'a -> 'b
-  val controlled_execution: (exn -> string) -> ('a -> 'b) -> 'a -> 'b
+  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 toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
 end;
 
@@ -32,8 +33,6 @@
 exception EXCURSION_FAIL of exn * string;
 exception TOPLEVEL_ERROR;
 
-val debug = Unsynchronized.ref false;
-
 
 (* exn_context *)
 
@@ -137,13 +136,20 @@
 
 (** controlled execution **)
 
-fun debugging exn_message f x =
-  if ! debug
+val exception_trace_raw = Config.declare_option "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
   then print_exception_trace exn_message (fn () => f x)
   else f x;
 
-fun controlled_execution exn_message f x =
-  (f |> debugging exn_message |> Future.interruptible_task) x;
+fun controlled_execution exn_message opt_context f x =
+  (f |> debugging exn_message opt_context |> Future.interruptible_task) x;
 
 fun toplevel_error output_exn f x = f x
   handle exn =>
diff -r 2a091015a896 -r 2ba733f6e548 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Mar 20 17:55:33 2014 -0700
+++ b/src/Pure/Isar/toplevel.ML	Mon Mar 24 18:05:21 2014 +0100
@@ -29,9 +29,8 @@
   val interact: bool Unsynchronized.ref
   val timing: bool Unsynchronized.ref
   val profiling: int Unsynchronized.ref
-  val debug: bool Unsynchronized.ref
-  val debugging: ('a -> 'b) -> 'a -> 'b
-  val controlled_execution: ('a -> 'b) -> 'a -> 'b
+  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
@@ -235,19 +234,18 @@
 
 (* controlled execution *)
 
-val debug = Runtime.debug;
-fun debugging f = Runtime.debugging ML_Compiler.exn_message f;
-fun controlled_execution f = Runtime.controlled_execution ML_Compiler.exn_message f;
+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
+  |> 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
+        |> debugging NONE
         |> Runtime.toplevel_error
           (fn exn =>
             Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
@@ -272,11 +270,12 @@
 fun apply_transaction f g node =
   let
     val cont_node = reset_presentation node;
+    val context = cases_node I (Context.Proof o Proof.context_of) cont_node;
     fun state_error e nd = (State (SOME nd, SOME node), e);
 
     val (result, err) =
       cont_node
-      |> controlled_execution f
+      |> controlled_execution (SOME context) f
       |> state_error NONE
       handle exn => state_error (SOME exn) cont_node;
   in
@@ -305,11 +304,11 @@
 local
 
 fun apply_tr _ (Init f) (State (NONE, _)) =
-      State (SOME (Theory (Context.Theory (controlled_execution f ()), NONE)), NONE)
+      State (SOME (Theory (Context.Theory (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 (fn x => tap (f int) x) state
+      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;
diff -r 2a091015a896 -r 2ba733f6e548 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Mar 20 17:55:33 2014 -0700
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Mon Mar 24 18:05:21 2014 +0100
@@ -78,6 +78,7 @@
   let
     val _ = Secure.secure_mltext ();
     val space = ML_Env.name_space;
+    val opt_context = Context.thread_data ();
 
 
     (* input *)
@@ -168,7 +169,7 @@
       | SOME code =>
           apply_result
             ((code
-              |> Runtime.debugging exn_message
+              |> Runtime.debugging exn_message opt_context
               |> Runtime.toplevel_error (err o exn_message)) ())));
 
 
diff -r 2a091015a896 -r 2ba733f6e548 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Thu Mar 20 17:55:33 2014 -0700
+++ b/src/Pure/PIDE/command.ML	Mon Mar 24 18:05:21 2014 +0100
@@ -271,8 +271,8 @@
 val print_functions =
   Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
 
-fun print_error tr e =
-  (Toplevel.setmp_thread_position tr o Toplevel.controlled_execution) e ()
+fun print_error tr opt_context e =
+  (Toplevel.setmp_thread_position tr o Toplevel.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);
@@ -298,9 +298,10 @@
           let
             val {failed, command, state = st', ...} = eval_result eval;
             val tr = Toplevel.exec_id exec_id command;
+            val opt_context = try Toplevel.generic_theory_of st';
           in
             if failed andalso strict then ()
-            else print_error tr (fn () => print_fn tr st')
+            else print_error tr opt_context (fn () => print_fn tr st')
           end;
       in
         Print {
@@ -316,7 +317,7 @@
       let
         val params = {command_name = command_name, args = args};
       in
-        (case Exn.capture (Toplevel.controlled_execution get_pr) params of
+        (case Exn.capture (Toplevel.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 2a091015a896 -r 2ba733f6e548 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Thu Mar 20 17:55:33 2014 -0700
+++ b/src/Pure/System/isabelle_process.ML	Mon Mar 24 18:05:21 2014 +0100
@@ -48,7 +48,7 @@
   (case Symtab.lookup (Synchronized.value commands) name of
     NONE => error ("Undefined Isabelle protocol command " ^ quote name)
   | SOME cmd =>
-      (Toplevel.debugging cmd args handle exn =>
+      (Toplevel.debugging NONE cmd args handle exn =>
         error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^
           ML_Compiler.exn_message exn)));
 
diff -r 2a091015a896 -r 2ba733f6e548 src/Pure/Tools/proof_general_pure.ML
--- a/src/Pure/Tools/proof_general_pure.ML	Thu Mar 20 17:55:33 2014 -0700
+++ b/src/Pure/Tools/proof_general_pure.ML	Mon Mar 24 18:05:21 2014 +0100
@@ -121,11 +121,11 @@
     "Whether to enable timing in Isabelle";
 
 val _ =
-  ProofGeneral.preference_bool ProofGeneral.category_tracing
+  ProofGeneral.preference_option ProofGeneral.category_tracing
     NONE
-    Toplevel.debug
+    @{option exception_trace}
     "debugging"
-    "Whether to enable debugging";
+    "Whether to enable exception trace for toplevel command execution";
 
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_tracing