Running javascript in the infoview with ProofWidgets

Stream: mathlib4

[Thomas Murrills]

I'm trying to learn how to use ProofWidgets, and I've run into some challenges with running javascript in the infoview in VS code. It seems as though certain setups which work in a webpage don't work in the infoview.

I was wondering if there are any rules of thumb—or, even better, any deeper insights into the source of the limitations—that let you anticipate when javascript will "just work", and when you have to take special care.

For example, I'd expect this button to produce an alert when clicked, but it doesn't:

import ProofWidgets.Component.HtmlDisplay
open scoped ProofWidgets.Jsx in
#html
  <span>
    <button onclick="alert('I\\'m here!')">{.text "Are you there?"}</button>
  </span>

Getting elements by id and setting their properties seems problematic as well; this should append the string " + 1" to the text of the the div with each click, but nothing changes:

import ProofWidgets.Component.HtmlDisplay
open scoped ProofWidgets.Jsx in
#html
  <span>
    <div id="element">{.text "0"}</div>
    <button onClick="
        const e = document.getElementById('element');
        e.innerHTML += ' + 1'">
      {.text "add 1!"}
    </button>
  </span>

Does this have to with using RPC, somehow? (I'm unfamiliar with the internals.) Any help or pointers to relevant docs are appreciated!

Also appreciated are debugger tools: I'd like to right click > inspect the infoview as I would a browser window, but I can't seem to do that. (There must be a way, though...) Thanks! :)

[Wojciech Nawrocki]

For debugging in VSCode, use 'Developer: Open Webview Developer Tools' in the command palette.

[Thomas Murrills]

Ah, perfect, thanks! :)

[Wojciech Nawrocki]

As to what's going wrong, the issue is that you are trying to set onclick to a string whereas it should be a piece of code (which might be represented by that string, but is not equal to that string). In principle we could add special cases to the code that draw JSX trees to detect inline JS like you wrote and turn it into code (see htmlDisplay.tsx in the ProofWidgets repo for how this works, if you like), but that seems a bit hacky. Ideally we could write event handlers in Lean, but in general that requires a Lean to JS compiler.

[Wojciech Nawrocki]

One way to do what you want with the current technology is to specialize a ProofWidgets.Component to the particular event handler that you want:

structure NoProps
deriving Lean.Server.RpcEncodable

@[widget_module]
def AlertButton : ProofWidgets.Component NoProps where
  javascript :=
    "import * as React from 'react'
    const e = React.createElement

    export default function(props) {
      return e('button', {onClick: () => alert('I\\'m here!')}, props.children)
    }"

#html
  <span>
    <AlertButton>{.text "Are you there?"}</AlertButton>
  </span>

The alert still won't show because the infoview is sandboxed, but you can see in the console that the code runs.

[Wojciech Nawrocki]

And

structure NoProps
deriving Lean.Server.RpcEncodable

@[widget_module]
def AddOneButton : ProofWidgets.Component NoProps where
  javascript :=
    "import * as React from 'react'
    const e = React.createElement

    export default function(props) {
      return e('button', {
          onClick: () => {
            const e = document.getElementById('element')
            e.innerHTML += ' + 1'
          }
        },
        props.children)
    }"

#html
  <span>
      <div id="element">{.text "0"}</div>
      <AddOneButton>
        {.text "add 1!"}
      </AddOneButton>
    </span>

[Thomas Murrills]

Ah, okay, thanks so much! That explains a lot!

[Thomas Murrills]

Hmm, so here's an example which behaves unintuitively (to me). Let's say I'm trying to create HTML which has a script in it.

structure NoProps
deriving Lean.Server.RpcEncodable

@[widget_module]
def AddOneOnce : ProofWidgets.Component NoProps where
  javascript :=
    "import * as React from 'react'
    const e = React.createElement

    export default function(props) {
  return e('span', null,
    e('span', {id:\"test\"}, props.children),
    e('script',null, \"const e = document.getElementById(\\\"test\\\"); e.innerHTML += ' + 1'\"))
  }"

open scoped ProofWidgets.Jsx in
#html
  <AddOneOnce>
    {.text "0"}
  </AddOneOnce>

This produces the HTML you'd expect—HTML which, if opened in a browser, adds one once—but doesn't run the script produced when you'd expect it to. Is there something different about the timing in this case?

And is there a better way to factor this through two widgets? (I tried making the code to get the element and append " + 1" a separate widget which I passed to the other as a child, but hit a "cannot read properties of null" error—perhaps I should have expected that anyway, though (I'm still learning React).)

[Wojciech Nawrocki]

I would avoid writing <script> tags altogether. In React you should program everything in terms of event handlers, and rendering code to set things up before the final return.