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

[Kevin Kappelmann]

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
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev