src/Tools/jEdit/src/token_markup.scala
2011-06-16 wenzelm 2011-06-16 static token markup, based on outer syntax only; eliminated obsolete buffer.propertiesChanged (expensive due to remarking of full buffer etc.);