--- 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 ***
--- 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"
--- 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.
--- 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
--- 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 *)
--- 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)
--- 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"
--- 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)
*}
--- 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 *)
--- 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 #>
--- 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 =>
--- 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;
--- 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)) ())));
--- 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))
--- 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)));
--- 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