discontinued Toplevel.debug in favour of system option "exception_trace";
authorwenzelm
Mon Mar 24 12:00:17 2014 +0100 (2014-03-24)
changeset 56265785569927666
parent 56260 3d79c132e657
child 56266 da5f22a60cb3
discontinued Toplevel.debug in favour of system option "exception_trace";
NEWS
etc/options
src/Doc/IsarImplementation/Integration.thy
src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
src/Pure/Isar/attrib.ML
src/Pure/Isar/runtime.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/PIDE/command.ML
src/Pure/System/isabelle_process.ML
src/Pure/Tools/proof_general_pure.ML
     1.1 --- a/NEWS	Sun Mar 23 16:40:35 2014 +0100
     1.2 +++ b/NEWS	Mon Mar 24 12:00:17 2014 +0100
     1.3 @@ -34,6 +34,10 @@
     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  
    1.12  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.13  
     2.1 --- a/etc/options	Sun Mar 23 16:40:35 2014 +0100
     2.2 +++ b/etc/options	Mon Mar 24 12:00:17 2014 +0100
     2.3 @@ -97,6 +97,9 @@
     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  
    2.11  section "Editor Reactivity"
    2.12  
     3.1 --- a/src/Doc/IsarImplementation/Integration.thy	Sun Mar 23 16:40:35 2014 +0100
     3.2 +++ b/src/Doc/IsarImplementation/Integration.thy	Mon Mar 24 12:00:17 2014 +0100
     3.3 @@ -52,7 +52,6 @@
     3.4    @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
     3.5    @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
     3.6    @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
     3.7 -  @{index_ML Toplevel.debug: "bool Unsynchronized.ref"} \\
     3.8    @{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\
     3.9    @{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\
    3.10    \end{mldecls}
    3.11 @@ -79,9 +78,6 @@
    3.12    \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
    3.13    state if available, otherwise raises @{ML Toplevel.UNDEF}.
    3.14  
    3.15 -  \item @{ML "Toplevel.debug := true"} enables exception trace of the
    3.16 -  ML runtime system.
    3.17 -
    3.18    \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
    3.19    information for each Isar command being executed.
    3.20  
     4.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Sun Mar 23 16:40:35 2014 +0100
     4.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Mon Mar 24 12:00:17 2014 +0100
     4.3 @@ -285,7 +285,7 @@
     4.4  
     4.5  type tptp_problem = tptp_line list
     4.6  
     4.7 -fun debug f x = if !Runtime.debug then (f x; ()) else ()
     4.8 +fun debug f x = if Options.default_bool @{option exception_trace} then (f x; ()) else ()
     4.9  
    4.10  fun nameof_tff_atom_type (Atom_type str) = str
    4.11    | nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
     5.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Sun Mar 23 16:40:35 2014 +0100
     5.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Mon Mar 24 12:00:17 2014 +0100
     5.3 @@ -42,7 +42,7 @@
     5.4  ML {*
     5.5    if test_all @{context} then ()
     5.6    else
     5.7 -    (Toplevel.debug := true;
     5.8 +    (Options.default_put_bool @{option exception_trace} true;
     5.9       PolyML.print_depth 200;
    5.10       PolyML.Compiler.maxInlineSize := 0)
    5.11  *}
     6.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Sun Mar 23 16:40:35 2014 +0100
     6.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Mon Mar 24 12:00:17 2014 +0100
     6.3 @@ -11,9 +11,9 @@
     6.4  imports TPTP_Test TPTP_Proof_Reconstruction
     6.5  begin
     6.6  
     6.7 +declare [[exception_trace]]
     6.8  ML {*
     6.9  print_depth 200;
    6.10 -Toplevel.debug := true;
    6.11  PolyML.Compiler.maxInlineSize := 0;
    6.12  (* FIXME doesn't work with Isabelle?
    6.13     PolyML.Compiler.debug := true *)
     7.1 --- a/src/Pure/Isar/attrib.ML	Sun Mar 23 16:40:35 2014 +0100
     7.2 +++ b/src/Pure/Isar/attrib.ML	Mon Mar 24 12:00:17 2014 +0100
     7.3 @@ -458,6 +458,7 @@
     7.4    register_config Name_Space.names_short_raw #>
     7.5    register_config Name_Space.names_unique_raw #>
     7.6    register_config ML_Context.trace_raw #>
     7.7 +  register_config Runtime.exception_trace_raw #>
     7.8    register_config Proof_Context.show_abbrevs_raw #>
     7.9    register_config Goal_Display.goals_limit_raw #>
    7.10    register_config Goal_Display.show_main_goal_raw #>
     8.1 --- a/src/Pure/Isar/runtime.ML	Sun Mar 23 16:40:35 2014 +0100
     8.2 +++ b/src/Pure/Isar/runtime.ML	Mon Mar 24 12:00:17 2014 +0100
     8.3 @@ -10,15 +10,16 @@
     8.4    exception TERMINATE
     8.5    exception EXCURSION_FAIL of exn * string
     8.6    exception TOPLEVEL_ERROR
     8.7 -  val debug: bool Unsynchronized.ref
     8.8    val exn_context: Proof.context option -> exn -> exn
     8.9    type exn_info = {exn_position: exn -> Position.T, pretty_exn: exn -> Pretty.T}
    8.10    type error = ((serial * string) * string option)
    8.11    val exn_messages_ids: exn_info -> exn -> error list
    8.12    val exn_messages: exn_info -> exn -> (serial * string) list
    8.13    val exn_message: exn_info -> exn -> string
    8.14 -  val debugging: (exn -> string) -> ('a -> 'b) -> 'a -> 'b
    8.15 -  val controlled_execution: (exn -> string) -> ('a -> 'b) -> 'a -> 'b
    8.16 +  val exception_trace_raw: Config.raw
    8.17 +  val exception_trace: bool Config.T
    8.18 +  val debugging: (exn -> string) -> Context.generic option -> ('a -> 'b) -> 'a -> 'b
    8.19 +  val controlled_execution: (exn -> string) -> Context.generic option -> ('a -> 'b) -> 'a -> 'b
    8.20    val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
    8.21  end;
    8.22  
    8.23 @@ -32,8 +33,6 @@
    8.24  exception EXCURSION_FAIL of exn * string;
    8.25  exception TOPLEVEL_ERROR;
    8.26  
    8.27 -val debug = Unsynchronized.ref false;
    8.28 -
    8.29  
    8.30  (* exn_context *)
    8.31  
    8.32 @@ -137,13 +136,20 @@
    8.33  
    8.34  (** controlled execution **)
    8.35  
    8.36 -fun debugging exn_message f x =
    8.37 -  if ! debug
    8.38 +val exception_trace_raw = Config.declare_option "exception_trace";
    8.39 +val exception_trace = Config.bool exception_trace_raw;
    8.40 +
    8.41 +fun exception_trace_enabled NONE =
    8.42 +      (Options.default_bool (Config.name_of exception_trace_raw) handle ERROR _ => false)
    8.43 +  | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace;
    8.44 +
    8.45 +fun debugging exn_message opt_context f x =
    8.46 +  if exception_trace_enabled opt_context
    8.47    then print_exception_trace exn_message (fn () => f x)
    8.48    else f x;
    8.49  
    8.50 -fun controlled_execution exn_message f x =
    8.51 -  (f |> debugging exn_message |> Future.interruptible_task) x;
    8.52 +fun controlled_execution exn_message opt_context f x =
    8.53 +  (f |> debugging exn_message opt_context |> Future.interruptible_task) x;
    8.54  
    8.55  fun toplevel_error output_exn f x = f x
    8.56    handle exn =>
     9.1 --- a/src/Pure/Isar/toplevel.ML	Sun Mar 23 16:40:35 2014 +0100
     9.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Mar 24 12:00:17 2014 +0100
     9.3 @@ -29,9 +29,8 @@
     9.4    val interact: bool Unsynchronized.ref
     9.5    val timing: bool Unsynchronized.ref
     9.6    val profiling: int Unsynchronized.ref
     9.7 -  val debug: bool Unsynchronized.ref
     9.8 -  val debugging: ('a -> 'b) -> 'a -> 'b
     9.9 -  val controlled_execution: ('a -> 'b) -> 'a -> 'b
    9.10 +  val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
    9.11 +  val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
    9.12    val program: (unit -> 'a) -> 'a
    9.13    val thread: bool -> (unit -> unit) -> Thread.thread
    9.14    type transition
    9.15 @@ -235,19 +234,18 @@
    9.16  
    9.17  (* controlled execution *)
    9.18  
    9.19 -val debug = Runtime.debug;
    9.20 -fun debugging f = Runtime.debugging ML_Compiler.exn_message f;
    9.21 -fun controlled_execution f = Runtime.controlled_execution ML_Compiler.exn_message f;
    9.22 +fun debugging arg = Runtime.debugging ML_Compiler.exn_message arg;
    9.23 +fun controlled_execution arg = Runtime.controlled_execution ML_Compiler.exn_message arg;
    9.24  
    9.25  fun program body =
    9.26   (body
    9.27 -  |> controlled_execution
    9.28 +  |> controlled_execution NONE
    9.29    |> Runtime.toplevel_error ML_Compiler.exn_error_message) ();
    9.30  
    9.31  fun thread interrupts body =
    9.32    Thread.fork
    9.33      (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
    9.34 -        |> debugging
    9.35 +        |> debugging NONE
    9.36          |> Runtime.toplevel_error
    9.37            (fn exn =>
    9.38              Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
    9.39 @@ -272,11 +270,12 @@
    9.40  fun apply_transaction f g node =
    9.41    let
    9.42      val cont_node = reset_presentation node;
    9.43 +    val context = cases_node I (Context.Proof o Proof.context_of) cont_node;
    9.44      fun state_error e nd = (State (SOME nd, SOME node), e);
    9.45  
    9.46      val (result, err) =
    9.47        cont_node
    9.48 -      |> controlled_execution f
    9.49 +      |> controlled_execution (SOME context) f
    9.50        |> state_error NONE
    9.51        handle exn => state_error (SOME exn) cont_node;
    9.52    in
    9.53 @@ -305,11 +304,11 @@
    9.54  local
    9.55  
    9.56  fun apply_tr _ (Init f) (State (NONE, _)) =
    9.57 -      State (SOME (Theory (Context.Theory (controlled_execution f ()), NONE)), NONE)
    9.58 +      State (SOME (Theory (Context.Theory (controlled_execution NONE f ()), NONE)), NONE)
    9.59    | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
    9.60        exit_transaction state
    9.61    | apply_tr int (Keep f) state =
    9.62 -      controlled_execution (fn x => tap (f int) x) state
    9.63 +      controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
    9.64    | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
    9.65        apply_transaction (fn x => f int x) g state
    9.66    | apply_tr _ _ _ = raise UNDEF;
    10.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Sun Mar 23 16:40:35 2014 +0100
    10.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Mon Mar 24 12:00:17 2014 +0100
    10.3 @@ -78,6 +78,7 @@
    10.4    let
    10.5      val _ = Secure.secure_mltext ();
    10.6      val space = ML_Env.name_space;
    10.7 +    val opt_context = Context.thread_data ();
    10.8  
    10.9  
   10.10      (* input *)
   10.11 @@ -168,7 +169,7 @@
   10.12        | SOME code =>
   10.13            apply_result
   10.14              ((code
   10.15 -              |> Runtime.debugging exn_message
   10.16 +              |> Runtime.debugging exn_message opt_context
   10.17                |> Runtime.toplevel_error (err o exn_message)) ())));
   10.18  
   10.19  
    11.1 --- a/src/Pure/PIDE/command.ML	Sun Mar 23 16:40:35 2014 +0100
    11.2 +++ b/src/Pure/PIDE/command.ML	Mon Mar 24 12:00:17 2014 +0100
    11.3 @@ -271,8 +271,8 @@
    11.4  val print_functions =
    11.5    Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
    11.6  
    11.7 -fun print_error tr e =
    11.8 -  (Toplevel.setmp_thread_position tr o Toplevel.controlled_execution) e ()
    11.9 +fun print_error tr opt_context e =
   11.10 +  (Toplevel.setmp_thread_position tr o Toplevel.controlled_execution opt_context) e ()
   11.11      handle exn =>
   11.12        if Exn.is_interrupt exn then reraise exn
   11.13        else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
   11.14 @@ -298,9 +298,10 @@
   11.15            let
   11.16              val {failed, command, state = st', ...} = eval_result eval;
   11.17              val tr = Toplevel.exec_id exec_id command;
   11.18 +            val opt_context = try Toplevel.generic_theory_of st';
   11.19            in
   11.20              if failed andalso strict then ()
   11.21 -            else print_error tr (fn () => print_fn tr st')
   11.22 +            else print_error tr opt_context (fn () => print_fn tr st')
   11.23            end;
   11.24        in
   11.25          Print {
   11.26 @@ -316,7 +317,7 @@
   11.27        let
   11.28          val params = {command_name = command_name, args = args};
   11.29        in
   11.30 -        (case Exn.capture (Toplevel.controlled_execution get_pr) params of
   11.31 +        (case Exn.capture (Toplevel.controlled_execution NONE get_pr) params of
   11.32            Exn.Res NONE => NONE
   11.33          | Exn.Res (SOME pr) => SOME (make_print name args pr)
   11.34          | Exn.Exn exn => SOME (bad_print name args exn))
    12.1 --- a/src/Pure/System/isabelle_process.ML	Sun Mar 23 16:40:35 2014 +0100
    12.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Mar 24 12:00:17 2014 +0100
    12.3 @@ -48,7 +48,7 @@
    12.4    (case Symtab.lookup (Synchronized.value commands) name of
    12.5      NONE => error ("Undefined Isabelle protocol command " ^ quote name)
    12.6    | SOME cmd =>
    12.7 -      (Toplevel.debugging cmd args handle exn =>
    12.8 +      (Toplevel.debugging NONE cmd args handle exn =>
    12.9          error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^
   12.10            ML_Compiler.exn_message exn)));
   12.11  
    13.1 --- a/src/Pure/Tools/proof_general_pure.ML	Sun Mar 23 16:40:35 2014 +0100
    13.2 +++ b/src/Pure/Tools/proof_general_pure.ML	Mon Mar 24 12:00:17 2014 +0100
    13.3 @@ -121,11 +121,11 @@
    13.4      "Whether to enable timing in Isabelle";
    13.5  
    13.6  val _ =
    13.7 -  ProofGeneral.preference_bool ProofGeneral.category_tracing
    13.8 +  ProofGeneral.preference_option ProofGeneral.category_tracing
    13.9      NONE
   13.10 -    Toplevel.debug
   13.11 +    @{option exception_trace}
   13.12      "debugging"
   13.13 -    "Whether to enable debugging";
   13.14 +    "Whether to enable exception trace for toplevel command execution";
   13.15  
   13.16  val _ =
   13.17    ProofGeneral.preference_bool ProofGeneral.category_tracing