Widgets not displaying on some terms

[Vtec234]

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