clarified loaded_theories: map to qualified theory name; proper theory_name for PIDE editors;

global session_base for PIDE interaction;

more explicit jEdit file operations; less redundant JEdit_Resources.node_name();

early check and normalization of session directory, e.g. relevant for path information passed to ML process, which may have a different CWD;

tuned;

tuned

more fundamental euler's totient function on nat rather than int; avoid generic name phi; separate theory for euler's totient function

merged

more informative known_files: known_theories within the local session directory come first; more thorough Session.Base.platform_path;

less global theories -- conflict with AFP entries;

support for known theories files (according to multiple uses);

proper display_name;

clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);

tuned signature;

proper import qualifier for global theories; clarified uniqueness;

explicit theory qualifier for session "HOL-Proofs": its theory name space overlaps with session "HOL", even for further imports;

proper qualifier for imports;

clarified, according to Scala version;

tuned text;

clarified signature;

NEWS;

more robust: user could provide name with "/" etc.;

clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;

added system option record_proofs, which allows to build HOL-Proofs without special Proofs.thy;