def Lean.FileMap.rangeContainsHoverPos (text : FileMap) (r : Syntax.Range) (hoverPos : String.Pos.Raw) (includeStop : Bool := false) : Bool

Checks whether r contains hoverPos, taking into account EOF according to text.

Equations

• text.rangeContainsHoverPos r hoverPos includeStop = r.contains hoverPos (includeStop || r.stop == text.source.rawEndPos)

def Lean.FileMap.rangeOverlapsRequestedRange (text : FileMap) (documentRange requestedRange : Syntax.Range) (includeDocumentRangeStop includeRequestedRangeStop : Bool := false) : Bool

Equations

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

def Lean.FileMap.rangeIncludesRequestedRange (text : FileMap) (documentRange requestedRange : Syntax.Range) (includeDocumentRangeStop includeRequestedRangeStop : Bool := false) : Bool

Equations

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

inductive Lean.Language.SnapshotTree.foldSnaps.Control : Type

• done : Control
• proceed (foldChildren : Bool) : Control

def Lean.Language.SnapshotTree.foldSnaps {α : Type u_1} (tree : SnapshotTree) (init : α) (f : SnapshotTask SnapshotTree → α → Task (α × foldSnaps.Control)) : Task α

Equations

• tree.foldSnaps init f = Task.map (fun (x : α × Bool) => x.fst) (Lean.Language.SnapshotTree.foldSnaps.traverseTree✝ f init tree) Task.Priority.default true

def Lean.Language.SnapshotTree.findInfoTreeAtPos (text : FileMap) (tree : SnapshotTree) (hoverPos : String.Pos.Raw) (includeStop : Bool) : Task (Option Elab.InfoTree)

Finds the first (in pre-order) snapshot task in tree that contains hoverPos (including whitespace) and which contains an info tree, and then returns that info tree, waiting for any snapshot tasks on the way. Subtrees that do not contain the position are skipped without forcing their tasks. If the caller of this function needs the correct snapshot when the cursor is on whitespace, then this function is likely the wrong one to call, as it simply yields the first snapshot that contains hoverPos in its whitespace, which is not necessarily the correct one (e.g. it may be indentation-sensitive).

Equations

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

def Lean.Language.SnapshotTree.foldInfosInRange {α : Type u_1} (tree : SnapshotTree) (requestedRange : Syntax.Range) (init : α) (f : Elab.ContextInfo → Elab.Info → α → α) : Task α

Equations

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

def Lean.Language.SnapshotTree.collectMessagesInRange (tree : SnapshotTree) (requestedRange : Syntax.Range) : Task MessageLog

Equations

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

def Lean.Language.Lean.findCmdParsedSnap (initSnap : InitialSnapshot) (text : FileMap) (hoverPos : String.Pos.Raw) : Task (Option CommandParsedSnapshot)

Finds the first CommandParsedSnapshot containing hoverPos, asynchronously.

Equations

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

def Lean.Language.Lean.findCmdDataAtPos (initSnap : InitialSnapshot) (text : FileMap) (hoverPos : String.Pos.Raw) (includeStop : Bool) : Task (Option (Syntax × Elab.InfoTree))

Finds the command syntax and info tree of the first snapshot task containing pos, asynchronously. The info tree may be from a nested snapshot, such as a single tactic.

See SnapshotTree.findInfoTreeAtPos for details on how the search is done.

Equations

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

def Lean.Language.Lean.findInfoTreeAtPos (initSnap : InitialSnapshot) (text : FileMap) (hoverPos : String.Pos.Raw) (includeStop : Bool) : Task (Option Elab.InfoTree)

Finds the info tree of the first snapshot task containing pos, asynchronously. The info tree may be from a nested snapshot, such as a single tactic.

See SnapshotTree.findInfoTreeAtPos for details on how the search is done.

Equations

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