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

Gets the LSP range of syntax stx.

Equations

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

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

Return the beginning of the line contatining character pos.

Equations

• Lean.findLineStart s pos = match String.revFindAux s (fun (x : Char) => decide (x = '\n')) pos with | none => 0 | some n => { byteIdx := n.byteIdx + 1 }

def Lean.findIndentAndIsStart (s : String) (pos : String.Pos) : 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

• Lean.findIndentAndIsStart s pos = let start := Lean.findLineStart s pos; let body := String.findAux s (fun (x : Char) => decide (x ≠ ' ')) pos start; ((body - start).byteIdx, body == pos)