max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: simplify position type

Browse source
This commit is contained in:
Wojciech Nawrocki 2022-07-23 18:08:25 -04:00 • committed by Leonardo de Moura
parent b714e087d6
commit e30ae62dff
2 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Server/Requests.lean
View file

@ -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)

6
src/Lean/Widget/UserWidget.lean
View file

@ -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