| Mon, 12 Aug 2013 17:11:27 +0200 | wenzelm | manage hyperlinks via PIDE editor interface; | file | diff | annotate |
| Mon, 12 Aug 2013 14:53:16 +0200 | wenzelm | prefer PIDE editor operations; | file | diff | annotate |
| Mon, 12 Aug 2013 14:27:58 +0200 | wenzelm | central management of Document.Overlays, independent of Document_Model; | file | diff | annotate |
| Mon, 12 Aug 2013 12:06:48 +0200 | wenzelm | tuned signature; | file | diff | annotate |
| Mon, 12 Aug 2013 11:39:29 +0200 | wenzelm | tuned signature -- more abstract PIDE editor operations; | file | diff | annotate |