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