src/Tools/jEdit/src/structure_matching.scala
Wed, 05 Nov 2014 16:57:12 +0100 wenzelm explicit type Keyword.Keywords;
Tue, 28 Oct 2014 16:27:11 +0100 wenzelm tuned signature;
Tue, 28 Oct 2014 16:20:26 +0100 wenzelm proper selectMatch, e.g. relevant for S-click on gutter;
Tue, 28 Oct 2014 11:42:51 +0100 wenzelm explicit keyword category for commands that may start a block;
Wed, 22 Oct 2014 17:04:45 +0200 wenzelm find main command keyword of 'begin';
Wed, 22 Oct 2014 16:44:57 +0200 wenzelm restricted scanning;
Tue, 21 Oct 2014 21:20:45 +0200 wenzelm ignore improper tokens to avoid ambiguity of Range.touches (assuming that relevant tokens are separated properly);
Tue, 21 Oct 2014 21:02:36 +0200 wenzelm support for proof structure matching;
Tue, 21 Oct 2014 20:45:05 +0200 wenzelm tuned;
Tue, 21 Oct 2014 20:19:14 +0200 wenzelm support for begin/end matching;
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;
Tue, 21 Oct 2014 15:21:44 +0200 wenzelm support for structure matching;
less more (0) tip