2014-04-09 ago avoid confusion about pointless cursor movement with external links;
2014-03-03 ago tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
2014-03-03 ago tuned signature;
2013-12-09 ago added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
2013-11-17 ago centralized management of pending buffer edits;
2013-09-24 ago skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
2013-08-12 ago manage hyperlinks via PIDE editor interface;
2013-08-12 ago prefer PIDE editor operations;
2013-08-12 ago central management of Document.Overlays, independent of Document_Model;
2013-08-12 ago tuned signature;
2013-08-12 ago tuned signature -- more abstract PIDE editor operations;