tuned signature;

tuned signature: support general Build_Job instances;

tuned signature;

clarified signature: prefer static data;

tuned signature;

identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);

tuned signature;

tuned signature;

tuned signature;

tuned;

unused;

tuned signature (again);

tuned;

tuned;

proper deps from build_graph, not imports_graph (amending 0c704aba71e3);

misc tuning: more direct access to ancestors, without build_graph;

tuned signature (again);

clarified signature: reduce explicit access to static Sessions.Structure;

tuned signature;

clarified modules (again);

tuned;

tuned signature;

avoid premature Properties.uncompress: allow blob to be stored in another database;

more robust: synchronized access to database;

clarified signature: do not expose global state to object-oriented variants;

tuned comments and outline;

merged

Imported a theorem about Infinite_Sum. Importing this theory a bit earlier is causing syntactic ambiguities with Infinite_Set_Sum however; no_notation needed

A little bit more tidying up

tweaked Sledgehammer interaction

there won't be an E version 2.7

reverted 0506c3273814 -- the message is still useful

compile

adopt terminology suggested by Larry Paulson

more robust E proof parsing

avoid double 'Warning:' in Sledgehammer messages

tweaked abduction in Sledgehammer

slightly more documentation

renamed new Sledgehammer option

updated documentation

improve ad hoc abduction in Sledgehammer

tuning

don't apply abduction and consistency checking to goals of the form 'False'

implemented ad hoc abduction in Sledgehammer with E

tuned;

clarified scope of "serial" and "numa_index" within database;

clarified signature: allow more general init, e.g. from existing database;

clarified signature: allow to provide session_heaps by different means, e.g. from tmp directory or alternative session structure;

tuned;

simplified somewhat pointless error message (see also 0189fe0f6452);

clafified signature: simplify object-oriented reuse;

revert pointless 375c6b9ce9ea: overall thread context is already uninterruptible (see 54ac957c53ec);

tuned whitespace;

merged

Fixed a presentation error

Importation of basic group theory results, due to Jakob von Raumer from his AFP entry Jordan-Hölder Theorem

tuned whitespace;

tuned;

clarified signature, although "sql" argument is de-facto mandatory;

tuned;

proper SQL (amending 7ab9bac1ca96);

clarified signature: more explicit "synchronized" regions;

more robust interrupt handling, notably for Build_Job.terminate();

clarified signature: works for general Build_Job;

tuned;

clarified modules;

clarified signature;

proper log_lines, without protocol messages (amending cb3f5361fbca);

clarified signature;

tuned messages;

clarified error output vs. process_result stored in build_database (see also 13a0f537e232 and bff56eae3ec5);

clarified system option: guard for testing, until the database layout has stabilized;

merged

Simplified some proofs

clarified db content: avoid redundancy of historic ML_IDENTIFIER;

merged

proper filterNot, not filterNot-not;

option build_hostname allows to change hostname easily;

clarified permissions of build.db, following server.db;

enforce rebuild of Isabelle/ML, after various changes to build database management;

misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;

tuned: fewer warnings in IntelliJ IDEA;

clarified init_database vs. update_database: implicitly assume fresh "instance";

clarified Build_Process.Context: cover all static information;

tuned whitespace in generated SQL;

tuned: prefer typed operations;

clarified signature: more concise operations;

more robust options in "prefs" format: avoid odd control character;

proper settings for hostname: allow to adjust it in user space;

support for build database: still inactive; more detailed Build_Job.Node_Info;

tuned signature;

clarified signature: more robust operations;

tuned;

tuned;

more operations;

clarified signature: more operations;