tuning

NEWS;

merged

restrict node_required status and Theories panel to actual theories;

ranges of thy_load commands count as visible within perspective; convert ranges wrt. snapshot -- relevant for outdated situation;

tuned;

refer to thy_load command of auxiliary file;

proper static resolution of files via Thy_Load.load_thy, instead of TTY fall-back;

load files that are not provided by PIDE blobs; uniform resolve_files via Command.read;

tuned;

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