diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
index a7a8f0cb6c..bebfde1e36 100644
--- a/src/Lean/Server/FileWorker/RequestHandling.lean
+++ b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -116,7 +116,7 @@ def locationLinksOfInfo (kind : GoToKind) (ci : Elab.ContextInfo) (i : Elab.Info
     if let some modUri ← documentUriFromModule name then
       let range := { start := ⟨0, 0⟩, «end» := ⟨0, 0⟩ : Range }
       let ll : LocationLink := {
-        originSelectionRange? := (·.toLspRange text) <$> i.stx[2].getRange?
+        originSelectionRange? := (·.toLspRange text) <$> i.stx[2].getRange? (originalOnly := true)
         targetUri := modUri
         targetRange := range
         targetSelectionRange := range
diff --git a/src/Lean/Server/FileWorker/WidgetRequests.lean b/src/Lean/Server/FileWorker/WidgetRequests.lean
index 62531590c8..2db1768998 100644
--- a/src/Lean/Server/FileWorker/WidgetRequests.lean
+++ b/src/Lean/Server/FileWorker/WidgetRequests.lean
@@ -102,12 +102,17 @@ builtin_initialize
     (Array InteractiveDiagnostic)
     getInteractiveDiagnostics
 
+structure GetGoToLocationParams where
+  kind : FileWorker.GoToKind
+  info : WithRpcRef InfoWithCtx
+  deriving RpcEncoding
+
 builtin_initialize
   registerBuiltinRpcProcedure
     `Lean.Widget.getGoToLocation
-    (FileWorker.GoToKind × WithRpcRef InfoWithCtx)
+    GetGoToLocationParams
     (Array Lsp.LocationLink)
-    fun (kind, ⟨i⟩) => RequestM.asTask <|
+    fun ⟨kind, ⟨i⟩⟩ => RequestM.asTask <|
       FileWorker.locationLinksOfInfo kind i.ctx i.info
 
 end Lean.Widget
diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean
index 524293f3c7..99f94f9456 100644
--- a/src/Lean/Widget/InteractiveCode.lean
+++ b/src/Lean/Widget/InteractiveCode.lean
@@ -21,7 +21,8 @@ structure InfoWithCtx where
   info : Elab.Info
   deriving Inhabited, RpcEncoding with { withRef := true }
 
-structure CodeToken where
+/-- Information about a subexpression within delaborated code. -/
+structure SubexprInfo where
   /-- The `Elab.Info` node with the semantics of this part of the output. -/
   info : WithRpcRef InfoWithCtx
   /-- The position of this subexpression within the top-level expression.
@@ -32,7 +33,7 @@ structure CodeToken where
   deriving Inhabited, RpcEncoding
 
 /-- Pretty-printed syntax (usually but not necessarily an `Expr`) with embedded `Info`s. -/
-abbrev CodeWithInfos := TaggedText CodeToken
+abbrev CodeWithInfos := TaggedText SubexprInfo
 
 def CodeWithInfos.pretty (tt : CodeWithInfos) :=
   tt.stripTags