"Try this" data types

This defines the data types used in constructing "try this" widgets for suggestion-providing tactics and inline error-message hints, as well as basic infrastructure for generating info trees and widget content there from.

Code action information

structure Lean.Meta.Tactic.TryThis.TryThisInfo : Type

A packet of information about a "Try this" suggestion that we store in the infotree for the associated code action to retrieve.

• range : Lsp.Range

  The textual range to be replaced by one of the suggestions.

• suggestionTexts : Array (String × Option String)

  A list of suggestions for the user to choose from. Each suggestion may optionally come with an override for the code action title.

• codeActionPrefix? : Option String

  The prefix to display before the code action for a "Try this" suggestion if no custom code action title is provided. If not provided, "Try this: " is used.

instance Lean.Meta.Tactic.TryThis.instTypeNameTryThisInfo : TypeName TryThisInfo

Suggestion data

inductive Lean.Meta.Tactic.TryThis.SuggestionText : Type

Text to be used as a suggested replacement in the infoview. This can be either a TSyntax kind for a single kind : SyntaxNodeKind or a raw String.

Instead of using constructors directly, there are coercions available from these types to SuggestionText.

• tsyntax {kind : SyntaxNodeKind} : TSyntax kind → SuggestionText

  TSyntax kind used as suggested replacement text in the infoview. Note that while TSyntax is in general parameterized by a list of SyntaxNodeKinds, we only allow one here; this unambiguously guides pretty-printing.

• string : String → SuggestionText

  A raw string to be used as suggested replacement text in the infoview.

instance Lean.Meta.Tactic.TryThis.instInhabitedSuggestionText : Inhabited SuggestionText

instance Lean.Meta.Tactic.TryThis.instToMessageDataSuggestionText : ToMessageData SuggestionText

instance Lean.Meta.Tactic.TryThis.instCoeHeadTSyntaxConsSyntaxNodeKindNilSuggestionText {kind : SyntaxNodeKind} : CoeHead (TSyntax kind) SuggestionText

instance Lean.Meta.Tactic.TryThis.instCoeStringSuggestionText : Coe String SuggestionText

def Lean.Meta.Tactic.TryThis.SuggestionStyle : Type

Style hooks for Suggestions. See SuggestionStyle.error, .warning, .success, .value, and other definitions here for style presets. This is an arbitrary Json object, with the following interesting fields:

• title: the hover text in the suggestion link
• className: the CSS classes applied to the link
• style: A Json object with additional inline CSS styles such as color or textDecoration.

instance Lean.Meta.Tactic.TryThis.instSuggestionStyleInhabited : Inhabited SuggestionStyle

instance Lean.Meta.Tactic.TryThis.instSuggestionStyleToJson : ToJson SuggestionStyle

def Lean.Meta.Tactic.TryThis.SuggestionStyle.error (decorated : Bool := true) : SuggestionStyle

Style as an error. By default, decorates the text with an undersquiggle; providing the argument decorated := false turns this off.

def Lean.Meta.Tactic.TryThis.SuggestionStyle.warning (decorated : Bool := true) : SuggestionStyle

Style as a warning. By default, decorates the text with an undersquiggle; providing the argument decorated := false turns this off.

def Lean.Meta.Tactic.TryThis.SuggestionStyle.success : SuggestionStyle

Style as a success.

def Lean.Meta.Tactic.TryThis.SuggestionStyle.asHypothesis : SuggestionStyle

Style the same way as a hypothesis appearing in the infoview.

def Lean.Meta.Tactic.TryThis.SuggestionStyle.asInaccessible : SuggestionStyle

Style the same way as an inaccessible hypothesis appearing in the infoview.

def Lean.Meta.Tactic.TryThis.SuggestionStyle.value (t : Float) (showValueInHoverText : Bool := true) : SuggestionStyle

Draws the color from a red-yellow-green color gradient with red at 0.0, yellow at 0.5, and green at 1.0. Values outside the range [0.0, 1.0] are clipped to lie within this range.

With showValueInHoverText := true (the default), the value t will be included in the title of the HTML element (which appears on hover).

structure Lean.Meta.Tactic.TryThis.Suggestion : Type

Holds a suggestion for replacement, along with preInfo and postInfo strings to be printed immediately before and after that suggestion, respectively. It also includes an optional MessageData to represent the suggestion in logs; by default, this is none, and suggestion is used.

• suggestion : SuggestionText

  Text to be used as a replacement via a code action.

• preInfo? : Option String

  Optional info to be printed immediately before replacement text in a widget.

• postInfo? : Option String

  Optional info to be printed immediately after replacement text in a widget.

• style? : Option SuggestionStyle

  Optional style specification for the suggestion. If none (the default), the suggestion is styled as a text link. Otherwise, the suggestion can be styled as:

  • a status: .error, .warning, .success
  • a hypothesis name: .asHypothesis, .asInaccessible
  • a variable color: .value (t : Float), which draws from a red-yellow-green gradient, with red at 0.0 and green at 1.0.

  See SuggestionStyle for details.

  Note that this property is used only by the "try this" widget; it is ignored by the inline hint widget.

• messageData? : Option MessageData

  How to represent the suggestion as MessageData. This is used only in the info diagnostic. If none, we use suggestion. Use toMessageData to render a Suggestion in this manner.

• toCodeActionTitle? : Option (String → String)

  How to construct the text that appears in the lightbulb menu from the suggestion text. If none, we use fun ppSuggestionText => "Try this: " ++ ppSuggestionText. Only the pretty-printed suggestion : SuggestionText is used here.

instance Lean.Meta.Tactic.TryThis.instInhabitedSuggestion : Inhabited Suggestion

instance Lean.Meta.Tactic.TryThis.instToMessageDataSuggestion : ToMessageData Suggestion

instance Lean.Meta.Tactic.TryThis.instCoeSuggestionTextSuggestion : Coe SuggestionText Suggestion

Formatting

def Lean.Meta.Tactic.TryThis.getIndentAndColumn (map : FileMap) (range : String.Range) : Nat × Nat

Yields (indent, column) given a FileMap and a String.Range, where indent is the number of spaces by which the line that first includes range is initially indented, and column is the column range starts at in that line.

opaque Lean.Meta.Tactic.TryThis.format.inputWidth : Lean.Option Nat

An option allowing the user to customize the ideal input width. Defaults to 100. This option controls output format when the output is intended to be copied back into a lean file

def Lean.Meta.Tactic.TryThis.getInputWidth (o : Options) : Nat

Get the input width specified in the options

def Lean.Meta.Tactic.TryThis.SuggestionText.pretty : SuggestionText → CoreM Format

Pretty-prints a SuggestionText as a Format. If the SuggestionText is some TSyntax kind, we use the appropriate pretty-printer; strings are coerced to Formats as-is.

def Lean.Meta.Tactic.TryThis.SuggestionText.prettyExtra (s : SuggestionText) (w : Option Nat := none) (indent column : Nat := 0) : CoreM String

Pretty-prints a SuggestionText as a String and wraps with respect to the pane width, indentation, and column, via Format.prettyExtra. If w := none, then w := getInputWidth (← getOptions) is used. Raw Strings are returned as-is.

def Lean.Meta.Tactic.TryThis.Suggestion.toJsonAndInfoM (s : Suggestion) (w : Option Nat := none) (indent column : Nat := 0) : CoreM (Json × String × Option String)

Converts a Suggestion to Json in CoreM. We need CoreM in order to pretty-print syntax.

This also returns a String × Option String consisting of the pretty-printed text and any custom code action title if toCodeActionTitle? is provided.

If w := none, then w := getInputWidth (← getOptions) is used.

structure Lean.Meta.Tactic.TryThis.ProcessedSuggestions : Type

Represents processed data for a collection of suggestions that can be passed to a widget and pushed in an info leaf.

It contains the following data:

• suggestions: tuples of the form (j, t, p) where j is JSON containing a suggestion and its pre- and post-info, t is the text to be inserteed by the suggestion, and p is the code action prefix thereof.
• info: the TryThisInfo data corresponding to a collection of suggestions
• range: the range at which the suggestion is to be applied.

• suggestions : Array (Json × String × Option String)
• info : Elab.Info
• range : Lsp.Range

def Lean.Meta.Tactic.TryThis.processSuggestions (ref : Syntax) (range : String.Range) (suggestions : Array Suggestion) (codeActionPrefix? : Option String) : CoreM ProcessedSuggestions

Processes an array of Suggestions into data that can be used to construct a code-action info leaf and "try this" widget.