clarified source location;

added system property isabelle.laf, notably for initial system dialog; let L&F take care of font scaling, e.g. GTK+ for Linux where X11 dpi scaling does not really work;

NEWS;

tuned;

clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;

tuned whitespace;

more toplevel pretty printing;

back to full synchronization (cf. eb3e399f5b9f);

proper sequential version;

eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer); clarified Command.run_process etc.: join running eval, bypass running print; eliminated Command.memo in favour of regular Lazy.lazy; more Lazy.lazy status information;

modernized historic example;

more thorough Lazy.is_finished;

3 old example lemmas by Amine listed in the top 100 theorems

update_cartouches; trimmed whitespace;

memo_fork without locking, to avoid rare deadlock in Event_Timer.request due to execution overrun;

typos

unused;

tuned message;

explicit message channels for "state", "information"; separate state_message_color;

imitate font more carefully: err on smaller size; imitate HTML font, notably for Sidekick where short string is also shown as view status message;

more accurate selection of sessions;

more accurate selection of sessions;

discontinued central critical sections: NAMED_CRITICAL / CRITICAL;

more elementary Multithreading.synchronized;

proper Synchronized.var; more atomic operations;

removed remains from Proof General;

obsolete;

system option "pretty_margin" is superseded by "thy_output_margin";

tuned;

proper Synchronized.var;