src/Pure/PIDE/editor.scala
2017-06-17 ago maintain overlays within main state of document models;
2017-06-16 ago more general dispatcher operations;
2017-06-13 ago tuned signature;
2017-06-13 ago clarified modules;
2017-01-10 ago support "purge" operation on document model;
2017-01-10 ago proper template;
2016-12-23 ago tuned;
2016-12-23 ago tuned;
2016-11-24 ago explicit option editor_generated_input_delay, which is more aggressive by default;
2016-11-23 ago delay_first for machine generated editor events: avoid starvation, e.g. when operating on big sessions;
2015-11-21 ago double flush to ensure persistent "state" output is reset;
2015-08-11 ago support hyperlinks with optional focus change;
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;