HtmlIo.lean

import ProofWidgets.Data.Html
import ProofWidgets.Component.HtmlDisplay

namespace ProofWidgets

syntax (name := htmlIoCmd) "#html_io " term : command

open Lean Elab Server

unsafe def evalHtmlIoUnsafe (stx : Term) : TermElabM (IO Html) := do
  let htmlT := .app (mkConst ``IO) (mkConst ``Html)
  Term.evalTerm (IO Html) htmlT stx

@[implemented_by evalHtmlIoUnsafe]
opaque evalHtmlIo : Term → TermElabM (IO Html)

open Command Json in
@[command_elab htmlIoCmd]
def elabHtmlIoCmd : CommandElab := fun
  | stx@`(#html_io $t:term) =>
    runTermElabM fun _ => do
      let htX ← evalHtmlIo t
      let ht ← htX
      savePanelWidgetInfo stx ``HtmlDisplayPanel do
        return json% { html: $(← rpcEncode ht) }
  | stx => throwError "Unexpected syntax {stx}."

end ProofWidgets

open ProofWidgets
open scoped ProofWidgets.Jsx

#html_io do
  return Html.ofTHtml <b>Test <i>italic</i></b>