basic support for hyperlinks / Goto Definition Request;

--- a/src/Pure/PIDE/rendering.scala	Wed Dec 21 21:17:44 2016 +0100
+++ b/src/Pure/PIDE/rendering.scala	Wed Dec 21 21:18:37 2016 +0100
@@ -46,6 +46,11 @@
       resources.append(snapshot.node_name.master_dir, Path.explode(name))
     else name
 
+  def resolve_file_url(name: String): String =
+    if (Path.is_valid(name))
+      "file://" + resources.append(snapshot.node_name.master_dir, Path.explode(name))
+    else name
+
 
   /* tooltips */
 

--- a/src/Tools/VSCode/src/protocol.scala	Wed Dec 21 21:17:44 2016 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Wed Dec 21 21:18:37 2016 +0100
@@ -80,6 +80,16 @@
       }
   }
 
+  class RequestTextDocumentPosition(name: String)
+  {
+    def unapply(json: JSON.T): Option[(Id, String, Line.Position)] =
+      json match {
+        case RequestMessage(id, method, Some(TextDocumentPosition(uri, pos))) if method == name =>
+          Some((id, uri, pos))
+        case _ => None
+      }
+  }
+
 
   /* response message */
 
@@ -125,7 +135,10 @@
   object ServerCapabilities
   {
     val json: JSON.T =
-      Map("textDocumentSync" -> 1, "hoverProvider" -> true)
+      Map(
+        "textDocumentSync" -> 1,
+        "hoverProvider" -> true,
+        "definitionProvider" -> true)
   }
 
   object Shutdown extends Request0("shutdown")
@@ -277,15 +290,8 @@
 
   /* hover request */
 
-  object Hover
+  object Hover extends RequestTextDocumentPosition("textDocument/hover")
   {
-    def unapply(json: JSON.T): Option[(Id, String, Line.Position)] =
-      json match {
-        case RequestMessage(id, "textDocument/hover", Some(TextDocumentPosition(uri, pos))) =>
-          Some((id, uri, pos))
-        case _ => None
-      }
-
     def reply(id: Id, result: Option[(Line.Range, List[String])]): JSON.T =
     {
       val res =
@@ -296,4 +302,13 @@
       ResponseMessage(id, Some(res))
     }
   }
+
+
+  /* goto definition request */
+
+  object GotoDefinition extends RequestTextDocumentPosition("textDocument/definition")
+  {
+    def reply(id: Id, result: List[(String, Line.Range)]): JSON.T =
+      ResponseMessage(id, Some(result.map({ case (uri, range) => Location.apply(uri, range) })))
+  }
 }

--- a/src/Tools/VSCode/src/server.scala	Wed Dec 21 21:17:44 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Wed Dec 21 21:18:37 2016 +0100
@@ -234,6 +234,21 @@
   }
 
 
+  /* goto definition */
+
+  def goto_definition(id: Protocol.Id, uri: String, pos: Line.Position)
+  {
+    val result =
+      (for {
+        model <- state.value.models.get(uri)
+        rendering = model.rendering(options)
+        offset <- model.doc.offset(pos, text_length)
+      } yield rendering.hyperlinks(Text.Range(offset, offset + 1))) getOrElse Nil
+    channel.log("hyperlinks = " + result)
+    channel.write(Protocol.GotoDefinition.reply(id, result))
+  }
+
+
   /* main loop */
 
   def start()
@@ -254,6 +269,7 @@
           case Protocol.DidCloseTextDocument(uri) => channel.log("CLOSE " + uri)
           case Protocol.DidSaveTextDocument(uri) => channel.log("SAVE " + uri)
           case Protocol.Hover(id, uri, pos) => hover(id, uri, pos)
+          case Protocol.GotoDefinition(id, uri, pos) => goto_definition(id, uri, pos)
           case _ => channel.log("### IGNORED")
         }
       }

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 21 21:17:44 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Dec 21 21:18:37 2016 +0100
@@ -10,6 +10,11 @@
 
 import isabelle._
 
+object VSCode_Rendering
+{
+  private val hyperlink_elements =
+    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
+}
 
 class VSCode_Rendering(snapshot: Document.Snapshot, options: Options, resources: Resources)
   extends Rendering(snapshot, options, resources)
@@ -18,4 +23,36 @@
 
   def tooltip_margin: Int = options.int("vscode_tooltip_margin")
   def timing_threshold: Double = options.real("vscode_timing_threshold")
+
+
+  /* hyperlinks */
+
+  def hyperlinks(range: Text.Range): List[(String, Line.Range)] =
+  {
+    snapshot.cumulate[List[(String, Line.Range)]](
+      range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
+        {
+          case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
+            Some((resolve_file_url(name), Line.Range.zero) :: links)
+
+/* FIXME
+          case (links, Text.Info(_, XML.Elem(Markup.Url(name), _))) =>
+            Some(PIDE.editor.hyperlink_url(name) :: links)
+
+          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
+          if !props.exists(
+            { case (Markup.KIND, Markup.ML_OPEN) => true
+              case (Markup.KIND, Markup.ML_STRUCTURE) => true
+              case _ => false }) =>
+            val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
+            opt_link.map(_ :: links)
+
+          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
+            val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props)
+            opt_link.map(_ :: links)
+*/
+
+          case _ => None
+        }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
+  }
 }