src/Tools/jEdit/src/token_markup.scala
Sat, 19 Sep 2015 19:34:51 +0200 wenzelm tuned signature;
Sun, 03 May 2015 14:12:10 +0200 wenzelm tuned message;
Mon, 06 Apr 2015 22:11:01 +0200 wenzelm support for 'restricted' modifier: only qualified accesses outside the local scope;
Sat, 04 Apr 2015 21:21:40 +0200 wenzelm more general notion of command span: command keyword not necessarily at start;
Mon, 05 Jan 2015 14:13:38 +0100 wenzelm GUI.imitate_font: more explicit result size, e.g. relevant for caching;
Thu, 01 Jan 2015 17:27:52 +0100 wenzelm tuned signature;
Wed, 03 Dec 2014 14:04:38 +0100 wenzelm tuned signature;
Tue, 02 Dec 2014 16:40:11 +0100 wenzelm tuned signature -- more explicit types;
Tue, 02 Dec 2014 14:16:56 +0100 wenzelm node-specific syntax, with base_syntax as default;
Mon, 01 Dec 2014 19:25:20 +0100 wenzelm clarified token marker / syntax for mode vs. buffer;
Sat, 29 Nov 2014 14:43:10 +0100 wenzelm encode text with control symbols;
Wed, 29 Oct 2014 09:42:46 +0100 wenzelm more iterators;
Tue, 28 Oct 2014 16:19:04 +0100 wenzelm find command span in buffer;
Tue, 21 Oct 2014 19:20:48 +0200 wenzelm added option jedit_structure_limit;
Tue, 21 Oct 2014 17:49:51 +0200 wenzelm some structure matching, based on line token iterators;
less more (0) -15 tip