# HG changeset patch
# User wenzelm
# Date 1440439680 -7200
# Node ID a538a03972d21fec384823b57cf8a5dbe2494dd6
# Parent  7c5a877b0f8ea9450037f8d8bb95aadfae8cee1a
tuned;

diff -r 7c5a877b0f8e -r a538a03972d2 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Aug 24 19:49:17 2015 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Aug 24 20:08:00 2015 +0200
@@ -354,10 +354,10 @@
     if (text_area.isCaretVisible) text_area.getPainter.getCaretColor
     else {
       val debug_positions =
-        for {
-          c <- Debugger.focus()
-          pos <- c.debug_position
-        } yield pos
+        (for {
+          c <- Debugger.focus().iterator
+          pos <- c.debug_position.iterator
+        } yield pos).toList
       if (debug_positions.exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _)))
         rendering.caret_debugger_color
       else rendering.caret_invisible_color