# HG changeset patch
# User wenzelm
# Date 1489486967 -3600
# Node ID 68f5ebed961cb29e1fbe30ae175138d0e79a54e3
# Parent  844c067bc3d4e8a784192bbde1607f80a9f9c9fe
tuned;

diff -r 844c067bc3d4 -r 68f5ebed961c src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Tue Mar 14 11:16:23 2017 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Tue Mar 14 11:22:47 2017 +0100
@@ -30,14 +30,6 @@
 {
   /* breakpoints */
 
-  def toggle_breakpoint(command: Command, breakpoint: Long)
-  {
-    GUI_Thread.require {}
-
-    PIDE.debugger.toggle_breakpoint(command, breakpoint)
-    jEdit.propertiesChanged()
-  }
-
   def get_breakpoint(text_area: JEditTextArea, offset: Text.Offset): Option[(Command, Long)] =
   {
     GUI_Thread.require {}
diff -r 844c067bc3d4 -r 68f5ebed961c src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Tue Mar 14 11:16:23 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Mar 14 11:22:47 2017 +0100
@@ -439,11 +439,18 @@
   /* debugger */
 
   def toggle_breakpoint(text_area: JEditTextArea): Unit =
+  {
+    GUI_Thread.require {}
+
     if (PIDE.debugger.is_active()) {
-      for {
-        (command, serial) <- Debugger_Dockable.get_breakpoint(text_area, text_area.getCaretPosition)
-      } Debugger_Dockable.toggle_breakpoint(command, serial)
+      Debugger_Dockable.get_breakpoint(text_area, text_area.getCaretPosition) match {
+        case Some((command, breakpoint)) =>
+          PIDE.debugger.toggle_breakpoint(command, breakpoint)
+          jEdit.propertiesChanged()
+        case None =>
+      }
     }
+  }
 
 
   /* plugin options */