diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index 76f3ea7ab0..27bf2ed6c6 100644 --- a/src/Lean/Server/Requests.lean +++ b/src/Lean/Server/Requests.lean @@ -124,10 +124,10 @@ def bindWaitFindSnap (doc : EditableDocument) (p : Snapshot → Bool) /-- Helper for running an Rpc request at a particular snapshot. -/ def withWaitFindSnapAtPos - (lspPos : Lean.Lsp.TextDocumentPositionParams) + (lspPos : Lean.Lsp.Position) (f : Snapshots.Snapshot → RequestM α): RequestM (RequestTask α) := do let doc ← readDoc - let pos := doc.meta.text.lspPosToUtf8Pos lspPos.position + let pos := doc.meta.text.lspPosToUtf8Pos lspPos withWaitFindSnap doc (fun s => s.endPos >= pos) diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean index 882869b55a..b99b903719 100644 --- a/src/Lean/Widget/UserWidget.lean +++ b/src/Lean/Widget/UserWidget.lean @@ -92,7 +92,7 @@ builtin_initialize registerBuiltinAttribute attributeImpl structure GetWidgetSourceParams where /-- The hash of the sourcetext to retrieve. -/ hash: UInt64 - pos : Lean.Lsp.TextDocumentPositionParams + pos : Lean.Lsp.Position deriving ToJson, FromJson open Lean.Server Lean RequestM in @@ -140,10 +140,10 @@ structure GetWidgetsResponse where open Lean Server RequestM in /-- Get the `UserWidget`s present at a particular position. -/ @[serverRpcMethod] -def getWidgets (args : Lean.Lsp.TextDocumentPositionParams) : RequestM (RequestTask (GetWidgetsResponse)) := do +def getWidgets (args : Lean.Lsp.Position) : RequestM (RequestTask (GetWidgetsResponse)) := do let doc ← readDoc let filemap := doc.meta.text - let pos := filemap.lspPosToUtf8Pos args.position + let pos := filemap.lspPosToUtf8Pos args withWaitFindSnapAtPos args fun snap => do let env := snap.env let ws := widgetInfosAt? filemap snap.infoTree pos