-
Notifications
You must be signed in to change notification settings - Fork 80
/
html_cmd.lean
35 lines (32 loc) · 1001 Bytes
/
html_cmd.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
/-
Copyright (c) E.W.Ayers. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: E.W.Ayers
-/
prelude
import init.meta.widget.basic
import init.meta.lean.parser
import init.meta.interactive_base
import init.data.punit
open lean
open lean.parser
open interactive
open tactic
open widget
/-- Accepts terms with the type `component tactic_state empty` or `html empty` and
renders them interactively. -/
@[user_command]
meta def show_widget_cmd (x : parse $ tk "#html") : parser unit := do
⟨l,c⟩ ← cur_pos,
y ← parser.pexpr 0,
comp ← parser.of_tactic ((do
tactic.eval_pexpr (component tactic_state empty) y
) <|> (do
htm : html empty ← tactic.eval_pexpr (html empty) y,
c : component unit empty ← pure $ component.stateless (λ _, [htm]),
pure $ component.ignore_props $ component.ignore_action $ c
)),
save_widget ⟨l,c - ("#html").length - 1⟩ comp,
trace "successfully rendered widget"
pure ()
run_cmd skip