src/Tools/VSCode/src/server.scala

       }
     channel.write(Protocol.Hover.reply(id, result))
   }
 
 
+  /* 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()
   {
     channel.log("Server started " + Date.now())

           case Protocol.DidChangeTextDocument(uri, version, List(Protocol.TextDocumentContent(text))) =>
             update_document(uri, text)
           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")
         }
       }
       catch { case exn: Throwable => channel.log("*** ERROR: " + Exn.message(exn)) }
     }