Widgets not displaying on some terms

Stream: lean4

[Eric Wieser]

In the following example, the widget only displays in one place:

import ProofWidgets.Component.HtmlDisplay

open Lean ProofWidgets Jsx

syntax "foo" term : term
elab_rules : term
| `(term| foo%$stx $t) => do
  let ht := <h2>Hello world</h2>
  Widget.savePanelWidgetInfo (hash HtmlDisplayPanel.javascript)
    (return json% { html: $(← Server.RpcEncodable.rpcEncode ht) }) stx
  Elab.Term.elabTerm t none

example : Nat := foo 1 -- widget
example : Nat := foo (by exact 1) -- no widget

Am I passing the wrong syntax to savePanelWidgetInfo, or is this a bug?

[Eric Wieser]

Using Elab.Term.elabTerm (← `(term| id $t)) none seems to fix it, but I'd rather not insert the id term

[Eric Wieser]

Ah, wrapping with return Expr.mdata {} e also works

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

This is quite bizarre, the adjacent term should make no difference to whether the widget is displayed (since you put it on stx, not on t). I made an issue, lean4#3956.