src/Tools/jEdit/src/debugger_dockable.scala
changeset 60876 52edced9cce5
parent 60875 ee23c1d21ac3
child 60878 1f0d2bbcf38b
     1.1 --- a/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 14:14:49 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 16:05:41 2015 +0200
     1.3 @@ -325,7 +325,9 @@
     1.4      PIDE.session.global_options += main
     1.5      PIDE.session.debugger_updates += main
     1.6      Debugger.init(PIDE.session)
     1.7 +    Debugger.inc_active()
     1.8      handle_update()
     1.9 +    jEdit.propertiesChanged()
    1.10    }
    1.11  
    1.12    override def exit()
    1.13 @@ -334,6 +336,8 @@
    1.14      PIDE.session.debugger_updates -= main
    1.15      delay_resize.revoke()
    1.16      update_focus(None)
    1.17 +    Debugger.dec_active()
    1.18 +    jEdit.propertiesChanged()
    1.19    }
    1.20  
    1.21