src/Tools/jEdit/src/structure_matching.scala
2014-12-09 wenzelm 2014-12-09 tuned signature;
2014-12-01 wenzelm 2014-12-01 tuned signature;
2014-11-05 wenzelm 2014-11-05 clarified representation of type Keywords; tuned signature;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.Keywords;
2014-10-28 wenzelm 2014-10-28 tuned signature;
2014-10-28 wenzelm 2014-10-28 proper selectMatch, e.g. relevant for S-click on gutter;
2014-10-28 wenzelm 2014-10-28 explicit keyword category for commands that may start a block;
2014-10-22 wenzelm 2014-10-22 find main command keyword of 'begin';
2014-10-22 wenzelm 2014-10-22 restricted scanning;
2014-10-21 wenzelm 2014-10-21 ignore improper tokens to avoid ambiguity of Range.touches (assuming that relevant tokens are separated properly);
2014-10-21 wenzelm 2014-10-21 support for proof structure matching;
2014-10-21 wenzelm 2014-10-21 tuned;
2014-10-21 wenzelm 2014-10-21 support for begin/end matching;
2014-10-21 wenzelm 2014-10-21 added option jedit_structure_limit; tuned signature;
2014-10-21 wenzelm 2014-10-21 some structure matching, based on line token iterators;
2014-10-21 wenzelm 2014-10-21 support for structure matching; misc tuning;