--- a/src/Tools/jEdit/src/debugger_dockable.scala Tue Aug 11 14:13:36 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Tue Aug 11 14:21:00 2015 +0200
@@ -67,7 +67,7 @@
/* context menu */
def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] =
- if (get_breakpoint(text_area, offset).isDefined) {
+ if (Debugger.is_active() && get_breakpoint(text_area, offset).isDefined) {
val context = jEdit.getActionContext()
val name = "isabelle.toggle-breakpoint"
List(new EnhancedMenuItem(context.getAction(name).getLabel, name, context))
--- a/src/Tools/jEdit/src/isabelle.scala Tue Aug 11 14:13:36 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Tue Aug 11 14:21:00 2015 +0200
@@ -348,12 +348,12 @@
/* debugger */
- def toggle_breakpoint(text_area: JEditTextArea)
- {
- for {
- (command, serial) <- Debugger_Dockable.get_breakpoint(text_area, text_area.getCaretPosition)
- } Debugger_Dockable.toggle_breakpoint(command, serial)
- }
+ def toggle_breakpoint(text_area: JEditTextArea): Unit =
+ if (Debugger.is_active()) {
+ for {
+ (command, serial) <- Debugger_Dockable.get_breakpoint(text_area, text_area.getCaretPosition)
+ } Debugger_Dockable.toggle_breakpoint(command, serial)
+ }
/* plugin options */