# 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)