tuned signature;

proper command id for inlined errors, which is important for Command.State.accumulate;

clarified span position;

tuned;

tuned;

hybrid use of command blobs: inlined errors and auxiliary files; static check of theory imports;

more command categories, as in ML; tuned;

more command categories, as in ML;

tuned;

value-oriented user error, for well-defined Thy_Syntax.chop_common;

more explicit exception User_Error, with value-oriented equality;

tuned signature;

clarified positions of theory imports;

misc tuning -- more uniform ML vs. Scala;

tunes signature -- more uniform ML vs. Scala;

position parser as in ML;

tuned signature; minimal I/O on GUI thread should be OK;

rhs of eqn is only eta- but not beta-eta-contracted; hence the latter is performed explicitly if needed

simplified Command.resolve_files in ML, using blobs_index from Scala; clarified modules;

removed junk;

tuned;

merged

clarified markup for embedded files, early before execution;

clarified command content;