support VSCode DocumentHighlights;
authorwenzelm
Tue Jan 03 21:02:46 2017 +0100 (2017-01-03)
changeset 64767f5c4ffdb1124
parent 64766 6fd05caf55f0
child 64768 34ef44748370
support VSCode DocumentHighlights;
clarified modules;
src/Pure/PIDE/rendering.scala
src/Tools/VSCode/src/protocol.scala
src/Tools/VSCode/src/server.scala
src/Tools/jEdit/src/jedit_rendering.scala
     1.1 --- a/src/Pure/PIDE/rendering.scala	Tue Jan 03 19:22:17 2017 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Tue Jan 03 21:02:46 2017 +0100
     1.3 @@ -58,6 +58,8 @@
     1.4  
     1.5    private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
     1.6      Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
     1.7 +
     1.8 +  val caret_focus_elements = Markup.Elements(Markup.ENTITY)
     1.9  }
    1.10  
    1.11  abstract class Rendering(
    1.12 @@ -162,4 +164,53 @@
    1.13          Some(Text.Info(r, all_tips))
    1.14      }
    1.15    }
    1.16 +
    1.17 +
    1.18 +  /* caret focus */
    1.19 +
    1.20 +  private def entity_focus(range: Text.Range,
    1.21 +    check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] =
    1.22 +  {
    1.23 +    val results =
    1.24 +      snapshot.cumulate[Set[Long]](range, Set.empty, Rendering.caret_focus_elements, _ =>
    1.25 +          {
    1.26 +            case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
    1.27 +              props match {
    1.28 +                case Markup.Entity.Def(i) if check(true, i) => Some(serials + i)
    1.29 +                case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
    1.30 +                case _ => None
    1.31 +              }
    1.32 +            case _ => None
    1.33 +          })
    1.34 +    (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
    1.35 +  }
    1.36 +
    1.37 +  def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
    1.38 +  {
    1.39 +    val focus_defs = entity_focus(caret_range)
    1.40 +    if (focus_defs.nonEmpty) focus_defs
    1.41 +    else {
    1.42 +      val visible_defs = entity_focus(visible_range)
    1.43 +      entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i))
    1.44 +    }
    1.45 +  }
    1.46 +
    1.47 +  def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
    1.48 +  {
    1.49 +    val focus = caret_focus(caret_range, visible_range)
    1.50 +    if (focus.nonEmpty) {
    1.51 +      val results =
    1.52 +        snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ =>
    1.53 +          {
    1.54 +            case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
    1.55 +              props match {
    1.56 +                case Markup.Entity.Def(i) if focus(i) => Some(true)
    1.57 +                case Markup.Entity.Ref(i) if focus(i) => Some(true)
    1.58 +                case _ => None
    1.59 +              }
    1.60 +          })
    1.61 +      for (info <- results if info.info) yield info.range
    1.62 +    }
    1.63 +    else Nil
    1.64 +  }
    1.65  }
     2.1 --- a/src/Tools/VSCode/src/protocol.scala	Tue Jan 03 19:22:17 2017 +0100
     2.2 +++ b/src/Tools/VSCode/src/protocol.scala	Tue Jan 03 21:02:46 2017 +0100
     2.3 @@ -138,7 +138,8 @@
     2.4        Map(
     2.5          "textDocumentSync" -> 1,
     2.6          "hoverProvider" -> true,
     2.7 -        "definitionProvider" -> true)
     2.8 +        "definitionProvider" -> true,
     2.9 +        "documentHighlightProvider" -> true)
    2.10    }
    2.11  
    2.12    object Shutdown extends Request0("shutdown")
    2.13 @@ -315,6 +316,31 @@
    2.14    }
    2.15  
    2.16  
    2.17 +  /* document highlights request */
    2.18 +
    2.19 +  object DocumentHighlight
    2.20 +  {
    2.21 +    def text(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(1))
    2.22 +    def read(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(2))
    2.23 +    def write(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(3))
    2.24 +  }
    2.25 +
    2.26 +  sealed case class DocumentHighlight(range: Line.Range, kind: Option[Int] = None)
    2.27 +  {
    2.28 +    def json: JSON.T =
    2.29 +      kind match {
    2.30 +        case None => Map("range" -> Range(range))
    2.31 +        case Some(k) => Map("range" -> Range(range), "kind" -> k)
    2.32 +      }
    2.33 +  }
    2.34 +
    2.35 +  object DocumentHighlights extends RequestTextDocumentPosition("textDocument/documentHighlight")
    2.36 +  {
    2.37 +    def reply(id: Id, result: List[DocumentHighlight]): JSON.T =
    2.38 +      ResponseMessage(id, Some(result.map(_.json)))
    2.39 +  }
    2.40 +
    2.41 +
    2.42    /* diagnostics */
    2.43  
    2.44    sealed case class Diagnostic(range: Line.Range, message: String,
     3.1 --- a/src/Tools/VSCode/src/server.scala	Tue Jan 03 19:22:17 2017 +0100
     3.2 +++ b/src/Tools/VSCode/src/server.scala	Tue Jan 03 21:02:46 2017 +0100
     3.3 @@ -303,6 +303,21 @@
     3.4    }
     3.5  
     3.6  
     3.7 +  /* document highlights */
     3.8 +
     3.9 +  def document_highlights(id: Protocol.Id, node_pos: Line.Node_Position)
    3.10 +  {
    3.11 +    val result =
    3.12 +      (for ((rendering, offset) <- rendering_offset(node_pos))
    3.13 +        yield {
    3.14 +          val doc = rendering.model.doc
    3.15 +          rendering.caret_focus_ranges(Text.Range(offset, offset + 1), doc.full_range)
    3.16 +            .map(r => Protocol.DocumentHighlight.text(doc.range(r)))
    3.17 +        }) getOrElse Nil
    3.18 +    channel.write(Protocol.DocumentHighlights.reply(id, result))
    3.19 +  }
    3.20 +
    3.21 +
    3.22    /* main loop */
    3.23  
    3.24    def start()
    3.25 @@ -324,6 +339,7 @@
    3.26              close_document(uri)
    3.27            case Protocol.Hover(id, node_pos) => hover(id, node_pos)
    3.28            case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
    3.29 +          case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
    3.30            case _ => log("### IGNORED")
    3.31          }
    3.32        }
     4.1 --- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue Jan 03 19:22:17 2017 +0100
     4.2 +++ b/src/Tools/jEdit/src/jedit_rendering.scala	Tue Jan 03 21:02:46 2017 +0100
     4.3 @@ -127,8 +127,6 @@
     4.4  
     4.5    private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT)
     4.6  
     4.7 -  private val caret_focus_elements = Markup.Elements(Markup.ENTITY)
     4.8 -
     4.9    private val highlight_elements =
    4.10      Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
    4.11        Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL, Markup.SORTING,
    4.12 @@ -367,54 +365,8 @@
    4.13  
    4.14    /* caret focus */
    4.15  
    4.16 -  def entity_focus(range: Text.Range,
    4.17 -    check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] =
    4.18 -  {
    4.19 -    val results =
    4.20 -      snapshot.cumulate[Set[Long]](range, Set.empty, JEdit_Rendering.caret_focus_elements, _ =>
    4.21 -          {
    4.22 -            case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
    4.23 -              props match {
    4.24 -                case Markup.Entity.Def(i) if check(true, i) => Some(serials + i)
    4.25 -                case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
    4.26 -                case _ => None
    4.27 -              }
    4.28 -            case _ => None
    4.29 -          })
    4.30 -    (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
    4.31 -  }
    4.32 -
    4.33 -  def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
    4.34 -  {
    4.35 -    val focus_defs = entity_focus(caret_range)
    4.36 -    if (focus_defs.nonEmpty) focus_defs
    4.37 -    else {
    4.38 -      val visible_defs = entity_focus(visible_range)
    4.39 -      entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i))
    4.40 -    }
    4.41 -  }
    4.42 -
    4.43 -  def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
    4.44 -  {
    4.45 -    val focus = caret_focus(caret_range, visible_range)
    4.46 -    if (focus.nonEmpty) {
    4.47 -      val results =
    4.48 -        snapshot.cumulate[Boolean](visible_range, false, JEdit_Rendering.caret_focus_elements, _ =>
    4.49 -          {
    4.50 -            case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
    4.51 -              props match {
    4.52 -                case Markup.Entity.Def(i) if focus(i) => Some(true)
    4.53 -                case Markup.Entity.Ref(i) if focus(i) => Some(true)
    4.54 -                case _ => None
    4.55 -              }
    4.56 -          })
    4.57 -      for (info <- results if info.info) yield info.range
    4.58 -    }
    4.59 -    else Nil
    4.60 -  }
    4.61 -
    4.62    def entity_ref(range: Text.Range, focus: Set[Long]): List[Text.Info[Color]] =
    4.63 -    snapshot.select(range, JEdit_Rendering.caret_focus_elements, _ =>
    4.64 +    snapshot.select(range, Rendering.caret_focus_elements, _ =>
    4.65        {
    4.66          case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Entity.Ref(i)), _)) if focus(i) =>
    4.67            Some(entity_ref_color)