tuned;
authorwenzelm
Tue, 14 Mar 2017 11:22:47 +0100
changeset 65224 68f5ebed961c
parent 65223 844c067bc3d4
child 65225 ec9ec04546fc
tuned;
src/Tools/jEdit/src/debugger_dockable.scala
src/Tools/jEdit/src/isabelle.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 {}
--- 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 */