# HG changeset patch
# User wenzelm
# Date 1395658817 -3600
# Node ID 785569927666eea41564a4e8e3d18c71bf8970b4
# Parent  3d79c132e657ebbf44be57b73167b1b5c4091de3
discontinued Toplevel.debug in favour of system option "exception_trace";

diff -r 3d79c132e657 -r 785569927666 NEWS
--- 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 ***
 
diff -r 3d79c132e657 -r 785569927666 etc/options
--- 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"
 
diff -r 3d79c132e657 -r 785569927666 src/Doc/IsarImplementation/Integration.thy
--- 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.
 
diff -r 3d79c132e657 -r 785569927666 src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
--- 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"
diff -r 3d79c132e657 -r 785569927666 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
--- 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)
 *}
diff -r 3d79c132e657 -r 785569927666 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
--- 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 *)
diff -r 3d79c132e657 -r 785569927666 src/Pure/Isar/attrib.ML
--- 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 #>
diff -r 3d79c132e657 -r 785569927666 src/Pure/Isar/runtime.ML
--- 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 =>
diff -r 3d79c132e657 -r 785569927666 src/Pure/Isar/toplevel.ML
--- 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;
diff -r 3d79c132e657 -r 785569927666 src/Pure/ML/ml_compiler_polyml.ML
--- 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)) ())));
 
 
diff -r 3d79c132e657 -r 785569927666 src/Pure/PIDE/command.ML
--- 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))
diff -r 3d79c132e657 -r 785569927666 src/Pure/System/isabelle_process.ML
--- 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)));
 
diff -r 3d79c132e657 -r 785569927666 src/Pure/Tools/proof_general_pure.ML
--- 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