mathlib documentation

core / init.meta.widget.basic

A component is a piece of UI which may contain internal state. Use component.mk to build new components.

Using widgets. #

To make a widget, you need to make a custom executor object and then instead of calling save_info_thunk you call save_widget.

Additionally, you will need a compatible build of the vscode extension or web app to use widgets in vscode.

How it works: #

The design is inspired by React. If you are familiar with using React or Elm or a similar functional UI framework then that's helpful for this. The React article on reconciliation might be helpful.

One can imagine making a UI for a particular object as just being a function f : α → UI where UI is some inductive datatype for buttons, textboxes, lists and so on. The process of evaluating f is called rendering. So for example α could be tactic_state and the function renders a goal view.

HTML #

For our purposes, UI is an HTML tree and is written html α : Type. I'm going to assume some familiarity with HTML for the purposes of this document. An HTML tree is composed of elements and strings. Each element has a tag such as "div", "span", "article" and so on and a set of attributes and child html. Use the helper function h : stringlist (attr α) → list (html α) → html α to build new pieces of html. So for example:

h "ul" [] [
     h "li" [] ["this is list item 1"],
     h "li" [style [("color", "blue")]] ["this is list item 2"],
     h "hr" [] [],
     h "li" [] [
          h "span" [] ["there is a button here"],
          h "button" [on_click (λ _, 3)] ["click me!"]
     ]
]

Has the type html nat. The nat type is called the action and whenever the user interacts with the UI, the html will emit an object of type nat. So for example if the user clicks the button above, the html will 'emit' 3. The above example is compiled to the following piece of html:

<ul>
  <li>this is list item 1</li>
  <li style="{ color: blue; }">this is list item 2</li>
  <hr/>
  <li>
     <span>There is a button here</span>
     <button onClick="[handler]">click me!</button>
  </li>
</ul>

Components #

In order for the UI to react to events, you need to be able to take these actions α and alter some state. To do this we use components. component takes two type arguments: π and α. α is called the 'action' and π are the 'props'. The props can be thought of as a kind of wrapped function domain for component. So given C : component nat α, one can turn this into html with html.of_component 4 C : html α.

The base constructor for a component is pure:

meta def Hello : component string α := component.pure (λ s, ["hello, ", s, ", good day!"])

#html Hello "lean" -- renders "hello, lean, good day!"

So here a pure component is just a simple function π → list (html α). However, one can augment components with hooks. The hooks available for compoenents are listed in the inductive definition for component.

Here we will just look at the with_state hook, which can be used to build components with inner state.

meta inductive my_action
| increment
| decrement
open my_action

meta def Counter : component unit α :=
component.with_state
     my_action          -- the action of the inner component
     int                -- the state
     (λ _, 0)           -- initialise the state
     (λ _ _ s, s)       -- update the state if the props change
     (λ _ s a,          -- update the state if an action was received
          match a with
          | increment := (s + 1, none) -- replace `none` with `some _` to emit an action
          | decrement := (s - 1, none)
          end
     )
$ component.pure (λ state, ⟨⟩⟩, [
     button "+" (λ _, increment),
     to_string state,
     button "-" (λ _, decrement)
  ])

#html Counter ()

You can add many hooks to a component.

Given an active document, Lean (in server mode) maintains a set of widgets for the document. A widget is a component c, some p : Props and an internal state-manager which manages the states of the component and subcomponents and also handles the routing of events from the UI.

Reconciliation #

If a parent component's state changes, this can cause child components to change position or to appear and dissappear. However we want to preserve the state of these child components where we can. The UI system will try to match up these child components through a process called reconciliation.

Reconciliation will make sure that the states are carried over correctly and will also not rerender subcomponents if they haven't changed their props or state. To compute whether two components are the same, the system will perform a hash on their VM objects. Not all VM objects can be hashed, so it's important to make sure that any items that you expect to change over the lifetime of the component are fed through the 'Props' argument. This is why we need the props argument on component. The reconciliation engine uses the props_eq predicate passed to the component constructor to determine whether the props have changed and hence whether the component should be re-rendered.

Keys #

If you have some list of components and the list changes according to some state, it is important to add keys to the components so that if two components change order in the list their states are preserved. If you don't provide keys or there are duplicate keys then you may get some strange behaviour in both the Lean widget engine and react.

It is possible to use incorrect HTML tags and attributes, there is (currently) no type checking that the result is a valid piece of HTML. So for example, the client widget system will error if you add a text_change_event attribute to anything other than an element tagged with input.

Styles with Tachyons #

The widget system assumes that a stylesheet called 'tachyons' is present. You can find documentation for this stylesheet at Tachyons.io. Tachyons was chosen because it is very terse and allows arbitrary styling without using inline styles and without needing to dynamically load a stylesheet.

Further work (up for grabs!) #

inductive widget.mouse_event_kind  :
Type
meta inductive widget.effect  :
Type

An effect is some change that the widget makes outside of its own state. Usually, giving instructions to the editor to perform some task.

  • insert_text_relative will insert at a line relative to the position of the widget.
  • insert_text_absolute will insert text at the precise position given.
  • reveal_position will move the editor to view the given position.
  • highlight_position will add a text highlight to the given position.
  • clear_highlighting will remove all highlights created with highlight_position.
  • copy_text will copy the given text to the clipboard.
  • custom can be used to pass custom effects to the client without having to recompile Lean.
meta def widget.effects  :
Type
meta def widget.as_element {α : Type} :
widget.html αoption (string × list (widget.attr α) × list (widget.html α))
meta def widget.key {α β : Type} [has_to_string β] :
β → widget.attr α
meta def widget.className {α : Type} :
stringwidget.attr α
meta def widget.on_click {α : Type} :
(unit → α)widget.attr α
meta def widget.on_mouse_enter {α : Type} :
(unit → α)widget.attr α
meta def widget.on_mouse_leave {α : Type} :
(unit → α)widget.attr α
meta def widget.h {α : Type} :
stringlist (widget.attr α)list (widget.html α)widget.html α

Alias for html.element.

meta def widget.cn {α : Type} :
stringwidget.attr α

Alias for className.

meta def widget.button {α : Type} :
stringthunk αwidget.html α
meta def widget.textbox {α : Type} :
string(string → α)widget.html α
meta structure widget.select_item (α : Type) :
Type
  • result : α
  • key : string
  • view : list (widget.html α)
meta def widget.select {α : Type} [decidable_eq α] :
list (widget.select_item α)α → widget.html α

Choose from a dropdown selection list.

meta def widget.with_attrs {α : Type} :
list (widget.attr α)widget.html αwidget.html α

If the html is not an of_element it will wrap it in a div.

meta def widget.with_attr {α : Type} :
widget.attr αwidget.html αwidget.html α

If the html is not an of_element it will wrap it in a div.

meta def widget.with_style {α : Type} :
stringstringwidget.html αwidget.html α
meta def widget.with_cn {α : Type} :
stringwidget.html αwidget.html α
meta def widget.with_key {α β : Type} [has_to_string β] :
β → widget.html αwidget.html α
meta constant tactic.save_widget  :
poswidget.component tactic_state emptytactic unit

Same as tactic.save_info_thunk except saves a widget to be displayed by a compatible infoviewer.

meta constant tactic.trace_widget_at (p : pos) (w : widget.component tactic_state empty) (text : string := "(widget)") :

Outputs a widget trace position at the given position.

meta def tactic.trace_widget (w : widget.component tactic_state empty) (text : string := "(widget)") :

Outputs a widget trace position at the current default trace position.