clarified count_file;

clarified modules;

clarified option type;

count document nodes via raw file length;

clarified Load_State / load_limit;

clarified Load_State;

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

count nodes uniformly: avoid overloaded session;

clarified signature;

clarified options -- more scalable;

prefer atomic edits -- potentially more robust;

clarified signature -- potentially more robust;

more sequential access to Session.manager.global_state: avoid minor divergence of tip version;

clarified share_common_data: after finished checkpoint, before next edits;

support headless_load_limit for more scalable load process;

tuned message;

clarified incremental loading: requirements based on maximal nodes;

tuned signature;

tuned;

tuned message;

more explicit type Load_State;

tuned messages (again) -- avoid confusion wrt. total remaining size;

tuned message;

tuned;

clarified theory status;

tuned messages;

tuned signature;

proper clean_theories wrt. dynamic dep_graph;

tuned signature;

find theory files via session structure: much faster Prover IDE startup;

clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories);

proper finished_theory status for result;

load theories in stages, to reduce ML heap requirements;

clarified signature;

tuned important special case;

tuned signature;

clarified state variable: avoid extra mutability via Promise;

more explicit type Dump.Session, with context information;

clarified signature: prefer operations without position;

prefer Theory_Ordering theory names are unique (due to proper session context);

clarified signature: full dependency graph;

support for share_common_data after define_command and before actual update: this affects string particles of command tokens;

support unicode_symbols in input source;

clarified signature;
suppress already loaded theories;

tuned;

more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;

clarified Node_Status vs. is_suppressed, e.g. relevant for purged nodes in Theories_Dockable after 0626cae56b6f;

proper session base foundations (amending e848328cb2c1);

include loaded_files as doc_blobs (without purging);

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

clarified signature;

clarified defaults via system options;

clarified modules and signature;

more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;

proper status after commit;

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

tuned signature;

clarified modules;

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