merged

remove Hoare dependency from Fold.thy

added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;

turned 'boogie_open' into thy_load command, without any declarations of 'uses';

tuned signature;

clarified type Token.file;

expand all files uniformly;

added build option -l (list files);

prefer classic take_prefix/take_suffix over chop_while (cf. 0659e84bdc5f);

more basic file dependencies -- no load command here;

tuned signature (again, cf. ff9cd47be39b);

updated Thy_Load.check_thy;

simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;

tuned signature;

simplified Thy_Load.provide: do not store full path;

prefer ML_file over old uses; updated generated files;

merged

abstracted lemmas

prefer ML_file over old uses;

prefer ML_file over old uses;

'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;