"Try this" code action and tactic suggestions #
This implements a mechanism for tactics to print a message saying Try this: <suggestion>
,
where <suggestion>
is a link to a replacement tactic. Users can either click on the link
in the suggestion (provided by a widget), or use a code action which applies the suggestion.
Raw widget #
Code action #
Formatting #
Delaborate e
into syntax suitable for use by refine
.
Equations
Instances For
Delaborate e
into a suggestion suitable for use by refine
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Add a "try this" suggestion. This has two effects:
- A widget diagnostic is displayed, saying
Try this: <suggestion>
with a link on<suggestion>
to apply the suggestion - A code action is added, which will apply the suggestion.
The parameters are:
ref
: the span of the widget diagnostics
: aSuggestion
, which containssuggestion
: the replacement textpreInfo?
: an optional string shown immediately before the replacement text in the widget message (only)postInfo?
: an optional string shown immediately after the replacement text in the widget message (only)messageData?
: an optionalMessageData
displayed instead ofsuggestion
. If set, impliesdiffGranularity = .none
.toCodeActionTitle?
: an optional functionString → String
describing how to transform the pretty-printed suggestion text into the code action text which appears in the lightbulb menu. Ifnone
, we simply prepend"Try This: "
to the suggestion text.
origSpan?
: a syntax object whose span is the actual text to be replaced bysuggestion
. If not provided it defaults toref
.header
: a string that begins the display. By default, it is"Try this:"
.codeActionPrefix?
: an optional string to be used as the prefix of the replacement text if the suggestion does not have a customtoCodeActionTitle?
. If not provided,"Try this: "
is used.diffGranularity
: How to compute the diff display in the suggestion. Defaults to only displaying the inserted string.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Add a list of "try this" suggestions as a single "try these" suggestion. This has two effects:
- A widget diagnostic is displayed, saying
Try these: <list of suggestions>
with a link on each suggestion in<list of suggestions>
to apply each suggestion - A code action for each suggestion is added, which will apply the suggestion.
The parameters are:
ref
: the span of the widget diagnosticsuggestions
: an array ofSuggestion
s, which each containsuggestion
: the replacement textpreInfo?
: an optional string shown immediately before the replacement text in the widget message (only)postInfo?
: an optional string shown immediately after the replacement text in the widget message (only)messageData?
: an optionalMessageData
displayed instead ofsuggestion
. If set, impliesdiffGranularity = .none
.toCodeActionTitle?
: an optional functionString → String
describing how to transform the pretty-printed suggestion text into the code action text which appears in the lightbulb menu. Ifnone
, we simply prepend"Try this: "
to the suggestion text.
origSpan?
: a syntax object whose span is the actual text to be replaced bysuggestion
. If not provided it defaults toref
.header
: a string that precedes the list. By default, it is"Try these:"
.style?
(deprecated): unused.codeActionPrefix?
: an optional string to be used as the prefix of the replacement text for all suggestions which do not have a customtoCodeActionTitle?
. If not provided,"Try this: "
is used.diffGranularity
: How to compute the diff display in the suggestion. Defaults to only displaying the inserted string.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Tactic-specific widget hooks #
Add an exact e
or refine e
suggestion.
The parameters are:
ref
: the span of the widget diagnostice
: the replacement expressionorigSpan?
: a syntax object whose span is the actual text to be replaced bysuggestion
. If not provided it defaults toref
.addSubgoalsMsg
: if true (default false), any remaining subgoals will be shown afterRemaining subgoals:
codeActionPrefix?
: an optional string to be used as the prefix of the replacement text if the suggestion does not have a customtoCodeActionTitle?
. If not provided,"Try this: "
is used.checkState?
: if passed, the tactic state in which the generated tactic will be validated, insertingexpose_names
if necessary.tacticErrorAsInfo
: if true (default false), if a generated tactic is invalid (e.g., due to a pretty-printing issue), the resulting error message will be logged as an info message instead of being thrown as an error. Has no effect ifcheckState?
isnone
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Add exact e
or refine e
suggestions if they can be successfully generated; for those that
cannot, display messages indicating the invalid generated tactics.
The parameters are:
ref
: the span of the widget diagnostices
: the array of replacement expressionsorigSpan?
: a syntax object whose span is the actual text to be replaced bysuggestion
. If not provided it defaults toref
.addSubgoalsMsg
: if true (default false), any remaining subgoals will be shown afterRemaining subgoals:
codeActionPrefix?
: an optional string to be used as the prefix of the replacement text for all suggestions which do not have a customtoCodeActionTitle?
. If not provided,"Try this: "
is used.checkState?
: if passed, the tactic state in which the generated tactics will be validated, insertingexpose_names
if necessary.tacticErrorAsInfo
: if true (default true), invalid generated tactics will log info messages instead of throwing an error. The default behavior differs fromaddExactSuggestion
because throwing an error means that any subsequent suggestions will not be displayed. Has no effect ifcheckState?
isnone
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Add a term suggestion.
The parameters are:
ref
: the span of the widget diagnostice
: the replacement expressionorigSpan?
: a syntax object whose span is the actual text to be replaced bysuggestion
. If not provided it defaults toref
.header
: a string which precedes the suggestion. By default, it's"Try this:"
.codeActionPrefix?
: an optional string to be used as the prefix of the replacement text if the suggestion does not have a customtoCodeActionTitle?
. If not provided,"Try this: "
is used.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Add term suggestions.
The parameters are:
ref
: the span of the widget diagnostices
: an array of the replacement expressionsorigSpan?
: a syntax object whose span is the actual text to be replaced bysuggestion
. If not provided it defaults toref
.header
: a string which precedes the list of suggestions. By default, it's"Try these:"
.codeActionPrefix?
: an optional string to be used as the prefix of the replacement text for all suggestions which do not have a customtoCodeActionTitle?
. If not provided,"Try this: "
is used.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Add a suggestion for have h : t := e
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Add a suggestion for rw [h₁, ← h₂] at loc
.
Parameters:
ref
: the span of the widget diagnosticrules
: a list of arguments torw
, with the second componenttrue
if the rewrite is reversedtype?
: the goal after the suggested rewrite,.none
if the rewrite closes the goal, or.undef
if the resulting goal is unknownloc?
: the hypothesis at which the rewrite is performed, ornone
if the goal is targetedorigSpan?
: a syntax object whose span is the actual text to be replaced bysuggestion
. If not provided it defaults toref
.checkState?
: if passed, the tactic state in which the generated tactic will be validated, insertingexpose_names
if necessary