A Go-To-Module widget

This file defines:

• goToModule, a clickable widget bringing the user to a given module (at a customizable position and with customizable visible text)
• goToModuleOfDecls/goToModuleOfDecl, the same for bringing the user to the position before or after declarations from a (single) module, as specified

def ImportGraph.Widget.getModuleUri (modName : Lean.Name) : Lean.Server.RequestM (Lean.Server.RequestTask Lean.Lsp.DocumentUri)

Tries to resolve the module modName to a source file URI. This has to be done in the Lean server since the Environment does not keep track of source URIs.

Equations

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

structure ImportGraph.Widget.GoToModuleProps : Type

Widget props for ImportGraph.Widget.GoToModule.

• modName : Lean.Name
• pos : Lean.Lsp.Position
• overrideText : Option String

@[instance_reducible]

instance ImportGraph.Widget.instRpcEncodableGoToModuleProps : Lean.Server.RpcEncodable GoToModuleProps

Equations

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

def ImportGraph.Widget.GoToModule : Lean.Widget.Module

When clicked, this widget component jumps to the source of the module modName at the provided pos, assuming a source URI can be found for the module. Allows `override

Equations

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

def ImportGraph.Widget.pastEndOfFile : Lean.Lsp.Position

A position past the end of any file, assuming no file has more than 4294967296 lines.

Equations

• ImportGraph.Widget.pastEndOfFile = { line := 1 <<< 32, character := 0 }

def ImportGraph.Widget.goToModule (modName : Lean.Name) (pos : Lean.Lsp.Position := { line := 0, character := 0 }) (overrideText : Option String := none) : Lean.CoreM Lean.MessageData

Creates a clickable link which takes the user to the provided module.

By default, takes the user to the top of the module. Providing pos will bring the user to that position in the file.

By default, the module name is used as the link's text. The text can be overridden by providing overrideText.

Equations

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

def ImportGraph.Widget.getMaxDeclarationRange? (decls : Array Lean.Name) : Lean.CoreM (Option Lean.DeclarationRange)

Gets the latest-ending range among all declarations, or none if none could be found. Assumes all declarations come from the same module.

Equations

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

def ImportGraph.Widget.getMinDeclarationRange? (decls : Array Lean.Name) : Lean.CoreM (Option Lean.DeclarationRange)

Gets the earliest-starting range among all declarations, or none if none could be found. Assumes all declarations come from the same module.

Equations

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

inductive ImportGraph.Widget.RelativeRangeLocation : Type

Where the cursor should end up relative to given range(s) after a go-to-module.

• start (lineBefore : Bool := true) : RelativeRangeLocation

  Places the cursor by default on the line before the range(s). If lineBefore := false, places the cursor just at the start of the range(s).

• end (lineAfter : Bool := true) : RelativeRangeLocation

  Places the cursor by default on the line after the range(s). If lineAfter := false, places the cursor just at the end of the range(s).

def ImportGraph.Widget.goToModuleOfDecls (decls : Array Lean.Name) (location : RelativeRangeLocation := RelativeRangeLocation.end) (fallbackModule : Option Lean.Name := none) (overrideText : Option String := none) : Lean.CoreM Lean.MessageData

Goes to either before or after all of the ranges of all provided decls. The location the cursor ends up may be specified by setting location:

• .end (lineAfter := true) (the default): go the first character of the line after the range of the last declaration.
• .end (lineAfter := false): place the cursor at the end of the range of the last declaration.
• .start (lineBefore := true): place the cursor on the line before the first declaration.
• .start (lineBefore := false): place the cursor at the beginning of the range of the first declaration.

(We use the full range, including e.g. the body of the declaration.)

Errors if no decl has a module and fallBackModule is not specified.

Ignores declarations with no position information (such as autogenerated declarations). If a module is found but no range can be found, goes to the end or beginning of the module, according to location.

Errors if not all declarations come from the same module.

By default, the link text is the name of decl's module. The text can be overridden with overrideText.

Equations

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

@[inline]

def ImportGraph.Widget.goToModuleOfDecl (decl : Lean.Name) (location : RelativeRangeLocation := RelativeRangeLocation.end) (overrideText : Option String := none) : Lean.CoreM Lean.MessageData

Goes to either before or after the range of the provided decl. The location the cursor ends up may be specified by setting location:

• .end (lineAfter := true) (the default): go the first character of the line of the declaration.
• .end (lineAfter := false): place the cursor at the end of the range of the declaration.
• .start (lineBefore := true): place the cursor on the line before the declaration.
• .start (lineBefore := false): place the cursor at the beginning of the range of the declaration.

(We use the full range, including e.g. the body of the declaration.)

Errors if decl has no module.

If the declaration has a module but no range can be found, goes to the end or beginning of the module, according to location.

Errors if not all declarations come from the same module.

By default, the link text is the name of decl's module. The text can be overridden with overrideText.

Equations

• ImportGraph.Widget.goToModuleOfDecl decl location overrideText = ImportGraph.Widget.goToModuleOfDecls #[decl] location none overrideText