more thorough GUI update;
authorwenzelm
Mon, 24 Aug 2015 11:45:26 +0200
changeset 61015 2c34ab15e3eb
parent 61014 39f67bb4e609
child 61016 7c5a877b0f8e
more thorough GUI update;
src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 24 11:38:05 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 24 11:45:26 2015 +0200
@@ -323,11 +323,9 @@
       for {
         pos <- c.debug_position
         link <- PIDE.editor.hyperlink_position(false, current_snapshot, pos)
-      } {
-        link.follow(view)
-        view.getTextArea.repaint()
-      }
+      } link.follow(view)
     }
+    JEdit_Lib.jedit_text_areas(view.getBuffer).foreach(_.repaint())
   }