basic support for hyperlinks / Goto Definition Request;
authorwenzelm
Wed Dec 21 21:18:37 2016 +0100 (2016-12-21)
changeset 646485d7f741aaccb
parent 64647 bbfcef118acb
child 64649 d67c3094a0c2
basic support for hyperlinks / Goto Definition Request;
src/Pure/PIDE/rendering.scala
src/Tools/VSCode/src/protocol.scala
src/Tools/VSCode/src/server.scala
src/Tools/VSCode/src/vscode_rendering.scala
     1.1 --- a/src/Pure/PIDE/rendering.scala	Wed Dec 21 21:17:44 2016 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Wed Dec 21 21:18:37 2016 +0100
     1.3 @@ -46,6 +46,11 @@
     1.4        resources.append(snapshot.node_name.master_dir, Path.explode(name))
     1.5      else name
     1.6  
     1.7 +  def resolve_file_url(name: String): String =
     1.8 +    if (Path.is_valid(name))
     1.9 +      "file://" + resources.append(snapshot.node_name.master_dir, Path.explode(name))
    1.10 +    else name
    1.11 +
    1.12  
    1.13    /* tooltips */
    1.14  
     2.1 --- a/src/Tools/VSCode/src/protocol.scala	Wed Dec 21 21:17:44 2016 +0100
     2.2 +++ b/src/Tools/VSCode/src/protocol.scala	Wed Dec 21 21:18:37 2016 +0100
     2.3 @@ -80,6 +80,16 @@
     2.4        }
     2.5    }
     2.6  
     2.7 +  class RequestTextDocumentPosition(name: String)
     2.8 +  {
     2.9 +    def unapply(json: JSON.T): Option[(Id, String, Line.Position)] =
    2.10 +      json match {
    2.11 +        case RequestMessage(id, method, Some(TextDocumentPosition(uri, pos))) if method == name =>
    2.12 +          Some((id, uri, pos))
    2.13 +        case _ => None
    2.14 +      }
    2.15 +  }
    2.16 +
    2.17  
    2.18    /* response message */
    2.19  
    2.20 @@ -125,7 +135,10 @@
    2.21    object ServerCapabilities
    2.22    {
    2.23      val json: JSON.T =
    2.24 -      Map("textDocumentSync" -> 1, "hoverProvider" -> true)
    2.25 +      Map(
    2.26 +        "textDocumentSync" -> 1,
    2.27 +        "hoverProvider" -> true,
    2.28 +        "definitionProvider" -> true)
    2.29    }
    2.30  
    2.31    object Shutdown extends Request0("shutdown")
    2.32 @@ -277,15 +290,8 @@
    2.33  
    2.34    /* hover request */
    2.35  
    2.36 -  object Hover
    2.37 +  object Hover extends RequestTextDocumentPosition("textDocument/hover")
    2.38    {
    2.39 -    def unapply(json: JSON.T): Option[(Id, String, Line.Position)] =
    2.40 -      json match {
    2.41 -        case RequestMessage(id, "textDocument/hover", Some(TextDocumentPosition(uri, pos))) =>
    2.42 -          Some((id, uri, pos))
    2.43 -        case _ => None
    2.44 -      }
    2.45 -
    2.46      def reply(id: Id, result: Option[(Line.Range, List[String])]): JSON.T =
    2.47      {
    2.48        val res =
    2.49 @@ -296,4 +302,13 @@
    2.50        ResponseMessage(id, Some(res))
    2.51      }
    2.52    }
    2.53 +
    2.54 +
    2.55 +  /* goto definition request */
    2.56 +
    2.57 +  object GotoDefinition extends RequestTextDocumentPosition("textDocument/definition")
    2.58 +  {
    2.59 +    def reply(id: Id, result: List[(String, Line.Range)]): JSON.T =
    2.60 +      ResponseMessage(id, Some(result.map({ case (uri, range) => Location.apply(uri, range) })))
    2.61 +  }
    2.62  }
     3.1 --- a/src/Tools/VSCode/src/server.scala	Wed Dec 21 21:17:44 2016 +0100
     3.2 +++ b/src/Tools/VSCode/src/server.scala	Wed Dec 21 21:18:37 2016 +0100
     3.3 @@ -234,6 +234,21 @@
     3.4    }
     3.5  
     3.6  
     3.7 +  /* goto definition */
     3.8 +
     3.9 +  def goto_definition(id: Protocol.Id, uri: String, pos: Line.Position)
    3.10 +  {
    3.11 +    val result =
    3.12 +      (for {
    3.13 +        model <- state.value.models.get(uri)
    3.14 +        rendering = model.rendering(options)
    3.15 +        offset <- model.doc.offset(pos, text_length)
    3.16 +      } yield rendering.hyperlinks(Text.Range(offset, offset + 1))) getOrElse Nil
    3.17 +    channel.log("hyperlinks = " + result)
    3.18 +    channel.write(Protocol.GotoDefinition.reply(id, result))
    3.19 +  }
    3.20 +
    3.21 +
    3.22    /* main loop */
    3.23  
    3.24    def start()
    3.25 @@ -254,6 +269,7 @@
    3.26            case Protocol.DidCloseTextDocument(uri) => channel.log("CLOSE " + uri)
    3.27            case Protocol.DidSaveTextDocument(uri) => channel.log("SAVE " + uri)
    3.28            case Protocol.Hover(id, uri, pos) => hover(id, uri, pos)
    3.29 +          case Protocol.GotoDefinition(id, uri, pos) => goto_definition(id, uri, pos)
    3.30            case _ => channel.log("### IGNORED")
    3.31          }
    3.32        }
     4.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 21 21:17:44 2016 +0100
     4.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 21 21:18:37 2016 +0100
     4.3 @@ -10,6 +10,11 @@
     4.4  
     4.5  import isabelle._
     4.6  
     4.7 +object VSCode_Rendering
     4.8 +{
     4.9 +  private val hyperlink_elements =
    4.10 +    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
    4.11 +}
    4.12  
    4.13  class VSCode_Rendering(snapshot: Document.Snapshot, options: Options, resources: Resources)
    4.14    extends Rendering(snapshot, options, resources)
    4.15 @@ -18,4 +23,36 @@
    4.16  
    4.17    def tooltip_margin: Int = options.int("vscode_tooltip_margin")
    4.18    def timing_threshold: Double = options.real("vscode_timing_threshold")
    4.19 +
    4.20 +
    4.21 +  /* hyperlinks */
    4.22 +
    4.23 +  def hyperlinks(range: Text.Range): List[(String, Line.Range)] =
    4.24 +  {
    4.25 +    snapshot.cumulate[List[(String, Line.Range)]](
    4.26 +      range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
    4.27 +        {
    4.28 +          case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
    4.29 +            Some((resolve_file_url(name), Line.Range.zero) :: links)
    4.30 +
    4.31 +/* FIXME
    4.32 +          case (links, Text.Info(_, XML.Elem(Markup.Url(name), _))) =>
    4.33 +            Some(PIDE.editor.hyperlink_url(name) :: links)
    4.34 +
    4.35 +          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
    4.36 +          if !props.exists(
    4.37 +            { case (Markup.KIND, Markup.ML_OPEN) => true
    4.38 +              case (Markup.KIND, Markup.ML_STRUCTURE) => true
    4.39 +              case _ => false }) =>
    4.40 +            val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
    4.41 +            opt_link.map(_ :: links)
    4.42 +
    4.43 +          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
    4.44 +            val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props)
    4.45 +            opt_link.map(_ :: links)
    4.46 +*/
    4.47 +
    4.48 +          case _ => None
    4.49 +        }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
    4.50 +  }
    4.51  }