On 25/03/2022 13:38, Makarius wrote:
*** Isabelle/VSCode Prover IDE ***
* Command-line tools "isabelle electron" and "isabelle node" provide
access to the underlying technologies of VSCodium, for use in other
applications. This essentially provides a freely programmable Chromium
browser engine that works uniformly on all platforms.
Here are some further hints on Electron and Node.js.
* "isabelle node" opens a REPL to the JavaScript/Node platform. Here are
some examples for its prompt:
$ isabelle node
Welcome to Node.js v14.16.0.
Type ".help" for more information.
> var a = 1
undefined
> var b = 2
undefined
> a + b
3
* "isabelle electron" opens a "splash screen" application about Electron by
default. It is more interesting to open a different application. I have
prepared a tiny example here:
$ hg clone https://makarius.sketis.net/repos/test-electron
$ isabelle electron --app=test-electron
Thus we get a high-end Chromium browser window with minimal effort. It works
uniformly on all platforms. Full HTML5 and PDF are supported without further
ado. But this is not a proper web browser, e.g. there is no navigation bar.
Potential applications of Electron for Isabelle:
* A portable PDF viewer via pdfjs, with our own add-ons to manage
Isabelle-specific URLs. Thus the PDF can point back to a running Prover IDE,
for example. (This already works with our PIDE HTTP server setup and the
bundle pdfjs component).
* Other JavaScript-based viewers or editors, e.g. for certain diagrams.
This will require more work to connect to Isabelle/PIDE, though.
* For Isabelle/jEdit, it will run in a separate window. For Isabelle/VSCode
it can be incorporated directly into the WebviewPanel of the editor (e.g. see
the Markdown preview).
Summary: We have a whole new world of technology based on Chromium/HTML/CSS/JS
bundled with Isabelle. The file-system footprint is about 1.2 GB for all
platforms together, and 300MB for just one platform (for end-user Isabelle
application bundles).
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
