| Mon, 12 Aug 2013 18:02:01 +0200 | wenzelm | merged | changeset | files |
| Mon, 12 Aug 2013 17:57:51 +0200 | wenzelm | clarified Query_Operation.register: avoid hard-wired parallel policy; | changeset | files |
| Mon, 12 Aug 2013 17:17:49 +0200 | wenzelm | moved generic module to its proper place; | changeset | files |
| Mon, 12 Aug 2013 17:11:27 +0200 | wenzelm | manage hyperlinks via PIDE editor interface; | changeset | files |
| Mon, 12 Aug 2013 15:09:13 +0200 | wenzelm | tuned whitespace; | changeset | files |
| Mon, 12 Aug 2013 14:53:16 +0200 | wenzelm | prefer PIDE editor operations; | changeset | files |
| Mon, 12 Aug 2013 14:27:58 +0200 | wenzelm | central management of Document.Overlays, independent of Document_Model; | changeset | files |
| Mon, 12 Aug 2013 13:32:26 +0200 | wenzelm | tuned -- use Multi_Map; | changeset | files |