src/Pure/PIDE/editor.scala
Mon, 09 Dec 2013 12:16:52 +0100 wenzelm added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
Sun, 17 Nov 2013 16:02:06 +0100 wenzelm centralized management of pending buffer edits;
Tue, 24 Sep 2013 16:35:01 +0200 wenzelm skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
Mon, 12 Aug 2013 17:11:27 +0200 wenzelm manage hyperlinks via PIDE editor interface;
Mon, 12 Aug 2013 14:53:16 +0200 wenzelm prefer PIDE editor operations;
Mon, 12 Aug 2013 14:27:58 +0200 wenzelm central management of Document.Overlays, independent of Document_Model;
Mon, 12 Aug 2013 12:06:48 +0200 wenzelm tuned signature;
Mon, 12 Aug 2013 11:39:29 +0200 wenzelm tuned signature -- more abstract PIDE editor operations;
less more (0) tip