eliminated global option: breakpoints control this individually;
authorwenzelm
Mon Aug 10 21:11:15 2015 +0200 (2015-08-10)
changeset 60884f3039309702e
parent 60883 8eb8640d7300
child 60885 d8d51f956f05
eliminated global option: breakpoints control this individually;
etc/options
src/Pure/Tools/debugger.ML
src/Tools/jEdit/src/debugger_dockable.scala
     1.1 --- a/etc/options	Mon Aug 10 21:06:10 2015 +0200
     1.2 +++ b/etc/options	Mon Aug 10 21:11:15 2015 +0200
     1.3 @@ -107,9 +107,6 @@
     1.4  public option ML_debugger_active : bool = true
     1.5    -- "ML debugger active at run-time, for code compiled with debugger instrumentation"
     1.6  
     1.7 -public option ML_debugger_stepping : bool = false
     1.8 -  -- "ML debugger in single-step mode"
     1.9 -
    1.10  public option ML_statistics : bool = true
    1.11    -- "ML run-time system statistics"
    1.12  
     2.1 --- a/src/Pure/Tools/debugger.ML	Mon Aug 10 21:06:10 2015 +0200
     2.2 +++ b/src/Pure/Tools/debugger.ML	Mon Aug 10 21:11:15 2015 +0200
     2.3 @@ -213,8 +213,7 @@
     2.4    ML_Debugger.on_breakpoint
     2.5      (SOME (fn (_, break) =>
     2.6        if not (is_debugging ()) andalso
     2.7 -        (! break orelse Options.default_bool @{system_option ML_debugger_stepping} orelse
     2.8 -          is_stepping ()) andalso
     2.9 +        (! break orelse is_stepping ()) andalso
    2.10          Options.default_bool @{system_option ML_debugger_active}
    2.11        then
    2.12          (case Simple_Thread.get_name () of
     3.1 --- a/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 21:06:10 2015 +0200
     3.2 +++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 21:11:15 2015 +0200
     3.3 @@ -304,9 +304,6 @@
     3.4    private val debugger_active =
     3.5      new JEdit_Options.Check_Box("ML_debugger_active", "Active", "Enable debugger at run-time")
     3.6  
     3.7 -  private val debugger_stepping =
     3.8 -    new JEdit_Options.Check_Box("ML_debugger_stepping", "Stepping", "Enable single-step mode")
     3.9 -
    3.10    private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
    3.11  
    3.12    private val controls =
    3.13 @@ -316,7 +313,7 @@
    3.14        expression_label, Component.wrap(expression_field),
    3.15        sml_button, eval_button,
    3.16        pretty_text_area.search_label, pretty_text_area.search_field,
    3.17 -      debugger_stepping, debugger_active, zoom)
    3.18 +      debugger_active, zoom)
    3.19    add(controls.peer, BorderLayout.NORTH)
    3.20  
    3.21  
    3.22 @@ -354,7 +351,6 @@
    3.23          Debugger.init(PIDE.session)
    3.24          GUI_Thread.later {
    3.25            debugger_active.load()
    3.26 -          debugger_stepping.load()
    3.27            handle_resize()
    3.28          }
    3.29