| Mon, 13 Jun 2011 23:09:01 +0200 | wenzelm | some direct text foreground painting, instead of token marking; | file | diff | annotate |
| Mon, 13 Jun 2011 14:22:33 +0200 | wenzelm | imitate original Chunk.paintChunkList; | file | diff | annotate |
| Mon, 13 Jun 2011 13:53:41 +0200 | wenzelm | tuned; | file | diff | annotate |
| Mon, 13 Jun 2011 12:33:53 +0200 | wenzelm | always use our text painter; | file | diff | annotate |
| Mon, 13 Jun 2011 12:29:26 +0200 | wenzelm | use orig_text_painter for extras outside main text (also required to update internal line infos); | file | diff | annotate |
| Sun, 12 Jun 2011 22:26:03 +0200 | wenzelm | more precise imitation of original TextAreaPainter$PaintText; | file | diff | annotate |
| Sun, 12 Jun 2011 20:24:25 +0200 | wenzelm | tuned; | 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 |