GUI actions depend on active debugger;
authorwenzelm
Tue, 11 Aug 2015 14:21:00 +0200
changeset 60890 e2aeaa397e93
parent 60889 7f210887cc4e
child 60891 89b7c84b0480
GUI actions depend on active debugger;
src/Tools/jEdit/src/debugger_dockable.scala
src/Tools/jEdit/src/isabelle.scala
--- 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 */