merged

avoid exhaustion of worker threads, notably due to complex interaction of future/promise/lazy in Proofterm.make_thm_node;

more robust: insist in finished future;

unused;

further refinement of code equations for mask operation

uniform mask operation

clearer separation of pre-word bit list material

added lemma

more consequent transferability

more robust scheduler shutdown, notably for spurious crashes;

unclear why I ever asked for type tree2

enforce pide_session to see if all isabelle_cronjob tasks work smoothly with it;

proper pretty printing for latex output, notably for pide_session=true (default);

clarified name to avoid duplication (no distinction of data on host = lrzcloud2);

clarified names;

more errors;

follow Phabricator update 2020 Week 27;

tuned;

unused;

clarified errors: avoid hiding of import_errors/dir_errors by their consequences (file-access problems);

clarified errors: avoid accidental import from other session that happens to be within overall selection (notably "isabelle build -a");

clarified signature;

clarified order --- proper sorting of requirements;

obsolete (see 9cde8c4ea5a5);

tuned --- based on hints by IntelliJ;

tuned signature;

updated to polyml-5.8.1 (official release);

subtle change of Theory_Data extend/merge semantics due to Theory.join_theory; explicitly check for extend as identity;

clarified -- avoid non-standard extend/merge;

tuned -- avoid non-standard extend;