Summary
- eliminated clones;
- trim blanks -- more thoroughly than in update_cartouches (for single-line comments);
- more operations (as in ML);
- more specific tool "isabelle update_comments", for uniformity with formal comments in embedded languages;
- clarified Token.is_text (cf. Parse.text in ML);
- more operations;
- support for completion;
- allow LaTeX source as formal comment;
- clarified signature;
- clarified SML (no formal comments) vs. Isabelle/ML (arbitrary comments);
- clarified signature;
- clarified modules: uniform notion of formal comments;