pretty printing latex string in infoview

Stream: general

[Frederick Pu]

is there any way to render a string as latex in the infoview using some sort of widget or something"?

[Adam Topaz]

I have a PR #19378 that has been neglected for a while (sorry).

[Julian Berman]

There's also https://www.youtube.com/watch?v=tp_h3vzkObo from Kyle and Patrick right?

[Adam Topaz]

If you want something like this for your own project, here is a snippet that should work for you:

import ProofWidgets
import Lean

open Lean ProofWidgets ProofWidgets.Jsx

open Elab Command in
elab "#explain" t:term : command => liftTermElabM do
  let tt ← Term.elabTerm t <| some (.const `String [])
  let src ← unsafe Meta.evalExpr String (.const `String []) tt
  let html : Html := <MarkdownDisplay contents = {src} />
  Widget.savePanelWidgetInfo
    (hash HtmlDisplayPanel.javascript)
    (return json% { html: $(← Server.RpcEncodable.rpcEncode html) })
    t

#explain "foo bar"

[Adam Topaz]

Kyle and Patrick's tool is an "informalization" tool that generates web pages, IIRC.