# HG changeset patch
# User wenzelm
# Date 1440409526 -7200
# Node ID 2c34ab15e3ebc25ae1ce93036a7dc9357a31571a
# Parent  39f67bb4e609bcc6c372a1442054ff54779a3c97
more thorough GUI update;

diff -r 39f67bb4e609 -r 2c34ab15e3eb 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())
   }