src/Tools/VSCode/src/protocol.scala

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