--- 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 */