clarified messages: indicate termination explicitly;

avoid accidental update of base session sources (following documentation in "system" manual);

more scalable output of YXML files;

avoid vacuous session Pure -- dump does not read_pure_theory;

clarified vacuous selection vs. Pure;

tuned signature;

cumulative errors for session partitions;

proper guard for process_theory: ensure uniform precedence of results;

load HOL-Proofs first: it introduces some extra "thm" items that are required later on;

more complete coverage of sessions: process_theory operation needs to handle duplicate theories;

proper build_graph to make session selection work as in "isabelle build";

incorporate sessions with record_proofs;

clarified signature;

clarified signature;

clarified signature;

clarified signature;

clarified treatment of base logic image;

simplified options: always split;

proper guard -- avoid bad result;

split into standard partitions, for improved scalability;

clarified defaults;

tuned signature;

clarified signature: static Dump.Context vs. dynamic Dump.Session;

discontinued pointless dump_checkpoint and share_common_data -- superseded by base logic image in Isabelle/MMT;

avoid censorship of options, e.g. relevant for Isabelle/MMT to provide its own value;

consolidate less aggressively: avoid live-lock when PIDE round-trip takes too long (e.g. in complex theory hierarchies);

clarified share_common_data: after finished checkpoint, before next edits;

obsolete (see 030a6baa5cb2 and d14ddb1df52c);

added dump_options: disabled by default;

more ambitious options (again);

more ambitious options (again, after 93aa546ffbac);

eliminated pointless theory graph (reverting parts of a56eab490f4e): it caused problems with loaded vs. non-loaded node names, e.g. for theory Pure (see also 29bb1ebb188f);

disable fragile options for now;

more robust;

disable share_common_data for now (amending 0f8742b5a9e8) -- potentially more robust;

load theories in stages, to reduce ML heap requirements;

clarified signature;

more explicit type Dump.Session, with context information;

more scalable isabelle dump (and derivatives): mark individual theories to share common data in ML;

enable share_common_data for "isabelle dump" and its derivatives (e.g. "isabelle mmt_import"): this has the potential to reduce ML heap size considerably, after initial command definitions;

more scalable -- less ML heap requirements;

tuned whitespace;

support unicode_symbols in input source;

tuned signature;

tuned signature;

clarified signature;
suppress already loaded theories;

tuned signature;

system option "system_heaps" supersedes various command-line options for "system build mode";
clarified "isabelle jedit" options -n, -s, -u;

tuned messages;

tuned signature;

clarified signature, notably cascade of dump_options, deps, resources, session;

unused;

clarified signature;

clarified errors, according to Isabelle/MMT;
tuned signature;

tuned, according to Isabelle/MMT;

clarified options: ensure consolidated Node_Status and thus percentage = 100% for progress;

tuned;

clarified sessions_deps, according to Isabelle/MMT usage;

tuned signature: for other dump-like tools;

unused;

tuned;

clarified defaults via system options;

unbounded tracing for proper termination, e.g. relevant for theory Sequents.Hard_Quantifiers;

proper return code for runtime failure;

clarified errors: no result from forced session.stop, check pending theories;

suppress some theories to allow "isabelle dump -o skip_proofs";

tuned signature;

tuned signature;

tuned signature;

clarified modules;

--HG--
rename : src/Pure/Thy/thy_resources.scala => src/Pure/PIDE/headless.scala

tuned message;

more detailed session dependencies, with conditions for theories;

tuned signature;

implicit use of NUMA policy, absorbing potential errors;

more uniform Progress, with theory() for batch-build and theory_percentage() for PIDE session;

more accurate output;

clarified defaults;
more uniform treatment of "disabled" case;

more accurate output;

support for watchdog_timeout;

tuned signature;

removed junk;

tuned output;

continuously clean frontier of already committed theories: much less resource requirements;

clarified error progress and error_rc;

tuned signature;

tuned signature;

dump aspects asynchronously;

more detailed progress;

more robust default options, notably for node consolidation;

tuned;

clarified quasi_consolidated state: ensure that exports are present for ok nodes;

clarified modules;

proper session dirs;

tuned;

proper error;

proper build_heap;

disable export_document by default (presently unused and for demo/testing purposes): avoid spurious IO exception in highly parallel environment;

tuned signature;

clarified signature: prefer Document.Snapshot;

more args;

documentation for "isabelle dump";

more dump aspects, with options;
tuned signature;

clarified default: all aspects;

store Isabelle symbols in canonical form;
tuned signature;

clarified outermost progress.interrupt_handler;

report theory progress via PIDE node status;

shutdown ML process before output: Theories_Result is timeless/stateless;

more operations;
more output;

more accurate dependencies;
tuned;

more formal dump aspects;
support output dir;

support to dump build database produced by PIDE session;