--- 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
+ }
}
--- 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,
--- 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")
}
}
--- 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)