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

chore: upstream rangeOfStx? from Batteries (#10490)

Browse source 
This PR upstreams a helper function that is used in ProofWidgets.

---------

Co-authored-by: Marc Huisinga <mhuisi@protonmail.com>
This commit is contained in:
Kim Morrison 2025-09-22 22:21:14 +10:00 • committed by GitHub
parent 979c2b4af0
commit 20b0bd0a20
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Data/Lsp/Utf16.lean
View file

@ -94,6 +94,10 @@ def utf8PosToLspPos (text : FileMap) (pos : String.Pos) : Lsp.Position :=
def utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
{ start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
/-- Gets the LSP range of syntax `stx`. -/
def lspRangeOfStx? (text : FileMap) (stx : Syntax) (canonicalOnly := false) : Option Lsp.Range :=
text.utf8RangeToLspRange <$> stx.getRange? canonicalOnly
def lspRangeToUtf8Range (text : FileMap) (range : Lsp.Range) : String.Range :=
{ start := text.lspPosToUtf8Pos range.start, stop := text.lspPosToUtf8Pos range.end }