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

Gets the LSP range from a String.Range.

Equations

• Lean.FileMap.utf8RangeToLspRange text range = { start := Lean.FileMap.utf8PosToLspPos text range.start, end := Lean.FileMap.utf8PosToLspPos text range.stop }

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.FileMap.ofPosition (text : Lean.FileMap) (pos : Lean.Position) : String.Pos

Convert a Lean.Position to a String.Pos.

Equations

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

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 = Char.ofNat 10)) 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

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

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

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

Equations

• Lean.Syntax.ofRange range canonical = Lean.Syntax.atom (Lean.SourceInfo.synthetic range.start range.stop canonical) ""

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

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

Equations

• Lean.FileMap.lineStart map line = if h : line - 1 < Array.size map.positions then Array.get map.positions { val := line - 1, isLt := h } else Option.getD (Array.back? map.positions) 0