parellel scheduling of node edits and execution;

tuned error message;

retrieve imports from document state, with fall-back on theory loader for preloaded theories;
misc tuning;

explicit check of finished evaluation;

refined Document.edit: less stateful update via Graph.schedule;
clarified node result -- more direct get_theory;
clarified Document.joint_commands;

simplified exec: eliminated unused status flag;

consistently use variable name 'F' for filters

generalize lemmas about LIM and LIMSEQ to tendsto

HOL-Nominal-Examples: respect distinction between sets and functions

less verbosity in batch mode -- spam reduction and notable performance improvement;
clarified Proof_Display.print_consts;