"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

Equations

• Lean.Meta.Tactic.TryThis.instTypeNameTryThisInfo = Lean.Meta.Tactic.TryThis.inst✝

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

Equations

• Lean.Meta.Tactic.TryThis.instInhabitedSuggestionText = { default := Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax default }

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

Equations

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

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

Equations

• Lean.Meta.Tactic.TryThis.instCoeHeadTSyntaxConsSyntaxNodeKindNilSuggestionText = { coe := Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax }

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

Equations

• Lean.Meta.Tactic.TryThis.instCoeStringSuggestionText = { coe := Lean.Meta.Tactic.TryThis.SuggestionText.string }

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.

Equations

• Lean.Meta.Tactic.TryThis.SuggestionStyle = Lean.Json

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

Equations

• Lean.Meta.Tactic.TryThis.instSuggestionStyleInhabited = Lean.instInhabitedJson

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

Equations

• Lean.Meta.Tactic.TryThis.instSuggestionStyleToJson = Lean.instToJsonJson

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.

Equations

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

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.

Equations

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

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

Style as a success.

Equations

• Lean.Meta.Tactic.TryThis.SuggestionStyle.success = Lean.Json.mkObj [("className", Lean.Json.str "information pointer dim")]

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

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

Equations

• Lean.Meta.Tactic.TryThis.SuggestionStyle.asHypothesis = Lean.Json.mkObj [("className", Lean.Json.str "goal-hyp pointer dim")]

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

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

Equations

• Lean.Meta.Tactic.TryThis.SuggestionStyle.asInaccessible = Lean.Json.mkObj [("className", Lean.Json.str "goal-inaccessible pointer dim")]

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).

Equations

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

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

Equations

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

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

Equations

• Lean.Meta.Tactic.TryThis.instToMessageDataSuggestion = { toMessageData := fun (s : Lean.Meta.Tactic.TryThis.Suggestion) => s.messageData?.getD (Lean.toMessageData s.suggestion) }

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

Equations

• Lean.Meta.Tactic.TryThis.instCoeSuggestionTextSuggestion = { coe := fun (t : Lean.Meta.Tactic.TryThis.SuggestionText) => { suggestion := t } }

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.

Equations

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

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

Equations

• Lean.Meta.Tactic.TryThis.getInputWidth o = Lean.Option.get o Lean.Meta.Tactic.TryThis.format.inputWidth

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.

Equations

• (Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax stx).pretty = Lean.PrettyPrinter.ppCategory kind stx.raw
• (Lean.Meta.Tactic.TryThis.SuggestionText.string s).pretty = pure (Std.Format.text s)

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.

Equations

• One or more equations did not get rendered due to their size.
• (Lean.Meta.Tactic.TryThis.SuggestionText.string s_1).prettyExtra w indent column = pure s_1

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.

Equations

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

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.

Equations

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