Code

feat: bundle of widget improvements#2964

Code

Merged

kim-em merged 18 commits intoleanprover:masterleanprover/lean4:masterfrom Vtec234:widget-modulesVtec234/lean4:widget-modulesCopy head branch name to clipboardDec 21, 2023

+554-206

Commits

Commits on Dec 20, 2023

• feat: generalize UserWidgetDefinition to Widget.Module

  Vtec234

  committed
  ba856c5

  Copy full SHA for ba856c5

• feat: report duplicate widget modules

  Vtec234

  committed
  01c296d

  Copy full SHA for 01c296d

• fix: work around leanprover#2044 in derive handler

  Vtec234

  committed
  35894a9

  Copy full SHA for 35894a9

• chore: typo

  Vtec234

  committed
  a19c02d

  Copy full SHA for a19c02d

• feat: support RPC references in widget props

  Vtec234

  committed
  34bea79

  Copy full SHA for 34bea79

• feat: support global widget registration

  Vtec234

  committed
  15a79fb

  Copy full SHA for 15a79fb

• feat: show widgets at per-line granularity

  Vtec234

  committed
  29c72b2

  Copy full SHA for 29c72b2

• fix: user widgets test

  Vtec234

  committed
  7fc51e5

  Copy full SHA for 7fc51e5

• fix: RpcEncodable test

  Vtec234

  committed
  cb3a315

  Copy full SHA for cb3a315

• doc: clarify RpcEncodable

  Vtec234

  committed
  3c54f54

  Copy full SHA for 3c54f54

• chore: undo renaming

  Vtec234

  committed
  7f3c397

  Copy full SHA for 7f3c397

• chore: drop name field

  Vtec234

  committed
  7d50cf0

  Copy full SHA for 7d50cf0

• fix: scope more instance names

  Vtec234

  committed
  5712e91

  Copy full SHA for 5712e91

• doc: more on widget modules

  Vtec234

  committed
  6add66e

  Copy full SHA for 6add66e

• chore: publicize some functions

  Vtec234

  committed
  04fdfec

  Copy full SHA for 04fdfec

• chore: restore flake.nix

  Vtec234

  committed
  3189fb7

  Copy full SHA for 3189fb7

• feat: more backwards compat

  Vtec234

  committed
  95d7286

  Copy full SHA for 95d7286

• fix: stray instance

  Vtec234

  committed
  43628c9

  Copy full SHA for 43628c9