uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style; discontinued obsolete 'txt_raw' (superseded by 'text_raw'); eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds); 'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind; changed tagging of diagnostic commands within proof;

tuning

merged

do not introduce consts too early unnecessarily

added lemma

merged

prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;

make SML/NJ happy;