tuned message: same error may occur in different contexts;

detect more errors;

tuned messages;

more general error suffixes, e.g. for messages that are broken over several lines;

another Latex error seen in the wild:
Undefined control sequence.
\isamarkupcancel #1->\xout

more error information according to @<Print type of token list@> in pdfweb.tex;

positions as postlude: avoid intrusion of odd %-forms into main tex source;

clarified file pattern;

simplified positions -- line is also human-readable in generated .tex file;

more robust range on preceding comment-line;
no range for blank lines;
avoid recursive output_text/mark_range;
clarified Latex.output_token (no range) vs. Thy_Output.present_token (with range);

proper file;

clarified file positions;

re-implemented "isabelle document" in Isabelle/Scala, include latex_errors here;

more robust Windows support;

more explicit latex errors;

some support for LaTeX;