# HG changeset patch
# User wenzelm
# Date 1439295660 -7200
# Node ID e2aeaa397e93532d2b0c19ab66f8a040b53394eb
# Parent  7f210887cc4eb743191b917298f1350a88220f16
GUI actions depend on active debugger;

diff -r 7f210887cc4e -r e2aeaa397e93 src/Tools/jEdit/src/debugger_dockable.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))
diff -r 7f210887cc4e -r e2aeaa397e93 src/Tools/jEdit/src/isabelle.scala
--- 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 */