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

[Kevin Kappelmann]

Hi all,

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.

Steps to re-reproduce: (1) build HOL (2) start Isabelle/VSCode (3) visit 
HOL.List or HOL.Transcendental (4) process stops responding.

Best wishes,

Kevin

```
theory Test
   imports
     HOL.Nat (*go to Nat.thy and back -- no problems*)
     HOL.List (*go to List.thy and back -- no more responses*)
     HOL.Transcendental (*same as for List.thy*)
begin

(*just some text to check whether the process is still responding*)
lemma "True"
   apply contradiction
   sorry

end
```

On 03.07.25 20:52, Makarius wrote:
> On 03/07/2025 16:34, Lawrence Paulson wrote:
>> This is cool and totally great. I hope we don't pay a price in memory 
>> usage?
> 
> There is no change on the Isabelle/ML side.
> 
> On the Isabelle/Scala side, the memory usage should be the same as if 
> the theory had been loaded interactively into the Prover IDE.
> 
> Nonetheless, we need to watch out for irregularities, after many years 
> without that functionality.
> 
> 
>      Makarius
>