isabelle build options -c -x -B refer to imports_graph;

more uniform checks;

tuned signature;

clarified error;

clarified settings -- avoid hard-wired directories;
tuned documentation;

include target sessions as well: avoid default "Draft" qualification;

clarified signature;
simplified options;

more accurate dependencies;
tuned;

more accurate theory_graph: avoid imports of loaded_theories with incomplete node name;

clarified signature: Known.theories retains Document.Node.Entry (with header);

tuned signature;

tuned;

support 'export_files' in session ROOT;

support for build_database_server (PostgreSQL);
clarified signature;

clarified store.clean_output: cleanup user_output_dir even in system_mode;

clarified store directories;
discontinued settings ISABELLE_PATH, ISABELLE_OUTPUT;

tuned;

clarified handling of output heap;

more abstract database access;

clarified heap vs. database operations: discontinued correlation of directory;

tuned signature;

support Store with options;

tuned signature;

clarified signature;

tuned signature;

cleanup session output before starting build job;
tuned signature;

support for XZ.Cache;

clarified signature: prefer selective include_sessions;

tuned signature;

support for "session_start";

allow cancellation of Sessions.deps/base_info via progress.stopped (progress.echo only happens for options like "verbose");

tuned;

treat sessions as entities with defining position;
tuned signature;

formal treatment of documentation names;

formal check of @{cite} bibtex entries -- only in batch-mode session builds;

implicit thy_load context for bibtex files;

avoid clash with special files in HTML output;

tuned signature;

added document antiquotation @{session name};
renamed protocol function "Prover.session_base" to "Prover.init_session_base" according to the ML/Scala operation;

disallow theory name "ROOT";

PIDE markup for session ROOT files;

tuned;

retain files in Pure.thy, notably $POLYML_EXE;

tuned signature;

tuned;

tuned signature;

clarified signature (again);

clarified exclusion: operate on completed selection, as last step;

tuned;

tuned signature;

clarifified selection: always wrt. build_graph structure;
tuned signature;

tuned;

tuned signature;

backed out odd "bug fix" 671decd2e627;

uniform graph restriction: build_graph is more sparse than imports_graph and may yield different results for exclude_session_groups / exclude_sessions (e.g. "isabelle build -a -X main");

clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;

proper deps;

allow unrelated ancestor;
clarified error;

support alternative ancestor session;

support focus_session, for much faster startup of Isabelle/jEdit;
more options for "isabelle jedit";

init only once (see also c0f776b661fa);

clarified terminology;

tuned signature;

do not store bulky Session.Deps;

avoid duplicate invocation of expensive Sessions.deps on full_sessions;
tuned;

clarified ROOT syntax: 'sessions' and 'theories' are optional, but need to be non-empty;

removed unused option, which is potentially expensive;

allow to augment session context via explicit session infos;
more compact required_session interface;

synthesize session with all required theories from other session imports;

clarified signature;

clarified signature;

clarified signature;

clarified signature;

clarified signature: global_theories is always required;

tuned signature;

clarified modules;

more permissive: db could be empty after hard crash;

uniform system name;

provide theory timing information, similar to command timing but always considered relevant;

tuned signature;

clarified signature;

clarified meta_digest;

tuned signature;

tuned signature;

operations for graph display;

tuned signature;

tuned;

clarified signature: public access to ROOT file syntax;

theory qualifier is always session name (see also 31e8a86971a8);

clarified node_syntax (amending ae38b8c0fdd9): default to overall_syntax, e.g. relevant for command spans wrt. bad header;

process ROOT files only once, which allows duplicate (or overlapping) session root directories;

discontinued obsolete 'files' in session ROOT;

more compact (second-order) digest for 10^2..10^3 source files, with slightly increased risk of collisions;

sources_stamp refers to full sources;
simplified data storage (again);

persistent storage of imported_sources;

cache sources: invoke SHA1.digest at most once;
maintain imported_sources, as required for new theories;

tuned;

option -B for "isabelle build" and "isabelle imports";

more standard merge operation;

unused;

more accurate node_syntax: avoid overall_syntax for PIDE edits;

tuned signature;

clarified theory syntax vs. overall session syntax;

unused;

more informative loaded_theories: dependencies and syntax;

tuned signature;

tuned;

tuned signature;

session-qualified theory names are mandatory;

maintain loaded_files for each theory;

clarified pure_files, based on uniform loaded_files;

tuned signature -- more readable output as Scala value;

proper standard_path to revert platform_path in JEdit_Sessions.session_base;

tolerate more errors (cf. 1e5ae735e026);

clarified signature: provide all_known information uniformly (it is subject to Sessions.T selection);

tuned;

clarified errors;

tuned;

clarified platform file operations;

proper bootstrap_name (amending b42743f5b595);

tuned signature;

unused;

store errors in build_history logs and database;

store errors in build db;

clarified use of XML.Cache;

tuned signature;

tuned signature;

clarified signature;

tuned signature;

clarified signature;

tuned signature;

tuned;

tuned signature;

tuned signature;

clarified modules;

meta_digest without accidental source positions (amending 1544e61e5314): avoid spurious rebuild of unrelated sessions after editing ROOT;

support for potential session imports;

support for Mercurial manifest check;

tuned;

proper imports_resources for import_name: avoid self-referential name resolution;

eliminated default_qualifier: just a constant;

proper theory_qualifier;

more operations;

tuned signature;

clarified;

store Sessions.Info.name;

more position information;

clarified session graph: collapse theories from other sessions;

clarified: Map index uses canonical files;

tuned signature;

tuned signature;

proper imports_base, notably for thy_deps;

tuned signature;

special theories are always global;

proper bootstrap base for building Pure;

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

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

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

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

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;

more qualifier treatment, but in the end it is still ignored;

more session_base information in ML;
tuned signature;

tuned;

tuned comment;

more explicit lookup of loaded_theories: base names allowed here;
no base names for known_theories;

support for all_known_theories of all sessions;

tuned;

known_theories from imported sessions;

tuned;

more checks;

tuned signature;

support for static session imports, without affect build hierarchy;

explicit Sessions.Selection;

clarified signature: tree structure is not essential;

tuned whitespace;

clarified fall-back name;

tuned signature;

clarified modules;

uniform import_name, with treatment of global and qualified theories;

tuned signature;

tuned signature;

tuned syntax;
some official documentation;

clarified: allow to qualify theories from ROOT;

refer to global_theories from all sessions, before selection;

tuned signature;

tuned;

provide session qualifier via resources;

tuned signature;

proper primary key;

tuned;

tuned;

access table via session_name: db may in principle contain multiple entries;

eliminated somewhat redundant inlined name (despite a7aa17a1f721);

tuned;

proper columns;

tuned signature;

more general signature: not limited to SQLite;

maintain persistent session info in SQLite database instead of log file;

tuned;

tuned message;

clarified signature;

more selective queries;

clarified data representation;

data representation with XML.Cache;
tuned;

clarified name;

SQL database operations for combined session info;

tuned signature;

unused;

clarified fall-back base, e.g. relevant for "isabelle jedit -l BAD";

clarified modules;

clarified modules;
tuned;

tuned whitespace;

clarified keywords;

more IDE support for Isabelle/Pure bootstrap;

clarified modules;

--HG--
rename : src/Tools/jEdit/src/isabelle_logic.scala => src/Tools/jEdit/src/jedit_sessions.scala

eliminated "xname" and variants;

clarified syntax;

tuned;

more standard session build process, including browser_info;
clarified final setup of global ML environment;

more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
avoid slowdown of Resources.loaded_files due to command name 'use' in Pure base syntax;

clarified ML bootstrap;

--HG--
rename : src/Pure/ML/ml_pervasive_initial.ML => src/Pure/ML/ml_pervasive0.ML
rename : src/Pure/ML/ml_pervasive_final.ML => src/Pure/ML/ml_pervasive1.ML

tuned;

tuned message;

proper SHA1 digest as annex to heap file: Poly/ML reads precise segment length;

support for Poly/ML heap hierarchy, which saves a lot of disk space;

clarified signature;

tuned signature;

find heaps uniformly via Sessions.Store;
tuned;

clarified modules;

clarified modules;