| Wed, 09 Apr 2014 13:32:34 +0200 |
wenzelm |
avoid confusion about pointless cursor movement with external links;
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 12:54:12 +0100 |
wenzelm |
tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
|
file |
diff |
annotate
|
| Mon, 03 Mar 2014 10:41:58 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 09 Dec 2013 12:16:52 +0100 |
wenzelm |
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
|
file |
diff |
annotate
|
| Sun, 17 Nov 2013 16:02:06 +0100 |
wenzelm |
centralized management of pending buffer edits;
|
file |
diff |
annotate
|
| 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.;
|
file |
diff |
annotate
|
| 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
|