tuned;
authorwenzelm
Mon, 24 Aug 2015 20:08:00 +0200
changeset 61017 a538a03972d2
parent 61016 7c5a877b0f8e
child 61018 32cc7d219c38
tuned;
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