more accurate documentation;

discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems'; print timing as tracing, to keep it out of the way in Proof General; no timing of control commands, especially relevant for Proof General;

more accurate documentation of "(structure)" mixfix;

more robust static structure reference, avoid dynamic Proof_Context.intern_skolem in Syntax_Phases.decode_term;

tuned comment;

just one syntax category "mixfix" -- check structure annotation semantically;

tuned message;