NEWS: PIDE is able to load theory markup from underlying database

[Makarius]

On 31/07/2025 11:34, Kevin Kappelmann wrote:
> 
> I experience a regression in Isabelle/VSCode: when opening large pre-built 
> theories (particularly, HOL.List and HOL.Transcendental) Isabelle/VSCode 
> prints the messages of the respective theory but then stops responding.

There is definitely something wrong here, even in current 
Isabelle/adaea1a92086 with its significant refinements of "reload_theory" 
concept of PIDE. I did manage to see output messages in theory HOL.List a few 
times before it disintegrates.

I've spent only 30min to look around in the Isabelle/VSCode sources, and did 
not find anything specific on the spot. I did see many fine points that need 
to be brushed up --- results from the last two Bachelor projects on 
Isabelle/VSCode that are not yet fully integrated.

This will happen soon, and be finished before the coming release at the end of 
this year, because someone else has provided a small budget for precisely such 
"brush up and proper integration" work in Isabelle/VSCode. (A much bigger 
budget will be required to turn the still *experimental* Isabelle/VSCode into 
proper production quality, at the level of Isabelle/jEdit.)


	Makarius