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);
authorwenzelm
Tue Mar 25 16:54:38 2014 +0100 (2014-03-25)
changeset 56279b4d874f6c6be
parent 56278 2576d3a40ed6
child 56280 f7de8392a507
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);
NEWS
etc/options
src/HOL/ex/ML.thy
src/Pure/Isar/attrib.ML
src/Pure/Isar/runtime.ML
src/Pure/ML/ml_context.ML
src/Pure/Tools/proof_general_pure.ML
     1.1 --- a/NEWS	Tue Mar 25 16:11:00 2014 +0100
     1.2 +++ b/NEWS	Tue Mar 25 16:54:38 2014 +0100
     1.3 @@ -34,10 +34,6 @@
     1.4  exception.  Potential INCOMPATIBILITY for non-conformant tactical
     1.5  proof tools.
     1.6  
     1.7 -* Discontinued old Toplevel.debug in favour of system option
     1.8 -"exception_trace", which may be also declared within the context via
     1.9 -"declare [[exception_trace = true]]".  Minor INCOMPATIBILITY.
    1.10 -
    1.11  * Command 'SML_file' reads and evaluates the given Standard ML file.
    1.12  Toplevel bindings are stored within the theory context; the initial
    1.13  environment is restricted to the Standard ML implementation of
    1.14 @@ -545,6 +541,13 @@
    1.15  
    1.16  *** ML ***
    1.17  
    1.18 +* Discontinued old Toplevel.debug in favour of system option
    1.19 +"ML_exception_trace", which may be also declared within the context via
    1.20 +"declare [[ML_exception_trace = true]]".  Minor INCOMPATIBILITY.
    1.21 +
    1.22 +* Renamed option "ML_trace" to "ML_source_trace". Minor
    1.23 +INCOMPATIBILITY.
    1.24 +
    1.25  * Proper context discipline for read_instantiate and instantiate_tac:
    1.26  variables that are meant to become schematic need to be given as
    1.27  fixed, and are generalized by the explicit context of local variables.
     2.1 --- a/etc/options	Tue Mar 25 16:11:00 2014 +0100
     2.2 +++ b/etc/options	Tue Mar 25 16:54:38 2014 +0100
     2.3 @@ -97,8 +97,11 @@
     2.4  option process_output_limit : int = 100
     2.5    -- "build process output limit in million characters (0 = unlimited)"
     2.6  
     2.7 -public option exception_trace : bool = false
     2.8 -  -- "exception trace for toplevel command execution"
     2.9 +
    2.10 +section "ML System"
    2.11 +
    2.12 +public option ML_exception_trace : bool = false
    2.13 +  -- "ML exception trace for toplevel command execution"
    2.14  
    2.15  
    2.16  section "Editor Reactivity"
     3.1 --- a/src/HOL/ex/ML.thy	Tue Mar 25 16:11:00 2014 +0100
     3.2 +++ b/src/HOL/ex/ML.thy	Tue Mar 25 16:54:38 2014 +0100
     3.3 @@ -121,7 +121,7 @@
     3.4  term "factorial 4"  -- "symbolic term"
     3.5  value "factorial 4"  -- "evaluation via ML code generation in the background"
     3.6  
     3.7 -declare [[ML_trace]]
     3.8 +declare [[ML_source_trace]]
     3.9  ML {* @{term "factorial 4"} *}  -- "symbolic term in ML"
    3.10  ML {* @{code "factorial"} *}  -- "ML code from function specification"
    3.11  
     4.1 --- a/src/Pure/Isar/attrib.ML	Tue Mar 25 16:11:00 2014 +0100
     4.2 +++ b/src/Pure/Isar/attrib.ML	Tue Mar 25 16:54:38 2014 +0100
     4.3 @@ -457,7 +457,7 @@
     4.4    register_config Name_Space.names_long_raw #>
     4.5    register_config Name_Space.names_short_raw #>
     4.6    register_config Name_Space.names_unique_raw #>
     4.7 -  register_config ML_Context.trace_raw #>
     4.8 +  register_config ML_Context.source_trace_raw #>
     4.9    register_config Runtime.exception_trace_raw #>
    4.10    register_config Proof_Context.show_abbrevs_raw #>
    4.11    register_config Goal_Display.goals_limit_raw #>
     5.1 --- a/src/Pure/Isar/runtime.ML	Tue Mar 25 16:11:00 2014 +0100
     5.2 +++ b/src/Pure/Isar/runtime.ML	Tue Mar 25 16:54:38 2014 +0100
     5.3 @@ -136,7 +136,7 @@
     5.4  
     5.5  (** controlled execution **)
     5.6  
     5.7 -val exception_trace_raw = Config.declare_option "exception_trace";
     5.8 +val exception_trace_raw = Config.declare_option "ML_exception_trace";
     5.9  val exception_trace = Config.bool exception_trace_raw;
    5.10  
    5.11  fun exception_trace_enabled NONE =
     6.1 --- a/src/Pure/ML/ml_context.ML	Tue Mar 25 16:11:00 2014 +0100
     6.2 +++ b/src/Pure/ML/ml_context.ML	Tue Mar 25 16:54:38 2014 +0100
     6.3 @@ -17,8 +17,8 @@
     6.4    val add_antiquotation: binding -> (Args.src -> Proof.context -> decl * Proof.context) ->
     6.5      theory -> theory
     6.6    val print_antiquotations: Proof.context -> unit
     6.7 -  val trace_raw: Config.raw
     6.8 -  val trace: bool Config.T
     6.9 +  val source_trace_raw: Config.raw
    6.10 +  val source_trace: bool Config.T
    6.11    val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
    6.12      Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
    6.13    val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
    6.14 @@ -137,8 +137,8 @@
    6.15          in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
    6.16    in ((ml_env @ end_env, ml_body), opt_ctxt') end;
    6.17  
    6.18 -val trace_raw = Config.declare "ML_trace" (fn _ => Config.Bool false);
    6.19 -val trace = Config.bool trace_raw;
    6.20 +val source_trace_raw = Config.declare "ML_source_trace" (fn _ => Config.Bool false);
    6.21 +val source_trace = Config.bool source_trace_raw;
    6.22  
    6.23  fun eval flags pos ants =
    6.24    let
    6.25 @@ -149,7 +149,7 @@
    6.26      val _ =
    6.27        (case Option.map Context.proof_of env_ctxt of
    6.28          SOME ctxt =>
    6.29 -          if Config.get ctxt trace then
    6.30 +          if Config.get ctxt source_trace then
    6.31              Context_Position.if_visible ctxt
    6.32                tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
    6.33            else ()
     7.1 --- a/src/Pure/Tools/proof_general_pure.ML	Tue Mar 25 16:11:00 2014 +0100
     7.2 +++ b/src/Pure/Tools/proof_general_pure.ML	Tue Mar 25 16:54:38 2014 +0100
     7.3 @@ -123,7 +123,7 @@
     7.4  val _ =
     7.5    ProofGeneral.preference_option ProofGeneral.category_tracing
     7.6      NONE
     7.7 -    @{option exception_trace}
     7.8 +    @{option ML_exception_trace}
     7.9      "debugging"
    7.10      "Whether to enable exception trace for toplevel command execution";
    7.11