# HG changeset patch
# User wenzelm
# Date 1438784576 -7200
# Node ID c4cb46e3cdd1a8ebc21369817bbbd7a64590df60
# Parent  f7f2bc0e4293d7cf937861661ca6c28e068d6b75
more controls;

diff -r f7f2bc0e4293 -r c4cb46e3cdd1 etc/options
--- a/etc/options	Wed Aug 05 16:22:40 2015 +0200
+++ b/etc/options	Wed Aug 05 16:22:56 2015 +0200
@@ -104,7 +104,7 @@
 public option ML_debugger : bool = false
   -- "ML debugger instrumentation for newly compiled code"
 
-public option ML_debugger_active : bool = false
+public option ML_debugger_active : bool = true
   -- "ML debugger active at run-time, for code compiled with debugger instrumentation"
 
 public option ML_debugger_stepping : bool = false
diff -r f7f2bc0e4293 -r c4cb46e3cdd1 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Wed Aug 05 16:22:40 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Wed Aug 05 16:22:56 2015 +0200
@@ -68,6 +68,15 @@
       quote(expression_field.getText))
   }
 
+
+  /* controls */
+
+  private val debugger_active =
+    new JEdit_Options.Check_Box("ML_debugger_active", "Active", "Enable debugger at run-time")
+
+  private val debugger_stepping =
+    new JEdit_Options.Check_Box("ML_debugger_stepping", "Stepping", "Enable single-step mode")
+
   private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
 
 
@@ -110,7 +119,11 @@
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>
         Debugger.init(PIDE.session)
-        GUI_Thread.later { handle_resize() }
+        GUI_Thread.later {
+          debugger_active.load()
+          debugger_stepping.load()
+          handle_resize()
+        }
 
       case _: Debugger.Update =>
         GUI_Thread.later { handle_update() }
@@ -149,6 +162,7 @@
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(
       context_label, Component.wrap(context_field),
       expression_label, Component.wrap(expression_field), eval_button,
-      pretty_text_area.search_label, pretty_text_area.search_field, zoom)
+      pretty_text_area.search_label, pretty_text_area.search_field,
+      debugger_stepping, debugger_active, zoom)
   add(controls.peer, BorderLayout.NORTH)
 }