more controls;
authorwenzelm
Wed Aug 05 16:22:56 2015 +0200 (2015-08-05)
changeset 60845c4cb46e3cdd1
parent 60844 f7f2bc0e4293
child 60846 a7e3f11c19b7
more controls;
etc/options
src/Tools/jEdit/src/debugger_dockable.scala
     1.1 --- a/etc/options	Wed Aug 05 16:22:40 2015 +0200
     1.2 +++ b/etc/options	Wed Aug 05 16:22:56 2015 +0200
     1.3 @@ -104,7 +104,7 @@
     1.4  public option ML_debugger : bool = false
     1.5    -- "ML debugger instrumentation for newly compiled code"
     1.6  
     1.7 -public option ML_debugger_active : bool = false
     1.8 +public option ML_debugger_active : bool = true
     1.9    -- "ML debugger active at run-time, for code compiled with debugger instrumentation"
    1.10  
    1.11  public option ML_debugger_stepping : bool = false
     2.1 --- a/src/Tools/jEdit/src/debugger_dockable.scala	Wed Aug 05 16:22:40 2015 +0200
     2.2 +++ b/src/Tools/jEdit/src/debugger_dockable.scala	Wed Aug 05 16:22:56 2015 +0200
     2.3 @@ -68,6 +68,15 @@
     2.4        quote(expression_field.getText))
     2.5    }
     2.6  
     2.7 +
     2.8 +  /* controls */
     2.9 +
    2.10 +  private val debugger_active =
    2.11 +    new JEdit_Options.Check_Box("ML_debugger_active", "Active", "Enable debugger at run-time")
    2.12 +
    2.13 +  private val debugger_stepping =
    2.14 +    new JEdit_Options.Check_Box("ML_debugger_stepping", "Stepping", "Enable single-step mode")
    2.15 +
    2.16    private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
    2.17  
    2.18  
    2.19 @@ -110,7 +119,11 @@
    2.20      Session.Consumer[Any](getClass.getName) {
    2.21        case _: Session.Global_Options =>
    2.22          Debugger.init(PIDE.session)
    2.23 -        GUI_Thread.later { handle_resize() }
    2.24 +        GUI_Thread.later {
    2.25 +          debugger_active.load()
    2.26 +          debugger_stepping.load()
    2.27 +          handle_resize()
    2.28 +        }
    2.29  
    2.30        case _: Debugger.Update =>
    2.31          GUI_Thread.later { handle_update() }
    2.32 @@ -149,6 +162,7 @@
    2.33      new Wrap_Panel(Wrap_Panel.Alignment.Right)(
    2.34        context_label, Component.wrap(context_field),
    2.35        expression_label, Component.wrap(expression_field), eval_button,
    2.36 -      pretty_text_area.search_label, pretty_text_area.search_field, zoom)
    2.37 +      pretty_text_area.search_label, pretty_text_area.search_field,
    2.38 +      debugger_stepping, debugger_active, zoom)
    2.39    add(controls.peer, BorderLayout.NORTH)
    2.40  }