added Session_Dockable.session_phase label;

separate Plugin.init_model; slightly more robust initialization of Document_View/Document_Model, depending of Session.phase;

simplified Session.Phase; slightly more robust session startup; misc tuning;

tuned messages -- cf. Admin/MacOS/App1;

tuned dialog;

explicit Session.Phase indication with associated event bus; asynchronous Session.start(); synchronous Session.stop(); added Plugin.session_manager on top of basic Session; eliminated separate isabelle.activate action; misc tuning;

tuned signature;

Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it;

tuned;

manage persistent syslog via Session, not Isabelle_Process; tuned;

tuned prover message categorization;

tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;

tuned message;

Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;

Snapshot.convert/revert: explicit error report to isolate sporadic crash;

make compiler doubly sure;

isabelle-process: less verbose no-commit mode;

tuned message;

tuned panel names and actions;

renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;

reactivated polyml-5.4.0 -- SVN 1214 fixes a problem with arbitrary precision arithmetic that was triggered by method "approximation" in HOL/Decision_Procs/Approximation_Ex.thy;

merged

more lists lemmas

merged

merged

tuned text

sections on @{code} and code_reflect

formal syntax diagram for code_reflect

distinguish SML and Eval explicitly

no_frees_* is subsumed by new framework mechanisms in Code_Preproc