Tue, 14 Jun 2011 11:36:08 +0200 | wenzelm | separate module for text area painting; | file | diff | annotate |
Sun, 12 Jun 2011 20:08:49 +0200 | wenzelm | separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance; | file | diff | annotate |
Sun, 12 Jun 2011 16:19:29 +0200 | wenzelm | check source dependencies only if jedit_build component is available; | file | diff | annotate |
Thu, 09 Jun 2011 10:59:25 +0200 | wenzelm | tuned; | file | diff | annotate |
Wed, 08 Jun 2011 22:06:05 +0200 | wenzelm | simplified directory structure; | file | diff | annotate |
Wed, 08 Jun 2011 21:40:54 +0200 | wenzelm | simplified directory structure; | file | diff | annotate |
Wed, 08 Jun 2011 21:29:49 +0200 | wenzelm | further jedit build option; | file | diff | annotate |
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); | file | diff | annotate | base |