'ML_file' evaluates ML text from a file directly within the theory, without predeclaration via 'uses';

add keywords of this node as well (e.g. relevant for Pure.thy);

tuned;

tuned message -- dynamic loading happens routinely, e.g. in TTY/PG interaction;

discontinued separate list of required files -- maintain only provided files as they occur at runtime; tuned signature;

find files via load commands within theory text; clarified Thy_Load.with_thy_text, simplified Thy_Load.check_thy;

clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;

pass syntax through check_thy;

use Thy_Header.read on explicit text only -- potentially via File.read, not Scan.byte_reader; tuned signatures;

clarified Parse.path vs. Parse.explode -- prefer errors in proper transaction context;