clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
--- a/NEWS Tue Mar 25 16:11:00 2014 +0100
+++ b/NEWS Tue Mar 25 16:54:38 2014 +0100
@@ -34,10 +34,6 @@
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.
-
* Command 'SML_file' reads and evaluates the given Standard ML file.
Toplevel bindings are stored within the theory context; the initial
environment is restricted to the Standard ML implementation of
@@ -545,6 +541,13 @@
*** ML ***
+* Discontinued old Toplevel.debug in favour of system option
+"ML_exception_trace", which may be also declared within the context via
+"declare [[ML_exception_trace = true]]". Minor INCOMPATIBILITY.
+
+* Renamed option "ML_trace" to "ML_source_trace". Minor
+INCOMPATIBILITY.
+
* Proper context discipline for read_instantiate and instantiate_tac:
variables that are meant to become schematic need to be given as
fixed, and are generalized by the explicit context of local variables.
--- a/etc/options Tue Mar 25 16:11:00 2014 +0100
+++ b/etc/options Tue Mar 25 16:54:38 2014 +0100
@@ -97,8 +97,11 @@
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 "ML System"
+
+public option ML_exception_trace : bool = false
+ -- "ML exception trace for toplevel command execution"
section "Editor Reactivity"
--- a/src/HOL/ex/ML.thy Tue Mar 25 16:11:00 2014 +0100
+++ b/src/HOL/ex/ML.thy Tue Mar 25 16:54:38 2014 +0100
@@ -121,7 +121,7 @@
term "factorial 4" -- "symbolic term"
value "factorial 4" -- "evaluation via ML code generation in the background"
-declare [[ML_trace]]
+declare [[ML_source_trace]]
ML {* @{term "factorial 4"} *} -- "symbolic term in ML"
ML {* @{code "factorial"} *} -- "ML code from function specification"
--- a/src/Pure/Isar/attrib.ML Tue Mar 25 16:11:00 2014 +0100
+++ b/src/Pure/Isar/attrib.ML Tue Mar 25 16:54:38 2014 +0100
@@ -457,7 +457,7 @@
register_config Name_Space.names_long_raw #>
register_config Name_Space.names_short_raw #>
register_config Name_Space.names_unique_raw #>
- register_config ML_Context.trace_raw #>
+ register_config ML_Context.source_trace_raw #>
register_config Runtime.exception_trace_raw #>
register_config Proof_Context.show_abbrevs_raw #>
register_config Goal_Display.goals_limit_raw #>
--- a/src/Pure/Isar/runtime.ML Tue Mar 25 16:11:00 2014 +0100
+++ b/src/Pure/Isar/runtime.ML Tue Mar 25 16:54:38 2014 +0100
@@ -136,7 +136,7 @@
(** controlled execution **)
-val exception_trace_raw = Config.declare_option "exception_trace";
+val exception_trace_raw = Config.declare_option "ML_exception_trace";
val exception_trace = Config.bool exception_trace_raw;
fun exception_trace_enabled NONE =
--- a/src/Pure/ML/ml_context.ML Tue Mar 25 16:11:00 2014 +0100
+++ b/src/Pure/ML/ml_context.ML Tue Mar 25 16:54:38 2014 +0100
@@ -17,8 +17,8 @@
val add_antiquotation: binding -> (Args.src -> Proof.context -> decl * Proof.context) ->
theory -> theory
val print_antiquotations: Proof.context -> unit
- val trace_raw: Config.raw
- val trace: bool Config.T
+ val source_trace_raw: Config.raw
+ val source_trace: bool Config.T
val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
@@ -137,8 +137,8 @@
in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
in ((ml_env @ end_env, ml_body), opt_ctxt') end;
-val trace_raw = Config.declare "ML_trace" (fn _ => Config.Bool false);
-val trace = Config.bool trace_raw;
+val source_trace_raw = Config.declare "ML_source_trace" (fn _ => Config.Bool false);
+val source_trace = Config.bool source_trace_raw;
fun eval flags pos ants =
let
@@ -149,7 +149,7 @@
val _ =
(case Option.map Context.proof_of env_ctxt of
SOME ctxt =>
- if Config.get ctxt trace then
+ if Config.get ctxt source_trace then
Context_Position.if_visible ctxt
tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
else ()
--- a/src/Pure/Tools/proof_general_pure.ML Tue Mar 25 16:11:00 2014 +0100
+++ b/src/Pure/Tools/proof_general_pure.ML Tue Mar 25 16:54:38 2014 +0100
@@ -123,7 +123,7 @@
val _ =
ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- @{option exception_trace}
+ @{option ML_exception_trace}
"debugging"
"Whether to enable exception trace for toplevel command execution";