diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index 48d34de66c..a7a8f0cb6c 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -59,15 +59,14 @@ def handleHover (p : HoverParams)
 
 inductive GoToKind
   | declaration | definition | type
-  deriving BEq
+  deriving BEq, ToJson, FromJson
 
 open Elab GoToKind in
-partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
-    : RequestM (RequestTask (Array LocationLink)) := do
+def locationLinksOfInfo (kind : GoToKind) (ci : Elab.ContextInfo) (i : Elab.Info)
+    (infoTree? : Option InfoTree := none) : RequestM (Array LocationLink) := do
   let rc ← read
   let doc ← readDoc
   let text := doc.meta.text
-  let hoverPos := text.lspPosToUtf8Pos p.position
 
   let documentUriFromModule (modName : Name) : MetaM (Option DocumentUri) := do
     let some modFname ← rc.srcSearchPath.findModuleWithExt "lean" modName
@@ -97,15 +96,15 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
       return #[ll]
     return #[]
 
-  let locationLinksFromBinder (t : InfoTree) (i : Elab.Info) (id : FVarId) := do
-    if let some i' := t.findInfo? fun
+  let locationLinksFromBinder (i : Elab.Info) (id : FVarId) := do
+    if let some i' := infoTree? >>= InfoTree.findInfo? fun
         | Info.ofTermInfo { isBinder := true, expr := Expr.fvar id' .., .. } => id' == id
         | _ => false then
       if let some r := i'.range? then
         let r := r.toLspRange text
         let ll : LocationLink := {
           originSelectionRange? := (·.toLspRange text) <$> i.range?
-          targetUri := p.textDocument.uri
+          targetUri := doc.meta.uri
           targetRange := r
           targetSelectionRange := r
         }
@@ -117,7 +116,7 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
     if let some modUri ← documentUriFromModule name then
       let range := { start := ⟨0, 0⟩, «end» := ⟨0, 0⟩ : Range }
       let ll : LocationLink := {
-        originSelectionRange? := none
+        originSelectionRange? := (·.toLspRange text) <$> i.stx[2].getRange?
         targetUri := modUri
         targetRange := range
         targetSelectionRange := range
@@ -125,36 +124,47 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
       return #[ll]
     return #[]
 
+  if let Info.ofTermInfo ti := i then
+    let mut expr := ti.expr
+    if kind == type then
+      expr ← ci.runMetaM i.lctx do
+        return Expr.getAppFn (← Meta.instantiateMVars (← Meta.inferType expr))
+    match expr with
+    | Expr.const n .. => return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
+    | Expr.fvar id .. => return ← ci.runMetaM i.lctx <| locationLinksFromBinder i id
+    | _ => pure ()
+  if let Info.ofFieldInfo fi := i then
+    if kind == type then
+      let expr ← ci.runMetaM i.lctx do
+        Meta.instantiateMVars (← Meta.inferType fi.val)
+      if let some n := expr.getAppFn.constName? then
+        return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
+    else
+      return ← ci.runMetaM i.lctx <| locationLinksFromDecl i fi.projName
+  if let Info.ofCommandInfo ⟨`import, _⟩ := i then
+    if kind == definition || kind == declaration then
+      return ← ci.runMetaM i.lctx <| locationLinksFromImport i
+  -- If other go-tos fail, we try to show the elaborator or parser
+  if let some ei := i.toElabInfo? then
+    if kind == declaration && ci.env.contains ei.stx.getKind then
+      return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.stx.getKind
+    if kind == definition && ci.env.contains ei.elaborator then
+      return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator
+  return #[]
+
+open Elab GoToKind in
+def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
+    : RequestM (RequestTask (Array LocationLink)) := do
+  let rc ← read
+  let doc ← readDoc
+  let text := doc.meta.text
+  let hoverPos := text.lspPosToUtf8Pos p.position
+
   withWaitFindSnap doc (fun s => s.endPos > hoverPos)
     (notFoundX := pure #[]) fun snap => do
       if let some (ci, i) := snap.infoTree.hoverableInfoAt? (includeStop := true /- #767 -/) hoverPos then
-        if let Info.ofTermInfo ti := i then
-          let mut expr := ti.expr
-          if kind == type then
-            expr ← ci.runMetaM i.lctx do
-              return Expr.getAppFn (← Meta.instantiateMVars (← Meta.inferType expr))
-          match expr with
-          | Expr.const n .. => return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
-          | Expr.fvar id .. => return ← ci.runMetaM i.lctx <| locationLinksFromBinder snap.infoTree i id
-          | _ => pure ()
-        if let Info.ofFieldInfo fi := i then
-          if kind == type then
-            let expr ← ci.runMetaM i.lctx do
-              Meta.instantiateMVars (← Meta.inferType fi.val)
-            if let some n := expr.getAppFn.constName? then
-              return ← ci.runMetaM i.lctx <| locationLinksFromDecl i n
-          else
-            return ← ci.runMetaM i.lctx <| locationLinksFromDecl i fi.projName
-        if let Info.ofCommandInfo ⟨`import, _⟩ := i then
-          if kind == definition || kind == declaration then
-            return ← ci.runMetaM i.lctx <| locationLinksFromImport i
-        -- If other go-tos fail, we try to show the elaborator or parser
-        if let some ei := i.toElabInfo? then
-          if kind == declaration && ci.env.contains ei.stx.getKind then
-            return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.stx.getKind
-          if kind == definition && ci.env.contains ei.elaborator then
-            return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator
-      return #[]
+        locationLinksOfInfo kind ci i snap.infoTree
+      else return #[]
 
 open RequestM in
 def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option Widget.InteractiveGoals)) := do
diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean
index 478f14bc6f..0024ad1f8e 100644
--- a/src/Lean/Server/FileWorker/WidgetRequests.lean
+++ b/src/Lean/Server/FileWorker/WidgetRequests.lean
@@ -102,4 +102,16 @@ builtin_initialize
     (Array InteractiveDiagnostic)
     getInteractiveDiagnostics
 
+builtin_initialize
+  registerBuiltinRpcProcedure
+    `Lean.Widget.getGoToLocation
+    (WithRpcRef InfoWithCtx × FileWorker.GoToKind)
+    (Option Lsp.Location)
+    fun (⟨i⟩, kind) => RequestM.asTask do
+      let ls ← FileWorker.locationLinksOfInfo kind i.ctx i.info
+      return ls.back?.map fun lnk => {
+        uri := lnk.targetUri
+        range := lnk.targetSelectionRange
+      }
+
 end Lean.Widget