Skip to content

Commit 20b0bd0

Browse files
kim-emmhuisi
andauthored
chore: upstream rangeOfStx? from Batteries (#10490)
This PR upstreams a helper function that is used in ProofWidgets. --------- Co-authored-by: Marc Huisinga <[email protected]>
1 parent 979c2b4 commit 20b0bd0

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

src/Lean/Data/Lsp/Utf16.lean

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,10 @@ def utf8PosToLspPos (text : FileMap) (pos : String.Pos) : Lsp.Position :=
9494
def utf8RangeToLspRange (text : FileMap) (range : String.Range) : Lsp.Range :=
9595
{ start := text.utf8PosToLspPos range.start, «end» := text.utf8PosToLspPos range.stop }
9696

97+
/-- Gets the LSP range of syntax `stx`. -/
98+
def lspRangeOfStx? (text : FileMap) (stx : Syntax) (canonicalOnly := false) : Option Lsp.Range :=
99+
text.utf8RangeToLspRange <$> stx.getRange? canonicalOnly
100+
97101
def lspRangeToUtf8Range (text : FileMap) (range : Lsp.Range) : String.Range :=
98102
{ start := text.lspPosToUtf8Pos range.start, stop := text.lspPosToUtf8Pos range.end }
99103

0 commit comments

Comments
 (0)