Hi all,
First I want to thank Makarius and the people involved at TUM for
brushing up Isabelle/VSCode! Secondly, I want to report an - I suppose
parsing - issue when bootstraping Pure. Steps to reproduce in
Isabelle/a36a1cc0144c:
1. Start Isabelle/VSCode by using `isabelle vscode -l HOL`
2. Create and open a theory `Scratch.thy` with content
```
theory Scratch
imports Main
begin
ML‹
val _ = METHOD
›
end
```
3. Open `method.ML` (e.g. ctrl+click on `METHOD` in `Scratch.thy`)
4. Open `Pure/ROOT.ML` and wait for the bootstrap process
5. An error appears in the Isabelle output panel:
```
SML lexical error: bad input (line 229 of
"/my/path/to/isabelle/src/Pure/Isar/method.ML")
```
Best wishes,
Kevin
On 25.03.22 13:38, Makarius wrote:
*** Isabelle/VSCode Prover IDE ***
* VSCodium, an open-source distribution of VSCode without MS
telemetry, has been bundled with Isabelle as add-on component. The
command-line tool "isabelle vscode" automatically configures it as
Isabelle/VSCode and starts the application.
* 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.
This refers to Isabelle/73034d385688, which also provides an updated
README.md: VSCodium shows that in the regular extension dialog.
After some weeks of struggling with the underlying technologies, the
required patches to VSCodium turned out rather simple, see
Isabelle/src/Tools/VSCode/patches/.
This is the first time to make it semi-public. There are many small and
big questions that are still open, see details in
https://makarius.sketis.net/repos/isabelle_vscode_development/file/tip/TODO.md
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
