def Lean.FileMap.utf8RangeToLspRange (text : Lean.FileMap) (range : String.Range) : Lean.Lsp.Range

Gets the LSP range from a String.Range.

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

Gets the LSP range of syntax stx.

def Lean.FileMap.ofPosition (text : Lean.FileMap) (pos : Lean.Position) : String.Pos

Convert a Lean.Position to a String.Pos.

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

Return the beginning of the line contatining character pos.

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.

def Lean.Syntax.ofRange (range : String.Range) (canonical : optParam Bool true) : Lean.Syntax

Returns a synthetic Syntax which has the specified String.Range.

def Lean.FileMap.lineStart (map : Lean.FileMap) (line : Nat) : String.Pos

Returns the position of the start of (1-based) line line.