clarified syntax boundary cases and errors;

simplified JVM startup, based on stronger assumptions about the Java version provided as Isabelle component;

eliminated obsolete byte_reader -- theory headers + body files are parsed in full;

more direct File.read_bytes -- avoid cumulative copying of StringBuilder;

improved errors of parser combinators;

tuned messages: end-of-input rarely means physical end-of-file from the past;

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