background color for entity def/ref focus;
authorwenzelm
Thu Apr 14 22:55:53 2016 +0200 (2016-04-14)
changeset 629869d2fae6b31cc
parent 62985 4be23c432491
child 62987 dc8a8a7559e7
background color for entity def/ref focus;
src/Pure/PIDE/markup.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Pure/PIDE/markup.scala	Thu Apr 14 20:47:44 2016 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Thu Apr 14 22:55:53 2016 +0200
     1.3 @@ -86,11 +86,12 @@
     1.4  
     1.5    val BINDING = "binding"
     1.6    val ENTITY = "entity"
     1.7 -  val DEF = "def"
     1.8 -  val REF = "ref"
     1.9  
    1.10    object Entity
    1.11    {
    1.12 +    val Def = new Properties.Long("def")
    1.13 +    val Ref = new Properties.Long("ref")
    1.14 +
    1.15      def unapply(markup: Markup): Option[(String, String)] =
    1.16        markup match {
    1.17          case Markup(ENTITY, props) =>
     2.1 --- a/src/Tools/jEdit/etc/options	Thu Apr 14 20:47:44 2016 +0200
     2.2 +++ b/src/Tools/jEdit/etc/options	Thu Apr 14 22:55:53 2016 +0200
     2.3 @@ -99,6 +99,8 @@
     2.4  option spell_checker_color : string = "0000FFFF"
     2.5  option bad_color : string = "FF6A6A64"
     2.6  option intensify_color : string = "FFCC6664"
     2.7 +option entity_def_color : string = "CCD9FFA0"
     2.8 +option entity_ref_color : string = "E6FFCCA0"
     2.9  option breakpoint_disabled_color : string = "CCCC0080"
    2.10  option breakpoint_enabled_color : string = "FF9966FF"
    2.11  option quoted_color : string = "8B8B8B19"
     3.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Apr 14 20:47:44 2016 +0200
     3.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu Apr 14 22:55:53 2016 +0200
     3.3 @@ -185,6 +185,7 @@
     3.4    private val delay_caret_update =
     3.5      GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
     3.6        session.caret_focus.post(Session.Caret_Focus)
     3.7 +      JEdit_Lib.invalidate(text_area)
     3.8      }
     3.9  
    3.10    private val caret_listener = new CaretListener {
    3.11 @@ -219,26 +220,7 @@
    3.12                     changed.commands.exists(snapshot.node.commands.contains)))
    3.13                  text_overview.invoke()
    3.14  
    3.15 -              val visible_lines = text_area.getVisibleLines
    3.16 -              if (visible_lines > 0) {
    3.17 -                if (changed.assignment || load_changed)
    3.18 -                  text_area.invalidateScreenLineRange(0, visible_lines)
    3.19 -                else {
    3.20 -                  val visible_range = JEdit_Lib.visible_range(text_area).get
    3.21 -                  val visible_iterator =
    3.22 -                    snapshot.node.command_iterator(snapshot.revert(visible_range)).map(_._1)
    3.23 -                  if (visible_iterator.exists(changed.commands)) {
    3.24 -                    for {
    3.25 -                      line <- (0 until visible_lines).iterator
    3.26 -                      start = text_area.getScreenLineStartOffset(line) if start >= 0
    3.27 -                      end = text_area.getScreenLineEndOffset(line) if end >= 0
    3.28 -                      range = Text.Range(start, end)
    3.29 -                      line_cmds = snapshot.node.command_iterator(snapshot.revert(range)).map(_._1)
    3.30 -                      if line_cmds.exists(changed.commands)
    3.31 -                    } text_area.invalidateScreenLineRange(line, line)
    3.32 -                  }
    3.33 -                }
    3.34 -              }
    3.35 +              JEdit_Lib.invalidate(text_area)
    3.36              }
    3.37            }
    3.38          }
     4.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Apr 14 20:47:44 2016 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Thu Apr 14 22:55:53 2016 +0200
     4.3 @@ -234,6 +234,12 @@
     4.4      }
     4.5    }
     4.6  
     4.7 +  def invalidate(text_area: TextArea)
     4.8 +  {
     4.9 +    val visible_lines = text_area.getVisibleLines
    4.10 +    if (visible_lines > 0) text_area.invalidateScreenLineRange(0, visible_lines)
    4.11 +  }
    4.12 +
    4.13  
    4.14    /* graphics range */
    4.15  
     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Apr 14 20:47:44 2016 +0200
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Apr 14 22:55:53 2016 +0200
     5.3 @@ -151,6 +151,8 @@
     5.4  
     5.5    private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT)
     5.6  
     5.7 +  private val caret_focus_elements = Markup.Elements(Markup.ENTITY)
     5.8 +
     5.9    private val highlight_elements =
    5.10      Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
    5.11        Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING,
    5.12 @@ -206,7 +208,8 @@
    5.13        Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
    5.14        Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
    5.15        Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
    5.16 -      Markup.BAD + Markup.INTENSIFY + Markup.Markdown_Item.name ++ active_elements
    5.17 +      Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
    5.18 +      Markup.Markdown_Item.name ++ active_elements
    5.19  
    5.20    private val foreground_elements =
    5.21      Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
    5.22 @@ -250,6 +253,8 @@
    5.23    val spell_checker_color = color_value("spell_checker_color")
    5.24    val bad_color = color_value("bad_color")
    5.25    val intensify_color = color_value("intensify_color")
    5.26 +  val entity_def_color = color_value("entity_def_color")
    5.27 +  val entity_ref_color = color_value("entity_ref_color")
    5.28    val breakpoint_disabled_color = color_value("breakpoint_disabled_color")
    5.29    val breakpoint_enabled_color = color_value("breakpoint_enabled_color")
    5.30    val caret_debugger_color = color_value("caret_debugger_color")
    5.31 @@ -392,6 +397,37 @@
    5.32    }
    5.33  
    5.34  
    5.35 +  /* caret focus */
    5.36 +
    5.37 +  def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
    5.38 +  {
    5.39 +    val focus_results =
    5.40 +      snapshot.cumulate[Set[Long]](caret_range, Set.empty, Rendering.caret_focus_elements, _ =>
    5.41 +          {
    5.42 +            case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
    5.43 +              props match {
    5.44 +                case Markup.Entity.Def(i) => Some(serials + i)
    5.45 +                case Markup.Entity.Ref(i) => Some(serials + i)
    5.46 +                case _ => None
    5.47 +              }
    5.48 +            case _ => None
    5.49 +          })
    5.50 +    val focus = (Set.empty[Long] /: focus_results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
    5.51 +
    5.52 +    val visible =
    5.53 +      focus.nonEmpty &&
    5.54 +        snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ =>
    5.55 +            {
    5.56 +              case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
    5.57 +                props match {
    5.58 +                  case Markup.Entity.Def(i) if focus(i) => Some(true)
    5.59 +                  case _ => None
    5.60 +                }
    5.61 +            }).exists({ case Text.Info(_, visible) => visible })
    5.62 +    if (visible) focus else Set.empty[Long]
    5.63 +  }
    5.64 +
    5.65 +
    5.66    /* highlighted area */
    5.67  
    5.68    def highlight(range: Text.Range): Option[Text.Info[Color]] =
    5.69 @@ -697,7 +733,7 @@
    5.70  
    5.71    /* text background */
    5.72  
    5.73 -  def background(range: Text.Range): List[Text.Info[Color]] =
    5.74 +  def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] =
    5.75    {
    5.76      for {
    5.77        Text.Info(r, result) <-
    5.78 @@ -712,6 +748,14 @@
    5.79                  Some((Nil, Some(bad_color)))
    5.80                case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
    5.81                  Some((Nil, Some(intensify_color)))
    5.82 +              case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
    5.83 +                props match {
    5.84 +                  case Markup.Entity.Def(i) if focus(i) =>
    5.85 +                    Some((Nil, Some(entity_def_color)))
    5.86 +                  case Markup.Entity.Ref(i) if focus(i) =>
    5.87 +                    Some((Nil, Some(entity_ref_color)))
    5.88 +                  case _ => None
    5.89 +                }
    5.90                case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) =>
    5.91                  val color =
    5.92                    depth match {
     6.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Thu Apr 14 20:47:44 2016 +0200
     6.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Thu Apr 14 22:55:53 2016 +0200
     6.3 @@ -280,6 +280,13 @@
     6.4        robust_rendering { rendering =>
     6.5          val fm = text_area.getPainter.getFontMetrics
     6.6  
     6.7 +        val focus =
     6.8 +          JEdit_Lib.visible_range(text_area) match {
     6.9 +            case Some(visible_range) if caret_enabled =>
    6.10 +              rendering.caret_focus(JEdit_Lib.caret_range(text_area), visible_range)
    6.11 +            case _ => Set.empty[Long]
    6.12 +          }
    6.13 +
    6.14          for (i <- 0 until physical_lines.length) {
    6.15            if (physical_lines(i) != -1) {
    6.16              val line_range = Text.Range(start(i), end(i) min buffer.getLength)
    6.17 @@ -294,7 +301,7 @@
    6.18  
    6.19              // background color
    6.20              for {
    6.21 -              Text.Info(range, color) <- rendering.background(line_range)
    6.22 +              Text.Info(range, color) <- rendering.background(line_range, focus)
    6.23                r <- JEdit_Lib.gfx_range(text_area, range)
    6.24              } {
    6.25                gfx.setColor(color)