src/Tools/jEdit/src/jedit_editor.scala
Fri, 11 Oct 2013 20:45:21 +0200 wenzelm clarified Editor.current_command: allow outdated snapshot;
Tue, 24 Sep 2013 17:13:12 +0200 wenzelm more tolerant treatment of end-of-buffer -- avoid debatable situations of jEdit buffer boundaries;
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:56:12 +0200 wenzelm tuned signature;
Mon, 12 Aug 2013 11:39:29 +0200 wenzelm tuned signature -- more abstract PIDE editor operations;
less more (0) tip