# HG changeset patch
# User wenzelm
# Date 1439233875 -7200
# Node ID f3039309702e34c0b0b628c74eaeef443878c625
# Parent  8eb8640d7300bf964cefdcbdc394552850d6e918
eliminated global option: breakpoints control this individually;

diff -r 8eb8640d7300 -r f3039309702e etc/options
--- a/etc/options	Mon Aug 10 21:06:10 2015 +0200
+++ b/etc/options	Mon Aug 10 21:11:15 2015 +0200
@@ -107,9 +107,6 @@
 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
-  -- "ML debugger in single-step mode"
-
 public option ML_statistics : bool = true
   -- "ML run-time system statistics"
 
diff -r 8eb8640d7300 -r f3039309702e src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Mon Aug 10 21:06:10 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Mon Aug 10 21:11:15 2015 +0200
@@ -213,8 +213,7 @@
   ML_Debugger.on_breakpoint
     (SOME (fn (_, break) =>
       if not (is_debugging ()) andalso
-        (! break orelse Options.default_bool @{system_option ML_debugger_stepping} orelse
-          is_stepping ()) andalso
+        (! break orelse is_stepping ()) andalso
         Options.default_bool @{system_option ML_debugger_active}
       then
         (case Simple_Thread.get_name () of
diff -r 8eb8640d7300 -r f3039309702e src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 21:06:10 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 21:11:15 2015 +0200
@@ -304,9 +304,6 @@
   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() }
 
   private val controls =
@@ -316,7 +313,7 @@
       expression_label, Component.wrap(expression_field),
       sml_button, eval_button,
       pretty_text_area.search_label, pretty_text_area.search_field,
-      debugger_stepping, debugger_active, zoom)
+      debugger_active, zoom)
   add(controls.peer, BorderLayout.NORTH)
 
 
@@ -354,7 +351,6 @@
         Debugger.init(PIDE.session)
         GUI_Thread.later {
           debugger_active.load()
-          debugger_stepping.load()
           handle_resize()
         }