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;