statistics from session build output;

more uniform output;

added [simp] lemmas

more robust HTML rendering of hidden control symbols: Vacuous font bypasses minimal font-size restrictions of common browsers, transparent colour imitates hidden visibility while copy-paste still works;

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;