def Sparkle.Display.Mime.mkMarker (mime content : String) : String

Build the wire-format payload as a string. Pure: no IO.

Equations

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

def Sparkle.Display.Mime.emit (mime content : String) : IO Unit

Emit a MIME-tagged payload to stdout. Use from def main : IO or from #eval cells. Inside an elab block prefer the logEmit family below, which routes through Lean's message log so xeus-lean's WASM kernel can pick it up (the WASM build does not capture stdout).

Equations

• Sparkle.Display.Mime.emit mime content = IO.println (Sparkle.Display.Mime.mkMarker mime content)

def Sparkle.Display.Mime.html (content : String) : IO Unit

Convenience: emit a text/html payload.

Equations

• Sparkle.Display.Mime.html content = Sparkle.Display.Mime.emit "text/html" content

def Sparkle.Display.Mime.svg (content : String) : IO Unit

Convenience: emit an image/svg+xml payload.

Equations

• Sparkle.Display.Mime.svg content = Sparkle.Display.Mime.emit "image/svg+xml" content

def Sparkle.Display.Mime.markdown (content : String) : IO Unit

Convenience: emit a text/markdown payload.

Equations

• Sparkle.Display.Mime.markdown content = Sparkle.Display.Mime.emit "text/markdown" content

def Sparkle.Display.Mime.latex (content : String) : IO Unit

Convenience: emit a text/latex payload.

Equations

• Sparkle.Display.Mime.latex content = Sparkle.Display.Mime.emit "text/latex" content

def Sparkle.Display.Mime.logEmit {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.MonadOptions m] [Lean.AddMessageContext m] (mime content : String) : m Unit

Emit a MIME-tagged payload via Lean's info-message log. Works from any monad that supports logInfo (CommandElabM, TermElabM, MetaM, …). Required for elab blocks running under the WASM kernel, which doesn't have stdout capture.

Equations

• Sparkle.Display.Mime.logEmit mime content = Lean.logInfo ((Lean.MessageData.ofFormat ∘ Std.format) (Sparkle.Display.Mime.mkMarker mime content))

def Sparkle.Display.Mime.logSvg {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.MonadOptions m] [Lean.AddMessageContext m] (content : String) : m Unit

elab-friendly variant of svg.

Equations

• Sparkle.Display.Mime.logSvg content = Sparkle.Display.Mime.logEmit "image/svg+xml" content

def Sparkle.Display.Mime.logHtml {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.MonadOptions m] [Lean.AddMessageContext m] (content : String) : m Unit

elab-friendly variant of html.

Equations

• Sparkle.Display.Mime.logHtml content = Sparkle.Display.Mime.logEmit "text/html" content

def Sparkle.Display.Mime.logMarkdown {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.MonadOptions m] [Lean.AddMessageContext m] (content : String) : m Unit

elab-friendly variant of markdown.

Equations

• Sparkle.Display.Mime.logMarkdown content = Sparkle.Display.Mime.logEmit "text/markdown" content

def Sparkle.Display.Mime.logLatex {m : Type → Type} [Monad m] [Lean.MonadLog m] [Lean.MonadOptions m] [Lean.AddMessageContext m] (content : String) : m Unit

elab-friendly variant of latex.

Equations

• Sparkle.Display.Mime.logLatex content = Sparkle.Display.Mime.logEmit "text/latex" content