src/Tools/jEdit/lib/Tools/jedit
Tue, 14 Jun 2011 11:36:08 +0200 wenzelm separate module for text area painting;
Sun, 12 Jun 2011 20:08:49 +0200 wenzelm separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
Sun, 12 Jun 2011 16:19:29 +0200 wenzelm check source dependencies only if jedit_build component is available;
Thu, 09 Jun 2011 10:59:25 +0200 wenzelm tuned;
Wed, 08 Jun 2011 22:06:05 +0200 wenzelm simplified directory structure;
Wed, 08 Jun 2011 21:40:54 +0200 wenzelm simplified directory structure;
Wed, 08 Jun 2011 21:29:49 +0200 wenzelm further jedit build option;
Wed, 08 Jun 2011 20:58:51 +0200 wenzelm build jedit as part of regular startup script (in that case depending on jedit_build component);
less more (0) tip