# HG changeset patch
# User wenzelm
# Date 1395762878 -3600
# Node ID b4d874f6c6bec8bb4710df1a2bd57d76c7ad160f
# Parent  2576d3a40ed6ab30159b45a9486c9c702e60ef28
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);

diff -r 2576d3a40ed6 -r b4d874f6c6be NEWS
--- 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.
diff -r 2576d3a40ed6 -r b4d874f6c6be etc/options
--- 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"
diff -r 2576d3a40ed6 -r b4d874f6c6be src/HOL/ex/ML.thy
--- 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"
 
diff -r 2576d3a40ed6 -r b4d874f6c6be src/Pure/Isar/attrib.ML
--- 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 #>
diff -r 2576d3a40ed6 -r b4d874f6c6be src/Pure/Isar/runtime.ML
--- 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 =
diff -r 2576d3a40ed6 -r b4d874f6c6be src/Pure/ML/ml_context.ML
--- 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 ()
diff -r 2576d3a40ed6 -r b4d874f6c6be src/Pure/Tools/proof_general_pure.ML
--- 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";