tuned message -- include completion;

support for completion reports produced in Scala (inlined into messages);

more precises positions; more permissive imports;

avoid duplicate header errors, more precise positions; tuned signature;

tuned protocol -- resolve command positions in ML;

clarified modules;

add inequalities (move from AFP/Amortized_Complexity)

merge

inlining threshold

avoid controversial Pirate syntax

more markup, which helps to create missing imports;

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;