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