On 20/04/2022 13:45, Kevin Kappelmann wrote:
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")
```
I have addressed this in
https://isabelle.sketis.net/repos/isabelle-release/rev/072e6c0a2373 for
Isabelle2022-RC4 (expected within 1-2 days).
Playing a bit with Isabelle/VSCode, I see many things that do work and a some
that don't. More TODO items are here:
https://makarius.sketis.net/repos/isabelle_vscode_development/file/tip/TODO.md
So Isabelle/VScode is still an early experiment compared to the finished and
polished state of Isabelle/jEdit.
As a funny side-remark, someone who appears to be notable in the Java
community has recently advertized jEdit as "vintage, but still great" and
"similar to Visual Studio Code": https://www.youtube.com/watch?v=VJfdKhXoaWc
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
