From 20b0bd0a2018295db19d3dabb5905841fd16a679 Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Mon, 22 Sep 2025 22:21:14 +1000 Subject: [PATCH] chore: upstream `rangeOfStx?` from Batteries (#10490) This PR upstreams a helper function that is used in ProofWidgets. --------- Co-authored-by: Marc Huisinga --- src/Lean/Data/Lsp/Utf16.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Lean/Data/Lsp/Utf16.lean b/src/Lean/Data/Lsp/Utf16.lean index 1cebe55027..f04079b54c 100644 --- a/src/Lean/Data/Lsp/Utf16.lean +++ b/src/Lean/Data/Lsp/Utf16.lean @@ -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 }