# HG changeset patch # User wenzelm # Date 1483473766 -3600 # Node ID f5c4ffdb1124a03bc65dc78f1760592d320ec321 # Parent 6fd05caf55f0ede8f337389b2fc5e2476975b242 support VSCode DocumentHighlights; clarified modules; diff -r 6fd05caf55f0 -r f5c4ffdb1124 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Tue Jan 03 19:22:17 2017 +0100 +++ b/src/Pure/PIDE/rendering.scala Tue Jan 03 21:02:46 2017 +0100 @@ -58,6 +58,8 @@ private def pretty_typing(kind: String, body: XML.Body): XML.Tree = Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body) + + val caret_focus_elements = Markup.Elements(Markup.ENTITY) } abstract class Rendering( @@ -162,4 +164,53 @@ Some(Text.Info(r, all_tips)) } } + + + /* caret focus */ + + private def entity_focus(range: Text.Range, + check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] = + { + val results = + snapshot.cumulate[Set[Long]](range, Set.empty, Rendering.caret_focus_elements, _ => + { + case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) => + props match { + case Markup.Entity.Def(i) if check(true, i) => Some(serials + i) + case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i) + case _ => None + } + case _ => None + }) + (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 } + } + + def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] = + { + val focus_defs = entity_focus(caret_range) + if (focus_defs.nonEmpty) focus_defs + else { + val visible_defs = entity_focus(visible_range) + entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i)) + } + } + + def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] = + { + val focus = caret_focus(caret_range, visible_range) + if (focus.nonEmpty) { + val results = + 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 Markup.Entity.Ref(i) if focus(i) => Some(true) + case _ => None + } + }) + for (info <- results if info.info) yield info.range + } + else Nil + } } diff -r 6fd05caf55f0 -r f5c4ffdb1124 src/Tools/VSCode/src/protocol.scala --- a/src/Tools/VSCode/src/protocol.scala Tue Jan 03 19:22:17 2017 +0100 +++ b/src/Tools/VSCode/src/protocol.scala Tue Jan 03 21:02:46 2017 +0100 @@ -138,7 +138,8 @@ Map( "textDocumentSync" -> 1, "hoverProvider" -> true, - "definitionProvider" -> true) + "definitionProvider" -> true, + "documentHighlightProvider" -> true) } object Shutdown extends Request0("shutdown") @@ -315,6 +316,31 @@ } + /* document highlights request */ + + object DocumentHighlight + { + def text(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(1)) + def read(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(2)) + def write(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(3)) + } + + sealed case class DocumentHighlight(range: Line.Range, kind: Option[Int] = None) + { + def json: JSON.T = + kind match { + case None => Map("range" -> Range(range)) + case Some(k) => Map("range" -> Range(range), "kind" -> k) + } + } + + object DocumentHighlights extends RequestTextDocumentPosition("textDocument/documentHighlight") + { + def reply(id: Id, result: List[DocumentHighlight]): JSON.T = + ResponseMessage(id, Some(result.map(_.json))) + } + + /* diagnostics */ sealed case class Diagnostic(range: Line.Range, message: String, diff -r 6fd05caf55f0 -r f5c4ffdb1124 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Tue Jan 03 19:22:17 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Tue Jan 03 21:02:46 2017 +0100 @@ -303,6 +303,21 @@ } + /* document highlights */ + + def document_highlights(id: Protocol.Id, node_pos: Line.Node_Position) + { + val result = + (for ((rendering, offset) <- rendering_offset(node_pos)) + yield { + val doc = rendering.model.doc + rendering.caret_focus_ranges(Text.Range(offset, offset + 1), doc.full_range) + .map(r => Protocol.DocumentHighlight.text(doc.range(r))) + }) getOrElse Nil + channel.write(Protocol.DocumentHighlights.reply(id, result)) + } + + /* main loop */ def start() @@ -324,6 +339,7 @@ close_document(uri) case Protocol.Hover(id, node_pos) => hover(id, node_pos) case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos) + case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos) case _ => log("### IGNORED") } } diff -r 6fd05caf55f0 -r f5c4ffdb1124 src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Tue Jan 03 19:22:17 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Tue Jan 03 21:02:46 2017 +0100 @@ -127,8 +127,6 @@ 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, @@ -367,54 +365,8 @@ /* caret focus */ - def entity_focus(range: Text.Range, - check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] = - { - val results = - snapshot.cumulate[Set[Long]](range, Set.empty, JEdit_Rendering.caret_focus_elements, _ => - { - case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) => - props match { - case Markup.Entity.Def(i) if check(true, i) => Some(serials + i) - case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i) - case _ => None - } - case _ => None - }) - (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 } - } - - def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] = - { - val focus_defs = entity_focus(caret_range) - if (focus_defs.nonEmpty) focus_defs - else { - val visible_defs = entity_focus(visible_range) - entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i)) - } - } - - def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] = - { - val focus = caret_focus(caret_range, visible_range) - if (focus.nonEmpty) { - val results = - snapshot.cumulate[Boolean](visible_range, false, JEdit_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 Markup.Entity.Ref(i) if focus(i) => Some(true) - case _ => None - } - }) - for (info <- results if info.info) yield info.range - } - else Nil - } - def entity_ref(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] = - snapshot.select(range, JEdit_Rendering.caret_focus_elements, _ => + snapshot.select(range, Rendering.caret_focus_elements, _ => { case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _)) if focus(i) => Some(entity_ref_color)