"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 #
This is a widget which is placed by TryThis.addSuggestion
and TryThis.addSuggestions
.
When placed by addSuggestion
, it says Try this: <replacement>
where <replacement>
is a link which will perform the replacement.
When placed by addSuggestions
, it says:
Try these:
<replacement1>
<replacement2>
<replacement3>
- ...
where <replacement*>
is a link which will perform the replacement.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Code action #
This is a code action provider that looks for TryThisInfo
nodes and supplies a code action to
apply the replacement.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 three effects:
- An info diagnostic is displayed saying
Try this: <suggestion>
- A widget is registered, 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 info diagnostics
: aSuggestion
, which containssuggestion
: the replacement text;preInfo?
: an optional string shown immediately after the replacement text in the widget message (only)postInfo?
: an optional string shown immediately after the replacement text in the widget message (only)style?
: an optionalJson
object used as the value of thestyle
attribute of the suggestion text's element (not the whole suggestion element).messageData?
: an optional message to display in place ofsuggestion
in the info diagnostic (only). The widget message uses onlysuggestion
. IfmessageData?
isnone
, we simply usesuggestion
instead.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.
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 three effects:
- An info diagnostic is displayed saying
Try these: <list of suggestions>
- A widget is registered, saying
Try these: <list of suggestions>
with a link on each<suggestion>
to apply the suggestion - A code action for each suggestion is added, which will apply the suggestion.
The parameters are:
ref
: the span of the info diagnosticsuggestions
: an array ofSuggestion
s, which each containsuggestion
: the replacement text;preInfo?
: an optional string shown immediately after the replacement text in the widget message (only)postInfo?
: an optional string shown immediately after the replacement text in the widget message (only)style?
: an optionalJson
object used as the value of thestyle
attribute of the suggestion text's element (not the whole suggestion element).messageData?
: an optional message to display in place ofsuggestion
in the info diagnostic (only). The widget message uses onlysuggestion
. IfmessageData?
isnone
, we simply usesuggestion
instead.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?
: a default style for all suggestions which do not have a customstyle?
set.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
Tactic-specific widget hooks #
Add an exact e
or refine e
suggestion.
The parameters are:
ref
: the span of the info 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 info 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 info 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 info 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 info 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