# HG changeset patch
# User wenzelm
# Date 1439295216 -7200
# Node ID 7f210887cc4eb743191b917298f1350a88220f16
# Parent  35d85fd89fc1025153261ddef678c08ca55fcced
init/exit depending on active debugger panels;

diff -r 35d85fd89fc1 -r 7f210887cc4e etc/options
--- a/etc/options	Tue Aug 11 13:50:59 2015 +0200
+++ b/etc/options	Tue Aug 11 14:13:36 2015 +0200
@@ -104,9 +104,6 @@
 public option ML_debugger : bool = false
   -- "ML debugger instrumentation for newly compiled code"
 
-public option ML_debugger_active : bool = true
-  -- "ML debugger active at run-time, for code compiled with debugger instrumentation"
-
 public option ML_statistics : bool = true
   -- "ML run-time system statistics"
 
diff -r 35d85fd89fc1 -r 7f210887cc4e src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Tue Aug 11 13:50:59 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Tue Aug 11 14:13:36 2015 +0200
@@ -185,6 +185,8 @@
      (Output.system_message
         ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true));
 
+in
+
 fun debugger_loop thread_name =
   uninterruptible (fn restore_attributes => fn () =>
     let
@@ -194,19 +196,6 @@
       val _ = debugger_state thread_name;
     in Exn.release result end) ();
 
-in
-
-fun init () =
-  ML_Debugger.on_breakpoint
-    (SOME (fn (_, break) =>
-      if not (is_debugging ()) andalso (! break orelse is_stepping ()) andalso
-        Options.default_bool @{system_option ML_debugger_active}
-      then
-        (case Simple_Thread.get_name () of
-          SOME thread_name => debugger_loop thread_name
-        | NONE => ())
-      else ()));
-
 end;
 
 
@@ -215,7 +204,18 @@
 
 val _ =
   Isabelle_Process.protocol_command "Debugger.init"
-    (fn [] => init ());
+    (fn [] =>
+      ML_Debugger.on_breakpoint
+        (SOME (fn (_, break) =>
+          if not (is_debugging ()) andalso (! break orelse is_stepping ()) then
+            (case Simple_Thread.get_name () of
+              SOME thread_name => debugger_loop thread_name
+            | NONE => ())
+          else ())));
+
+val _ =
+  Isabelle_Process.protocol_command "Debugger.exit"
+    (fn [] => ML_Debugger.on_breakpoint NONE);
 
 val _ =
   Isabelle_Process.protocol_command "Debugger.breakpoint"
diff -r 35d85fd89fc1 -r 7f210887cc4e src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Tue Aug 11 13:50:59 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Tue Aug 11 14:13:36 2015 +0200
@@ -26,8 +26,8 @@
     def set_session(new_session: Session): State =
       copy(session = new_session)
 
-    def inc_active: State = copy(active = active + 1)
-    def dec_active: State = copy(active = active - 1)
+    def inc_active: (Boolean, State) = (active == 0, copy(active = active + 1))
+    def dec_active: (Boolean, State) = (active == 1, copy(active = active - 1))
 
     def toggle_breakpoint(breakpoint: Long): (Boolean, State) =
     {
@@ -131,15 +131,26 @@
 
   /* protocol commands */
 
-  def init(session: Session)
-  {
+  def set_session(session: Session): Unit =
     global_state.change(_.set_session(session))
-    current_state().session.protocol_command("Debugger.init")
-  }
 
   def is_active(): Boolean = current_state().active > 0
-  def inc_active(): Unit = global_state.change(_.inc_active)
-  def dec_active(): Unit = global_state.change(_.dec_active)
+
+  def inc_active(): Unit =
+    global_state.change(state =>
+    {
+      val (init, state1) = state.inc_active
+      if (init) state1.session.protocol_command("Debugger.init")
+      state1
+    })
+
+  def dec_active(): Unit =
+    global_state.change(state =>
+    {
+      val (exit, state1) = state.dec_active
+      if (exit) state1.session.protocol_command("Debugger.exit")
+      state1
+    })
 
   def active_breakpoint_state(breakpoint: Long): Option[Boolean] =
   {
diff -r 35d85fd89fc1 -r 7f210887cc4e src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 11 13:50:59 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 11 14:13:36 2015 +0200
@@ -298,19 +298,14 @@
     reactions += { case ButtonClicked(_) => thread_selection().map(Debugger.continue(_)) }
   }
 
-  private val debugger_active =
-    new JEdit_Options.Check_Box("ML_debugger_active", "Active", "Enable debugger at run-time")
-
   private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
 
   private val controls =
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(
       step_button, step_over_button, step_out_button, continue_button,
       context_label, Component.wrap(context_field),
-      expression_label, Component.wrap(expression_field),
-      sml_button, eval_button,
-      pretty_text_area.search_label, pretty_text_area.search_field,
-      debugger_active, zoom)
+      expression_label, Component.wrap(expression_field), sml_button, eval_button,
+      pretty_text_area.search_label, pretty_text_area.search_field, zoom)
   add(controls.peer, BorderLayout.NORTH)
 
 
@@ -345,11 +340,8 @@
   private val main =
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>
-        Debugger.init(PIDE.session)
-        GUI_Thread.later {
-          debugger_active.load()
-          handle_resize()
-        }
+        Debugger.set_session(PIDE.session)
+        GUI_Thread.later { handle_resize() }
 
       case _: Debugger.Update =>
         GUI_Thread.later { handle_update() }
@@ -359,7 +351,7 @@
   {
     PIDE.session.global_options += main
     PIDE.session.debugger_updates += main
-    Debugger.init(PIDE.session)
+    Debugger.set_session(PIDE.session)
     Debugger.inc_active()
     handle_update()
     jEdit.propertiesChanged()