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"}
]
}
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
Instances For
A code action suggestion associated with a hint in a message.
Refer to TryThis.Suggestion
; this extends that structure with a span?
field, allowing 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.
- toCodeActionTitle? : Option (String → String)
Instances For
Produces a diff that splits either on characters, tokens, or not at all, depending on the edit distance between the arguments.
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
Instances For
Equations
Instances For
Creates message data corresponding to a HintSuggestions
collection and adds the corresponding info
leaf.
Equations
Instances For
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 thespan?
field on any suggestions that specify it.codeActionPrefix?
: if specified, text to display in place of "Try this: " in the code action label