def Lean.Meta.Hint.tryThisDiffWidget : Widget.Module

A widget for rendering code action suggestions in error messages. Generally, this widget should not be used directly; instead, use MessageData.hint. Note that this widget is intended only for use within message data; it may not display line breaks properly if rendered as a panel widget.

The props to this widget are of the following form:

{
  "diff": [
    {"type": "unchanged", "text": "h"},
    {"type": "deletion", "text": "ello"},
    {"type": "insertion", "text": "i"}
  ],
  "suggestion": "hi",
  "range": {
    "start": {"line": 100, "character": 0},
    "end":   {"line": 100, "character": 5}
  }
}

Note: we cannot add the builtin_widget_module attribute here because that would require importing Lean.Widget.UserWidget, which in turn imports much of Lean.Elab -- the module where we want to be able to use this widget. Instead, we register the attribute post-hoc when we declare the regular "Try This" widget in Lean.Meta.Tactic.TryThis.

Equations

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

inductive Lean.Meta.Hint.DiffGranularity : Type

The granularity at which to display an inline diff for a suggested edit.

• auto : DiffGranularity

  Automatically select diff granularity based on edit distance.

• char : DiffGranularity

  Character-level diff.

• word : DiffGranularity

  Diff using whitespace-separated tokens.

• all : DiffGranularity

  "Monolithic" diff: shows a deletion of the entire existing source, followed by an insertion of the entire suggestion.

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

A code action suggestion associated with a hint in a message.

Refer to TryThis.Suggestion. This extends that structure with the following fields:

• span?: the span at which this suggestion should apply. This allows a single hint to suggest modifications at different locations. If span? is not specified, then the syntax reference provided to MessageData.hint will be used.
• diffGranularity: the granularity at which the diff for this suggestion should be rendered in the Infoview. See DiffMode for the possible granularities. This is .auto by default.

• suggestion : SuggestionText
• preInfo? : Option String
• postInfo? : Option String
• style? : Option SuggestionStyle
• messageData? : Option MessageData
• toCodeActionTitle? : Option (String → String)
• span? : Option Syntax
• diffGranularity : DiffGranularity

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

Equations

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

instance Lean.Meta.Hint.instToMessageDataSuggestion : ToMessageData Suggestion

Equations

• Lean.Meta.Hint.instToMessageDataSuggestion = { toMessageData := fun (s : Lean.Meta.Hint.Suggestion) => Lean.toMessageData s.toTryThisSuggestion }

def Lean.Meta.Hint.readableDiff (s s' : String) (granularity : DiffGranularity := DiffGranularity.auto) : Array (Diff.Action × String)

Produces a diff that splits either on characters, tokens, or not at all, depending on the selected diffMode.

Guarantees that all actions in the output will be maximally grouped; that is, instead of returning #[(.insert, "a"), (.insert, "b")], it will return #[(.insert, "ab")].

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Hint.readableDiff s s' Lean.Meta.Hint.DiffGranularity.char = Lean.Meta.Hint.readableDiff.charDiff s s'
• Lean.Meta.Hint.readableDiff s s' Lean.Meta.Hint.DiffGranularity.word = Lean.Meta.Hint.readableDiff.wordDiff s s'
• Lean.Meta.Hint.readableDiff s s' Lean.Meta.Hint.DiffGranularity.all = Lean.Meta.Hint.readableDiff.maxDiff s s'

def Lean.Meta.Hint.readableDiff.wordDiff (s s' : String) : Array (Diff.Action × String)

Equations

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

def Lean.Meta.Hint.readableDiff.charDiff (s s' : String) : Array (Diff.Action × String)

Equations

• Lean.Meta.Hint.readableDiff.charDiff s s' = Lean.Meta.Hint.readableDiff.joinCharDiff (Lean.Diff.diff (Lean.Meta.Hint.readableDiff.splitChars s) (Lean.Meta.Hint.readableDiff.splitChars s'))

def Lean.Meta.Hint.readableDiff.joinCharDiff (d : Array (Diff.Action × Char)) : Array (Diff.Action × String)

Given a Char diff, produces an equivalent String diff, joining actions of the same kind.

Equations

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

def Lean.Meta.Hint.readableDiff.maxDiff (s s' : String) : Array (Diff.Action × String)

Equations

• Lean.Meta.Hint.readableDiff.maxDiff s s' = #[(Lean.Diff.Action.delete, s), (Lean.Diff.Action.insert, s')]

def Lean.Meta.Hint.readableDiff.mkWhitespaceDiff (oldWs newWs : String) : Array (Diff.Action × String)

Equations

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

def Lean.Meta.Hint.readableDiff.splitChars (s : String) : Array Char

Equations

• Lean.Meta.Hint.readableDiff.splitChars s = s.toList.toArray

def Lean.Meta.Hint.readableDiff.splitWords (s : String) : Array String × Array String

Equations

• Lean.Meta.Hint.readableDiff.splitWords s = Lean.Meta.Hint.readableDiff.splitWordsAux s 0 0 #[] #[]

partial def Lean.Meta.Hint.readableDiff.splitWordsAux (s : String) (b i : String.Pos) (r ws : Array String) : Array String × Array String

def Lean.Meta.Hint.readableDiff.joinEdits {α : Type} (ds : Array (Diff.Action × α)) : Array (Diff.Action × Array α)

Equations

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

def Lean.Meta.Hint.mkSuggestionsMessage (suggestions : Array Suggestion) (ref : Syntax) (codeActionPrefix? : Option String) : CoreM MessageData

Creates message data corresponding to a HintSuggestions collection and adds the corresponding info leaf.

Equations

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

def Lean.MessageData.hint (hint : MessageData) (suggestions : Array Meta.Hint.Suggestion) (ref? : Option Syntax := none) (codeActionPrefix? : Option String := none) : CoreM MessageData

Creates a hint message with associated code action suggestions.

To provide a hint without an associated code action, use MessageData.hint'.

The arguments are as follows:

• hint: the main message of the hint, which precedes its code action suggestions.
• suggestions: the suggestions to display.
• ref?: if specified, the syntax location for the code action suggestions; otherwise, default to the syntax reference in the monadic state. Will be overridden by the span? field on any suggestions that specify it.
• codeActionPrefix?: if specified, text to display in place of "Try this: " in the code action label

Equations

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