diff -r e2726211f834 -r 32cb1f1a6a5d src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Tue Sep 18 19:33:45 2012 +0200 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Tue Sep 18 19:42:32 2012 +0200 @@ -119,6 +119,7 @@ refresh() } + text_area.getBuffer.setTokenMarker(new Token_Markup.Marker(true, None)) rich_text_area.activate() layout(Component.wrap(text_area)) = BorderPanel.Position.Center }