Contents

HTML widgets

Companion package

HTML widgets

\webwidget reserves a place in the text for the page’s own HTML, such as a status badge or a small control. The widget reports its size and where it may be split, much like the hyphenation points of a word. The line breaker then decides, together with the rest of the paragraph, whether and where to split it; in a narrow column it may run over several lines. The widget draws each part and marks the cut ends. In print it takes no space unless it has a default: \webwidget[default=text]{kind}. Other key=value parameters go to the page, which reads them from the widget’s instance. Drag the edge of the result to see the badge split.

The sum of the firstodd numbers is. The badge shows whether the Lean proof assistant has checked this. When its status changes, the paragraph is broken again around it.

The sum of the first $n$ odd numbers is $n^2$ \webwidget[decl=Nat.sum_odd_eq_sq]{lean}.
The badge shows whether the Lean proof assistant has checked this. When
its status changes, the paragraph is broken again around it.

The page registers the widget. In outline (the page’s source has the full menu):

reflowtex.host.define('lean', {    // \webwidget[decl=…]{lean}: instance.attrs.decl
  measure(instance, env) {  // the badge as segments, with a break point between each two
    const { segs, gaps } = segment(label());       // at spaces, and after . and _
    return {
      segments: segs.map(t => env.measure(text(t))),
      gaps: gaps.map(g => ({ width: g.space ? space : 0, penalty: g.space ? 100 : 300 })),
      ends: { left:  { cap: pad, cut: cutPad, overhang: 3.75 },    // closed and cut ends
              right: { cap: pad + chevron, cut: cutPad, overhang: 3.75 } },
    };
  },
  render(instance, host) {  // host.piece: { from, to, left: 'cap' | 'cut', right: 'cap' | 'cut' }
    const { from, to, left, right } = host.piece;
    host.el.innerHTML = badge(textOf(from, to), left, right);
    host.el.querySelector('button')?.addEventListener('click', e => openMenu(e.currentTarget, host.env));
  },
});
// The menu's "Show the declaration" changes the label, then env.invalidate():
// the badge is measured again and the paragraph broken again around it.