tuned;
uniform treatment of old-style and new-style comments;
eliminated clones;
trim blanks -- more thoroughly than in update_cartouches (for single-line comments);
more specific tool "isabelle update_comments", for uniformity with formal comments in embedded languages;