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