| Mon, 31 Dec 2018 20:08:32 +0100 | wenzelm | tuned; | file | diff | annotate |
| Tue, 05 Jun 2018 16:12:26 +0200 | wenzelm | less wasteful consolidation, based on PIDE front-end state and recent changes; | file | diff | annotate |
| Thu, 31 May 2018 22:27:13 +0200 | wenzelm | Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread; | file | diff | annotate |
| Fri, 06 Oct 2017 21:23:21 +0200 | wenzelm | even more robust syntax (amending 122df1fde073); | file | diff | annotate |
| Fri, 06 Oct 2017 17:13:57 +0200 | wenzelm | clarified node_syntax (amending ae38b8c0fdd9): default to overall_syntax, e.g. relevant for command spans wrt. bad header; | file | diff | annotate |
| Fri, 29 Sep 2017 22:41:19 +0200 | wenzelm | more accurate node_syntax: avoid overall_syntax for PIDE edits; | file | diff | annotate |
| Fri, 29 Sep 2017 22:12:32 +0200 | wenzelm | tuned signature; | file | diff | annotate |