tuned;

observer proper session hierarchy (according to build_graph): thus exported artifacts are always valid;

tuned;

clarified order: prefer bottom-up construction of partial content;

more thorough update_global_index: overwrite old content;

tuned;

tuned;

clarified HTML_Context: just one context type;

unused (see also 217e6cf61453, 5e7916535860);

merged

clarified Theory_Cache: prefer immutable data with Synchronized variable; clarified Export_Theory.Theory vs. Entity tables; entity_ref: proper treatment of entity kind;

tuned signature;

unused;

proper support of verit's return code for timeout

tuned whitespace;

updated to verit-2021.06.1-rmx, to address "Abnormal termination with exit code 14";

clarified signature;

prefer official Export.explode_name; avoid string interpolation: Isabelle/Scala is closer to Isabelle/ML than Python/Perl;

tuned;

avoid conflict with future keyword;

tuned messages;

clarified signature: more direct XML.symbol_length;

more direct Symbol.length: Symbol.decode is redundant, symbol counts are invariant under it;

tuned -- eliminate clones stemming from d28a51dd9da6;