store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing; integrity check of SHA1 digests produced in Scala vs. ML; tuned signature;

more symbols;

more symbol abbrevs to support HOL library maintenance;

reparse only for actually changed blobs; tuned signature;

proper document blobs for initial edit, which is relevant for loading auxiliary file buffers;

more formal Document.Blobs; removed junk;

tuned output;

proper update of text perspective for nodes with changed blobs, which is important to refresh the corresponding command perspective (otherwise it might refer to invalid thy_load commands and cause full execution of the node by the prover);

tuned iterator;

tuned;

tuned comment;

tuned output;