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

[Makarius]

On 30/06/2025 20:54, Makarius wrote:
> *** General ***
> 
> * A Prover IDE session, e.g. in Isabelle/jEdit or Isabelle/VSCode, is
> now able to load markup and messages from the underlying session
> database. Example: "isabelle jedit -l HOL src/HOL/Nat.thy" for theory
> "HOL.Nat" in session "HOL". This information is read-only: editing
> theory sources in the editor will invalidate formal markup, and replace
> it by an error message.

I have reworked this significantly in Isabelle/b66202c4e6d9, which also 
contains the slightly updated NEWS entry.

Most notably, there is now proper support for output messages, even within 
auxiliary files (e.g. 'ML_file'). This turned out surprisingly difficult, 
because the concept of "results" of a command are half-way between the 
obsolete REPL world and the PIDE document model. I made a lot of efforts to 
re-implement the interactive status-quo in the batch-build model of reloaded 
theories.


	Makarius