more explicit debugger caret rendering;
authorwenzelm
Mon Aug 24 00:20:20 2015 +0200 (2015-08-24)
changeset 61011018b0c996b54
parent 61010 cccfd7f6317d
child 61012 40a0a4077126
child 61014 39f67bb4e609
more explicit debugger caret rendering;
src/Pure/Tools/debugger.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/debugger_dockable.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Pure/Tools/debugger.scala	Sun Aug 23 22:47:01 2015 +0200
     1.2 +++ b/src/Pure/Tools/debugger.scala	Mon Aug 24 00:20:20 2015 +0200
     1.3 @@ -222,6 +222,8 @@
     1.4      })
     1.5    }
     1.6  
     1.7 +  def focus(): Option[Position.T] = global_state.value.focus
     1.8 +
     1.9    def set_focus(focus: Option[Position.T])
    1.10    {
    1.11      global_state.change(_.set_focus(focus))
     2.1 --- a/src/Tools/jEdit/etc/options	Sun Aug 23 22:47:01 2015 +0200
     2.2 +++ b/src/Tools/jEdit/etc/options	Mon Aug 24 00:20:20 2015 +0200
     2.3 @@ -119,6 +119,7 @@
     2.4  option quasi_keyword_color : string = "9966FFFF"
     2.5  option improper_color : string = "FF5050FF"
     2.6  option operator_color : string = "323232FF"
     2.7 +option caret_debugger_color : string = "FF9966FF"
     2.8  option caret_invisible_color : string = "50000080"
     2.9  option completion_color : string = "0000FFFF"
    2.10  option search_color : string = "66FFFF64"
     3.1 --- a/src/Tools/jEdit/src/debugger_dockable.scala	Sun Aug 23 22:47:01 2015 +0200
     3.2 +++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 24 00:20:20 2015 +0200
     3.3 @@ -328,6 +328,7 @@
     3.4      Debugger.set_focus(focus)
     3.5      if (focus.isDefined)
     3.6        PIDE.editor.hyperlink_position(false, current_snapshot, focus.get).foreach(_.follow(view))
     3.7 +    view.getTextArea.repaint()
     3.8    }
     3.9  
    3.10  
     4.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Aug 23 22:47:01 2015 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 24 00:20:20 2015 +0200
     4.3 @@ -279,6 +279,23 @@
     4.4      }
     4.5    }
     4.6  
     4.7 +  def is_hyperlink_position(snapshot: Document.Snapshot,
     4.8 +    text_offset: Text.Offset, pos: Position.T): Boolean =
     4.9 +  {
    4.10 +    pos match {
    4.11 +      case Position.Id_Offset0(id, offset) if offset > 0 =>
    4.12 +        snapshot.state.find_command(snapshot.version, id) match {
    4.13 +          case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node =>
    4.14 +            node.command_start(command) match {
    4.15 +              case Some(start) => text_offset == start + command.chunk.decode(offset)
    4.16 +              case None => false
    4.17 +            }
    4.18 +          case _ => false
    4.19 +        }
    4.20 +      case _ => false
    4.21 +    }
    4.22 +  }
    4.23 +
    4.24    def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
    4.25        : Option[Hyperlink] =
    4.26      pos match {
     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Sun Aug 23 22:47:01 2015 +0200
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 24 00:20:20 2015 +0200
     5.3 @@ -251,6 +251,7 @@
     5.4    val intensify_color = color_value("intensify_color")
     5.5    val breakpoint_disabled_color = color_value("breakpoint_disabled_color")
     5.6    val breakpoint_enabled_color = color_value("breakpoint_enabled_color")
     5.7 +  val caret_debugger_color = color_value("caret_debugger_color")
     5.8    val quoted_color = color_value("quoted_color")
     5.9    val antiquoted_color = color_value("antiquoted_color")
    5.10    val antiquote_color = color_value("antiquote_color")
     6.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Aug 23 22:47:01 2015 +0200
     6.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Aug 24 00:20:20 2015 +0200
     6.3 @@ -349,11 +349,13 @@
     6.4    private def caret_enabled: Boolean =
     6.5      caret_visible && (!text_area.hasFocus || text_area.isCaretVisible)
     6.6  
     6.7 -  private def caret_color(rendering: Rendering): Color =
     6.8 +  private def caret_color(rendering: Rendering, offset: Text.Offset): Color =
     6.9    {
    6.10 -    if (text_area.isCaretVisible)
    6.11 -      text_area.getPainter.getCaretColor
    6.12 -    else rendering.caret_invisible_color
    6.13 +    if (text_area.isCaretVisible) text_area.getPainter.getCaretColor
    6.14 +    else
    6.15 +      if (Debugger.focus().exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _)))
    6.16 +        rendering.caret_debugger_color
    6.17 +      else rendering.caret_invisible_color
    6.18    }
    6.19  
    6.20    private def paint_chunk_list(rendering: Rendering,
    6.21 @@ -416,7 +418,7 @@
    6.22  
    6.23                val astr = new AttributedString(s2)
    6.24                astr.addAttribute(TextAttribute.FONT, chunk_font)
    6.25 -              astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering))
    6.26 +              astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, r.start))
    6.27                astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
    6.28                gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
    6.29  
    6.30 @@ -604,7 +606,7 @@
    6.31  
    6.32              val astr = new AttributedString(" ")
    6.33              astr.addAttribute(TextAttribute.FONT, painter.getFont)
    6.34 -            astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering))
    6.35 +            astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering, caret))
    6.36              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
    6.37  
    6.38              val clip = gfx.getClip