feat: user widgets#1238

Merged

leodemoura merged 18 commits intoleanprover:masterfrom

Vtec234:widget-pr

Jul 25, 2022

Commits on Jul 20, 2022

feat: user widgets
EdAyers
committed
chore: remove Json.syntax docstring
EdAyers
committed
refactor: getWidgetInfos → getWidgets
EdAyers
committed
chore: use invalidParams error code

Vtec234
authored and
EdAyers
committed
chore: rebase on 2022-07-10

Vtec234
authored and
EdAyers
committed
fix: widgets are now defined using a `UserWidgetDefinition`
EdAyers
committed
doc: update widget docs
EdAyers
committed
style: userwidget
EdAyers
committed
test: remove unused rpc case from runner
EdAyers
committed
style: tests/lean/interactive/run.lean

EdAyers
and
gebner
committed
fix: local instances
EdAyers
committed
fix: add Inhabited Std.RBMap
EdAyers
committed
test: fix infoTree.lean

Vtec234
authored and
EdAyers
committed
test: strip some more indices

Vtec234
authored and
EdAyers
committed
doc: fix @kha issues
EdAyers
committed
fix: widgetSourceRegistry now stores the UserWidgetDefinition declaration name instead of WidgetSource
EdAyers
committed

Commits on Jul 23, 2022

refactor: simplify position type
Vtec234
committed

Commits on Jul 24, 2022

fix: tests
Vtec234
committed