src/Tools/VSCode/src/protocol.scala

   class Request0(name: String)
   {
     def unapply(json: JSON.T): Option[Id] =
       json match {
         case RequestMessage(id, method, _) if method == name => Some(id)
+        case _ => None
+      }
+  }
+
+  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
       }
   }
 
 

   }
 
   object ServerCapabilities
   {
     val json: JSON.T =
-      Map("textDocumentSync" -> 1, "hoverProvider" -> true)
+      Map(
+        "textDocumentSync" -> 1,
+        "hoverProvider" -> true,
+        "definitionProvider" -> true)
   }
 
   object Shutdown extends Request0("shutdown")
   {
     def reply(id: Id, error: String): JSON.T =

   object DidSaveTextDocument extends TextDocumentNotification("textDocument/didSave")
 
 
   /* hover request */
 
-  object 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
-      }
-
+  object Hover extends RequestTextDocumentPosition("textDocument/hover")
+  {
     def reply(id: Id, result: Option[(Line.Range, List[String])]): JSON.T =
     {
       val res =
         result match {
           case Some((range, contents)) => Map("contents" -> contents, "range" -> Range(range))
           case None => Map("contents" -> Nil)
         }
       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) })))
+  }
 }