[isabelle-dev] Isabelle/VSCode bootstrap issue: "SML lexical error: bad input..."

[Makarius]

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