@[deprecated Lean.FileMap.lspRangeOfStx? (since := "2025-09-23")]

def Lean.FileMap.rangeOfStx? (text : FileMap) (stx : Syntax) : Option Lsp.Range

Gets the LSP range of syntax stx.

Equations

• text.rangeOfStx? stx = text.utf8RangeToLspRange <$> stx.getRange?

def Lean.findLineStart (s : String) (pos : String.Pos.Raw) : String.Pos.Raw

Return the beginning of the line contatining character pos.

Equations

• Lean.findLineStart s pos = ((Option.map (fun (x : s.Pos) => x.next!) ((s.pos! pos).revFind? '\n')).getD s.startPos).offset

def Lean.findIndentAndIsStart (s : String) (pos : String.Pos.Raw) : Nat × Bool

Return the indentation (number of leading spaces) of the line containing pos, and whether pos is the first non-whitespace character in the line.

Equations

• One or more equations did not get rendered due to their size.