Widgets not displaying on some terms

Description

In the following snippet, the widget should display on both lines, but it only displays on one of them.

import Lean.Widget.UserWidget
open Lean

@[widget_module]
def HelloWidget : Widget.Module where
  javascript := r#"
    import React from 'react'
    export default function() {
      return React.createElement('h2', {}, 'Hello world')
    }
  "#

syntax "foo" term : term
elab_rules : term
| `(term| foo%$stx $t) => do
  Widget.savePanelWidgetInfo HelloWidget.javascriptHash (return .null) stx
  Elab.Term.elabTerm t none

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

Context

Reported by @eric-wieser on Zulip.

Steps to Reproduce

1. Run the above snippet.

Expected behavior: The widget is displayed when placing the cursor on either line.

Actual behavior: It only shows up on the first one.

Versions

4.7.0

Run the provided Lean 4.7.0 snippet first and compare widget behavior for foo 1 and foo (by exact 1). Start at the Widget.savePanelWidgetInfo call in the foo elaboration rule and determine why the widget is attached to only one term form; done means the widget displays when the cursor is placed on either example.