token marker for extended syntax styles;

--- 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
 }