Widgets used for tactic state and term-mode goal display
The vscode extension supports the display of interactive widgets.
Default implementation of these widgets are included in the core
library. We override them here using vm_override so that we can
change them quickly without waiting for the next Lean release.
The function widget_override.interactive_expression.mk renders a single
expression as a widget component. Each goal in a tactic state is rendered
using the widget_override.tactic_view_goal function,
a complete tactic state is rendered using
widget_override.tactic_view_component.
Lean itself calls the widget_override.term_goal_widget function to render
term-mode goals and widget_override.tactic_state_widget to render the
tactic state in a tactic proof.
- tag_expr : expr.address → expr → widget_override.interactive_expression.sf → widget_override.interactive_expression.sf
- compose : widget_override.interactive_expression.sf → widget_override.interactive_expression.sf → widget_override.interactive_expression.sf
- of_string : string → widget_override.interactive_expression.sf
eformat but without any of the formatting stuff like highlighting, groups etc.
Prints a debugging representation of an sf object.
Constructs an sf from an eformat by forgetting grouping, nesting, etc.
Flattens an sf, i.e. merges adjacent of_string constructors.
Post-process an sf object to eliminate tags for partial applications by
pushing the app_fn as far into the expression as possible. The effect is
that clicking on a sub-expression always includes the full argument list in
the popup.
Consider the expression id id 0. We push the app_fn for the partial
application id id inwards and eliminate it. Before:
(tag_expr [app_fn]
`(id.{1} (nat -> nat) (id.{1} nat))
(tag_expr [app_fn] `(id.{1} (nat -> nat)) "id")
"\n"
(tag_expr [app_arg] `(id.{1} nat) "id"))
"\n"
(tag_expr [app_arg] `(has_zero.zero.{0} nat nat.has_zero) "0")
After:
"id"
"\n"
(tag_expr [app_fn, app_arg] `(id.{1} nat) "id")
"\n"
(tag_expr [app_arg] `(has_zero.zero.{0} nat nat.has_zero) "0")
- on_mouse_enter : Π (γ : Type), subexpr → widget_override.interactive_expression.action γ
- on_mouse_leave_all : Π (γ : Type), widget_override.interactive_expression.action γ
- on_click : Π (γ : Type), subexpr → widget_override.interactive_expression.action γ
- on_tooltip_action : Π (γ : Type), γ → widget_override.interactive_expression.action γ
- on_close_tooltip : Π (γ : Type), widget_override.interactive_expression.action γ
- copy : Π (γ : Type), string → widget_override.interactive_expression.action γ
The actions accepted by an expression widget.
Renders a subexpression as a list of html elements.
Component for the type tooltip.
- none : widget_override.filter_type
- no_instances : widget_override.filter_type
- only_props : widget_override.filter_type
Supported tactic state filters.
Filters a local constant using the given filter.
Component for the filter dropdown.
Converts a name into an html element.
Converts a single local constant into a (singleton) local_collection
Groups consecutive local collections by type
Component that displays the main (first) goal.
- out : Π (γ : Type), γ → widget_override.tactic_view_action γ
- filter : Π (γ : Type), widget_override.filter_type → widget_override.tactic_view_action γ
Actions accepted by the tactic_view_component.
The "goals accomplished 🎉" HTML widget. This can be overridden using:
meta def my_new_msg {α : Type} : widget.html α := "my message"
attribute [vm_override my_new_msg] widget_override.goals_accomplished_message
Component that displays all goals, together with the $n goals message.
Component that displays the term-mode goal.
Component showing a local collection.
Component showing the current tactic state.
Widget used to display term-proof goals.