From: Makarius <makarius@sketis.net>
* Isabelle/VSCode Prover IDE *
The main toolbar provides access to Isabelle examples and
documentation. Plain text files are opened in the editor, but PDFs
require a suitable VSCode extension (e.g. "vscode-pdf" from the
marketplace).
Output panels for Isabelle Symbols and Sledgehammer, which imitate
Isabelle/jEdit dockables to some extent.
This refers to Isabelle/b42e2dd962a8, but the starting point was 486e094b676c:
approx. 12 days and 150 changesets earlier.
This integrates the Bachelor project by Diana Korchmar, LMU München. The
project was intended as an experiment to see if/how Isabelle/VSCode could
eventually catch up with Isabelle/jEdit. My conclusion: we need a quite
different approach; imitating existing Scala/Swing GUIs with untyped/unscoped
HTML/JS/CSS is not going to work --- it leads to unmaintainable self-forks.
There are also fundamental limitations of the underlying VSCode: Electron =
Node.js + Chromium. That might all be considered "popular" and "modern", but
it actually feels very archaic to me (funny scripting languages and
cooperative multitasking from the early 1980s).
Makarius
Last updated: Nov 05 2025 at 08:30 UTC