Defines the basic class of parameters for a select and insert widget.
This needs to be in a separate file in order to initialize the deriving handler.
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.