more explicit indication of missing files;

more uniform handling of inlined files;

tuned signature;

clarified Document.Blobs environment vs. actual edits of auxiliary files; more robust handling of vacuous edits;

release file errors at runtime: Command.eval instead of Command.read;

maintain blobs within document state: digest + text in ML, digest-only in Scala; resolve files for command span, based on defined blobs; tuned;

always reparse nodes with thy_load commands, to update inlined files;

proper Thy_Load.append of auxiliary file names; inlined errors;

proper theory name vs. node name;

clarified boundary cases of Document.Node.Name;

clarified Thy_Load.node_name;

inline blobs into command, via SHA1 digest; broadcast all blobs within edit, without storing the result;

persistent value;

caching of blob; precise file content according to jEdit IO;

tuned;

maintain document model for all files, with document view for theory only, and special blob for non-theory files;

tuned

whitespace tuning

tuning

more refactoring to accommodate SMT proofs

tuning

tuning

more correct NEWS

simplified old code

refactoring

refactoring

merged

BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate

add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt

refactored