Do not do manual html escaping of react components

[eric-wieser]

This attempts to fix #308. Rather than trying to assemble a string with correct HTML escaping and then have it be parsed to DOM nodes, we construct the dom node directly.

The previous parsing was broken, because in essence vscode tries to run JSON.parse (htmlParse (jSON.stringify (htmlEscape x))), and the encoders and decoders do not commute.

The goal parser still uses the escape-mangle-parser approach, but that's slightly more work to rewrite in a principled way. At any rate, it's not broken in the same way as no json-encoding is involved there.

This also removes some weird filename escaping that would result in filenames containing <> showing up with <> in the goal view.

[robertylewis]

Sorry for the dumb question, how do I build and install a version of the extension from a branch? Is it complicated? I see development directions in the readme, but not how to try out a new version.

[eric-wieser]

My workflow is:

• Open the repo in gitpod
• Wait for it to build
• Click the "debug" button, which opens a new instance of vscode pointing at the same filesystem in a new tab
• Let the extension offer to install elan
• Test out the new extension version there

[robertylewis]

I'm stuck on

Let the extension offer to install elan

When I click "debug", I get an error related to ms-vscode.cpptools # not available from openvsx, but works via "open in vscode". If I ignore the error, or comment it out, I get the new instance of VSCode in a new tab. But there's no Lean extension installed and the one I see in the marketplace is the official one. Am I mising a step?

[eric-wieser]

Ignoring the error is the right thing to do. I think you just have to wait a bit longer for the javascript to build before asking to debug; I don't think the debug button is linked to the compilation, which is happening in one of the many terminal sessions at the bottom.

Edit: The lean extension will be installed automatically if its working correctly.

[robertylewis]

npm run compile definitely finished (and populated out/) before I clicked debug. Is there a specific file I can look for to see that it build correctly? Are the cmake extension popups related?

[eric-wieser]

No, you can ignore the cmake popups too, they're for if you want to rebuild lean itself (and impossible to disable...)

[eric-wieser]

Here's the sequence of clicks I make:

(right button, then hit enter in the shell)

[eric-wieser]

@gebner or @EdAyers, would you mind taking a look at this?