# HG changeset patch # User wenzelm # Date 1460667353 -7200 # Node ID 9d2fae6b31ccb3bc985ce9cc519ae8207415d46d # Parent 4be23c432491dde28494334d3cfe0fa8e89f8727 background color for entity def/ref focus; diff -r 4be23c432491 -r 9d2fae6b31cc src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Thu Apr 14 20:47:44 2016 +0200 +++ b/src/Pure/PIDE/markup.scala Thu Apr 14 22:55:53 2016 +0200 @@ -86,11 +86,12 @@ val BINDING = "binding" val ENTITY = "entity" - val DEF = "def" - val REF = "ref" object Entity { + val Def = new Properties.Long("def") + val Ref = new Properties.Long("ref") + def unapply(markup: Markup): Option[(String, String)] = markup match { case Markup(ENTITY, props) => diff -r 4be23c432491 -r 9d2fae6b31cc src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Thu Apr 14 20:47:44 2016 +0200 +++ b/src/Tools/jEdit/etc/options Thu Apr 14 22:55:53 2016 +0200 @@ -99,6 +99,8 @@ option spell_checker_color : string = "0000FFFF" option bad_color : string = "FF6A6A64" option intensify_color : string = "FFCC6664" +option entity_def_color : string = "CCD9FFA0" +option entity_ref_color : string = "E6FFCCA0" option breakpoint_disabled_color : string = "CCCC0080" option breakpoint_enabled_color : string = "FF9966FF" option quoted_color : string = "8B8B8B19" diff -r 4be23c432491 -r 9d2fae6b31cc src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Thu Apr 14 20:47:44 2016 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Thu Apr 14 22:55:53 2016 +0200 @@ -185,6 +185,7 @@ private val delay_caret_update = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { session.caret_focus.post(Session.Caret_Focus) + JEdit_Lib.invalidate(text_area) } private val caret_listener = new CaretListener { @@ -219,26 +220,7 @@ changed.commands.exists(snapshot.node.commands.contains))) text_overview.invoke() - val visible_lines = text_area.getVisibleLines - if (visible_lines > 0) { - if (changed.assignment || load_changed) - text_area.invalidateScreenLineRange(0, visible_lines) - else { - val visible_range = JEdit_Lib.visible_range(text_area).get - val visible_iterator = - snapshot.node.command_iterator(snapshot.revert(visible_range)).map(_._1) - if (visible_iterator.exists(changed.commands)) { - for { - line <- (0 until visible_lines).iterator - start = text_area.getScreenLineStartOffset(line) if start >= 0 - end = text_area.getScreenLineEndOffset(line) if end >= 0 - range = Text.Range(start, end) - line_cmds = snapshot.node.command_iterator(snapshot.revert(range)).map(_._1) - if line_cmds.exists(changed.commands) - } text_area.invalidateScreenLineRange(line, line) - } - } - } + JEdit_Lib.invalidate(text_area) } } } diff -r 4be23c432491 -r 9d2fae6b31cc src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Thu Apr 14 20:47:44 2016 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Thu Apr 14 22:55:53 2016 +0200 @@ -234,6 +234,12 @@ } } + def invalidate(text_area: TextArea) + { + val visible_lines = text_area.getVisibleLines + if (visible_lines > 0) text_area.invalidateScreenLineRange(0, visible_lines) + } + /* graphics range */ diff -r 4be23c432491 -r 9d2fae6b31cc src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Thu Apr 14 20:47:44 2016 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Thu Apr 14 22:55:53 2016 +0200 @@ -151,6 +151,8 @@ private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT) + private val caret_focus_elements = Markup.Elements(Markup.ENTITY) + private val highlight_elements = Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING, @@ -206,7 +208,8 @@ Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE + Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE + Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE + - Markup.BAD + Markup.INTENSIFY + Markup.Markdown_Item.name ++ active_elements + Markup.BAD + Markup.INTENSIFY + Markup.ENTITY + + Markup.Markdown_Item.name ++ active_elements private val foreground_elements = Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM, @@ -250,6 +253,8 @@ val spell_checker_color = color_value("spell_checker_color") val bad_color = color_value("bad_color") val intensify_color = color_value("intensify_color") + val entity_def_color = color_value("entity_def_color") + val entity_ref_color = color_value("entity_ref_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") @@ -392,6 +397,37 @@ } + /* caret focus */ + + def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] = + { + val focus_results = + snapshot.cumulate[Set[Long]](caret_range, Set.empty, Rendering.caret_focus_elements, _ => + { + case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) => + props match { + case Markup.Entity.Def(i) => Some(serials + i) + case Markup.Entity.Ref(i) => Some(serials + i) + case _ => None + } + case _ => None + }) + val focus = (Set.empty[Long] /: focus_results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 } + + val visible = + focus.nonEmpty && + snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ => + { + case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) => + props match { + case Markup.Entity.Def(i) if focus(i) => Some(true) + case _ => None + } + }).exists({ case Text.Info(_, visible) => visible }) + if (visible) focus else Set.empty[Long] + } + + /* highlighted area */ def highlight(range: Text.Range): Option[Text.Info[Color]] = @@ -697,7 +733,7 @@ /* text background */ - def background(range: Text.Range): List[Text.Info[Color]] = + def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] = { for { Text.Info(r, result) <- @@ -712,6 +748,14 @@ Some((Nil, Some(bad_color))) case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) => Some((Nil, Some(intensify_color))) + case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) => + props match { + case Markup.Entity.Def(i) if focus(i) => + Some((Nil, Some(entity_def_color))) + case Markup.Entity.Ref(i) if focus(i) => + Some((Nil, Some(entity_ref_color))) + case _ => None + } case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) => val color = depth match { diff -r 4be23c432491 -r 9d2fae6b31cc src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Thu Apr 14 20:47:44 2016 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Thu Apr 14 22:55:53 2016 +0200 @@ -280,6 +280,13 @@ robust_rendering { rendering => val fm = text_area.getPainter.getFontMetrics + val focus = + JEdit_Lib.visible_range(text_area) match { + case Some(visible_range) if caret_enabled => + rendering.caret_focus(JEdit_Lib.caret_range(text_area), visible_range) + case _ => Set.empty[Long] + } + for (i <- 0 until physical_lines.length) { if (physical_lines(i) != -1) { val line_range = Text.Range(start(i), end(i) min buffer.getLength) @@ -294,7 +301,7 @@ // background color for { - Text.Info(range, color) <- rendering.background(line_range) + Text.Info(range, color) <- rendering.background(line_range, focus) r <- JEdit_Lib.gfx_range(text_area, range) } { gfx.setColor(color)