using widgets

Stream: general

[Scott Morrison]

@Edward Ayers, I'm not managing to get the example usage of #html working. I have:

open widget

meta def counter_widget {π α : Type} : component π α :=
component.ignore_props $ component.mk_simple int int 0 (λ _ x y, (x + y, none)) (λ _ s,
  h "div" [] [
    button "+" (1 : int),
    html.of_string $ to_string $ s,
    button "-" (-1)
  ]
)

#html counter_widget

example : true :=
begin

end

and I'm running the extension you linked to in the previous message.

But no where that I can find is this widget rendered...?

[Scott Morrison]

Screenshot-2020-06-15-11.20.12.png

[Edward Ayers]

Hi Scott, clicking anywhere in the #html keyword should show the widget in the infoview.

[Edward Ayers]

From the screenshot it looks like the system is working

[Edward Ayers]

The idea is that #html works the same as #eval or #check where the thing is displayed over the keyword

[Edward Ayers]

In the tactic block, you will only ever see the widgets that are added through the tactic.save_info method. If you want custom widgets in the tactic state, you can write your own custom tactics with a custom my_tactic.save_info or you can vm_override tactic.save_info