feat: preserve and render widget messages in HTML output

[alok]

Summary

Addresses #311 — preserves Lean user widget messages (MessageData.ofWidget) through the SubVerso → Verso pipeline instead of discarding them.

Before: (onWidget := fun _wi alt => convert alt) — widget instances thrown away, only alt text kept.
After: Widget javascriptHash + serialized props JSON flow through MessageContents.widget and are emitted as data attributes in HTML output.

Changes

SubVerso (alok/subverso@feature/widget-messages-rc6)

• Add | widget (javascriptHash : Nat) (props : String) (alt : MessageContents expr) constructor to Highlighted.MessageContents
• Change onWidget handler in Code.lean to evaluate widget props with an empty RpcObjectStore and store them (serializable widgets produce valid JSON; RPC-dependent widgets degrade to alt text)
• Update Export types, Quote instance, toString, startAt, stopAt pattern matches

Verso (this PR)

• Highlighted.lean (MessageContents.toHtml): Render .widget as <span class="widget-message" data-widget-hash="..." data-widget-props="..."> with alt text as visible content
• HighlightedToTex.lean: Render .widget as its alt text (widgets are interactive-only)
• External.lean: Add .widget case to findTrace?

How it works

When Lean code in a Verso document emits a widget message (e.g., a LeanPlot chart or ProofWidgets visualization):

1. SubVerso captures the WidgetInstance during highlighting, evaluates its props to JSON, and stores (hash, props, alt) in MessageContents.widget
2. Verso HTML renders the alt text as visible content, with the widget hash and props embedded as data-* attributes
3. Future JS can discover [data-widget-hash] elements, fetch the widget module source by hash, and hydrate them with React

Remaining work for full interactive rendering

Per the discussion in #311, complete widget rendering requires:

• Bundle React + @leanprover/infoview in generated HTML pages
• Implement infoview "shim mode" where server-dependent functions fail gracefully
• JS bootstrap to discover [data-widget-hash] elements, dynamically import widget modules by hash, and render React components with the serialized props
• Mechanism to retrieve widget module JS source (either bundled at build time or fetched from a known location)
• Opt-in mechanism for widgets to declare they are useful in non-interactive contexts (per David's suggestion)

Test plan

• lake build passes for SubVerso (56/56 jobs)
• lake build passes for Verso (470/470 jobs)
• Verify widget data flows through by creating a Verso doc with a widget-producing #eval and inspecting the HTML output for data-widget-hash attributes

🤖 Generated with Claude Code