Selection panel utilities #
The main declaration is
mkSelectionPanelRPC which helps creating rpc methods for widgets
generating tactic calls based on selected sub-expressions in the main goal.
There are also some minor helper functions.
Replace the sub-expression at the given position by a fresh meta-variable.
Structures providing parameters for a Select and insert widget.
- pos : Lean.Lsp.Position
Cursor position in the file at which the widget is being displayed.
The current tactic-mode goals.
Locations currently selected in the goal state.
- replaceRange : Lean.Lsp.Range
The range in the source document where the command will be inserted.
Helper function to create a widget allowing to select parts of the main goal and then display a link that will insert some tactic call.
The main argument is
mkCmdStr which is a function creating the link text and the tactic call text.
helpMsg argument is displayed when nothing is selected and
title is used as a panel title.
onlyGoal argument says whether the selected has to be in the goal. Otherwise it
can be in the local context.
onlyOne argument says whether one should select only one sub-expression.
In every cases, all selected subexpressions should be in the main goal or its local context.
The last arguments
params should not be provided so that the output
Params → RequestM (RequestTask Html) and can be fed to the
Note that the
goalType arguments to
mkCmdStr could be extracted for the
argument but that extraction would happen in every example, hence it is factored out here.
We also make sure
mkCmdStr is executed in the right context.
- One or more equations did not get rendered due to their size.