--- a/NEWS Sun Mar 23 16:40:35 2014 +0100
+++ b/NEWS Mon Mar 24 12:00:17 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 Sun Mar 23 16:40:35 2014 +0100
+++ b/etc/options Mon Mar 24 12:00:17 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 Sun Mar 23 16:40:35 2014 +0100
+++ b/src/Doc/IsarImplementation/Integration.thy Mon Mar 24 12:00:17 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/TPTP/TPTP_Parser/tptp_syntax.ML Sun Mar 23 16:40:35 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Mon Mar 24 12:00:17 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 Sun Mar 23 16:40:35 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Mon Mar 24 12:00:17 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 Sun Mar 23 16:40:35 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy Mon Mar 24 12:00:17 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 Sun Mar 23 16:40:35 2014 +0100
+++ b/src/Pure/Isar/attrib.ML Mon Mar 24 12:00:17 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 Sun Mar 23 16:40:35 2014 +0100
+++ b/src/Pure/Isar/runtime.ML Mon Mar 24 12:00:17 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 Sun Mar 23 16:40:35 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML Mon Mar 24 12:00:17 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 Sun Mar 23 16:40:35 2014 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML Mon Mar 24 12:00:17 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 Sun Mar 23 16:40:35 2014 +0100
+++ b/src/Pure/PIDE/command.ML Mon Mar 24 12:00:17 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 Sun Mar 23 16:40:35 2014 +0100
+++ b/src/Pure/System/isabelle_process.ML Mon Mar 24 12:00:17 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 Sun Mar 23 16:40:35 2014 +0100
+++ b/src/Pure/Tools/proof_general_pure.ML Mon Mar 24 12:00:17 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