Summary
- merged
- active jEdit actions;
- more symbols;
- clarified syntax;
- updated;
- some icons from Symbola font;
- more latex symbols, notably for embedded ML;
- uniform ML and document antiquotations;
- proper completion of path cartouche (amending 5a7c919a4ada);
- clarified error;
- more uniform path syntax (like url);
- liberal name as in document antiquotations;
- tuned;
- clarified antiquotations;
- tuned error;
- tuned whitespace;
- suppress ASCII art;