# HG changeset patch
# User wenzelm
# Date 1440368420 -7200
# Node ID 018b0c996b543b614ba255f1ed4643694ec332ef
# Parent  cccfd7f6317d72186cf08797ddec84c3558fa32a
more explicit debugger caret rendering;

diff -r cccfd7f6317d -r 018b0c996b54 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Sun Aug 23 22:47:01 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Mon Aug 24 00:20:20 2015 +0200
@@ -222,6 +222,8 @@
     })
   }
 
+  def focus(): Option[Position.T] = global_state.value.focus
+
   def set_focus(focus: Option[Position.T])
   {
     global_state.change(_.set_focus(focus))
diff -r cccfd7f6317d -r 018b0c996b54 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Sun Aug 23 22:47:01 2015 +0200
+++ b/src/Tools/jEdit/etc/options	Mon Aug 24 00:20:20 2015 +0200
@@ -119,6 +119,7 @@
 option quasi_keyword_color : string = "9966FFFF"
 option improper_color : string = "FF5050FF"
 option operator_color : string = "323232FF"
+option caret_debugger_color : string = "FF9966FF"
 option caret_invisible_color : string = "50000080"
 option completion_color : string = "0000FFFF"
 option search_color : string = "66FFFF64"
diff -r cccfd7f6317d -r 018b0c996b54 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Sun Aug 23 22:47:01 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 24 00:20:20 2015 +0200
@@ -328,6 +328,7 @@
     Debugger.set_focus(focus)
     if (focus.isDefined)
       PIDE.editor.hyperlink_position(false, current_snapshot, focus.get).foreach(_.follow(view))
+    view.getTextArea.repaint()
   }
 
 
diff -r cccfd7f6317d -r 018b0c996b54 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Aug 23 22:47:01 2015 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 24 00:20:20 2015 +0200
@@ -279,6 +279,23 @@
     }
   }
 
+  def is_hyperlink_position(snapshot: Document.Snapshot,
+    text_offset: Text.Offset, pos: Position.T): Boolean =
+  {
+    pos match {
+      case Position.Id_Offset0(id, offset) if offset > 0 =>
+        snapshot.state.find_command(snapshot.version, id) match {
+          case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node =>
+            node.command_start(command) match {
+              case Some(start) => text_offset == start + command.chunk.decode(offset)
+              case None => false
+            }
+          case _ => false
+        }
+      case _ => false
+    }
+  }
+
   def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
       : Option[Hyperlink] =
     pos match {
diff -r cccfd7f6317d -r 018b0c996b54 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sun Aug 23 22:47:01 2015 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 24 00:20:20 2015 +0200
@@ -251,6 +251,7 @@
   val intensify_color = color_value("intensify_color")
   val breakpoint_disabled_color = color_value("breakpoint_disabled_color")
   val breakpoint_enabled_color = color_value("breakpoint_enabled_color")
+  val caret_debugger_color = color_value("caret_debugger_color")
   val quoted_color = color_value("quoted_color")
   val antiquoted_color = color_value("antiquoted_color")
   val antiquote_color = color_value("antiquote_color")
diff -r cccfd7f6317d -r 018b0c996b54 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Aug 23 22:47:01 2015 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Aug 24 00:20:20 2015 +0200
@@ -349,11 +349,13 @@
   private def caret_enabled: Boolean =
     caret_visible && (!text_area.hasFocus || text_area.isCaretVisible)
 
-  private def caret_color(rendering: Rendering): Color =
+  private def caret_color(rendering: Rendering, offset: Text.Offset): Color =
   {
-    if (text_area.isCaretVisible)
-      text_area.getPainter.getCaretColor
-    else rendering.caret_invisible_color
+    if (text_area.isCaretVisible) text_area.getPainter.getCaretColor
+    else
+      if (Debugger.focus().exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _)))
+        rendering.caret_debugger_color
+      else rendering.caret_invisible_color
   }
 
   private def paint_chunk_list(rendering: Rendering,
@@ -416,7 +418,7 @@
 
               val astr = new AttributedString(s2)
               astr.addAttribute(TextAttribute.FONT, chunk_font)
-              astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering))
+              astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, r.start))
               astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
               gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
 
@@ -604,7 +606,7 @@
 
             val astr = new AttributedString(" ")
             astr.addAttribute(TextAttribute.FONT, painter.getFont)
-            astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering))
+            astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, caret))
             astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
 
             val clip = gfx.getClip