@[reducible, inline]

abbrev Sparkle.Display.Interactive.RegisterFn : Type

Type alias for the comm-bus registration entry point. Matches xeus-lean's CommBus.register : String → (Lean.Json → IO Lean.Json) → IO Unit.

Equations

• Sparkle.Display.Interactive.RegisterFn = (String → (Lean.Json → IO Lean.Json) → IO Unit)

opaque Sparkle.Display.Interactive.commBusBinding : IO.Ref (Option RegisterFn)

The currently-installed comm-bus backend, or none if nobody has wired one up yet. In the tutorial Docker image this is set at startup to CommBus.register; in a plain lake build of Sparkle it stays none and render falls back to emitting the HTML without a kernel-side handler.

def Sparkle.Display.Interactive.bindCommBus (impl : RegisterFn) : IO Unit

Install a comm-bus backend. Call this once at startup (e.g. via a top-level initialize in your project's Notebooks.lean) to wire up xeus-lean's CommBus.register.

Calling it twice replaces the previous binding.

Equations

• Sparkle.Display.Interactive.bindCommBus impl = ST.Ref.set Sparkle.Display.Interactive.commBusBinding (some impl)

structure Sparkle.Display.Interactive.Widget (S : Type) : Type

A generic interactive widget.

The S type parameter is the per-session mutable state. The handler closes over a snapshot of that state on every incoming message; if the handler needs to mutate the state it should do so via the IO.Ref directly (the snapshot argument is for read-only convenience).

• sessionId : String

  Session id the JS frontend will echo in comm_open.

• state : IO.Ref S

  Per-session mutable state.

• handler : S → Lean.Json → IO Lean.Json

  Message handler. s is a snapshot of state at receipt; use state.modify / state.set to mutate persistently.

• htmlOf : String → String

  Cell HTML / JS that sets up the JS side of the widget. Receives the session id; expected to embed it in a comm_open data.session field so the bound comm-bus routes the messages back to this widget's handler.

def Sparkle.Display.Interactive.render {S : Type} (w : Widget S) : IO Unit

Register w's handler with the bound comm-bus and emit its HTML into the current cell.

This is a side-effecting IO action — call it from a def main : IO Unit or, more typically, from #eval. The return is immediate; the handler runs whenever a comm_msg arrives, until the JS side closes the comm.

If no comm-bus backend has been bound (see bindCommBus), only the HTML is emitted — the JS side will render but the kernel won't respond to its messages. That's the expected fallback for offline lake builds; it lets test suites typecheck render calls without dragging in xeus-lean.

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.Display.Interactive.uniqueSessionId (tag : String) : IO String

Generate a fresh, probably-unique session id of the form <tag>-<random hex digits>. Convenient for one-shot widgets where you don't care about the id surviving across re-renders.

Equations

• One or more equations did not get rendered due to their size.