Thy_Info.use_thy_legacy removed

[Makarius]

*** ML ***

* Obsolete Thy_Info.use_thy_legacy has been removed. Rare
INCOMPATIBILITY: need to use formal PIDE session to load theories, e.g.
via "isabelle build" or "isabelle process_theories".


This refers to Isabelle/955f8ac18136.

The Isabelle2025-1 release already had this NEWS entry:

* The former command-line tool "isabelle process" has been renamed to
"isabelle ML_process", with new options -C DIR and -r (redirect). The
old option option -T to load individual theories via the Isabelle/ML
"use_thy" function has been removed. It is still possible to use
"Thy_Info.use_thy_legacy" together with "isabelle ML_process -e ...",
but that low-level entry to the theory loader will be removed at a later
stage. The proper way to process individual theories under program
control is via "isabelle process_theories". INCOMPATIBILITY.


So that's finally it: no "use_thy" anymore. It was the central Isabelle/ML 
operation since 1992, and already present in changeset 0 (Sep-1993):
https://isabelle.in.tum.de/repos/isabelle/file/a5a9c433f639/src/Pure/Thy/read.ML

The implementation behind it has changed many times since then, but now we 
have better ways to communicate between Isabelle/Scala and Isabelle/ML, 
without the old toplevel loop.

Rather soon, I will revisit the protocol function "build_theories" and its 
underlying ML function Thy_Info.use_theories, in order to make it more 
scalable and less sequential: meaning that intermediate states are removed 
earlier in the process, and heap space is released.


	Makarius