1/* Title: Tools/jEdit/src-base/syntax_style.scala 2 Author: Makarius 3 4Extended syntax styles: dummy version. 5*/ 6 7package isabelle.jedit_base 8 9 10import isabelle._ 11 12import org.gjt.sp.util.SyntaxUtilities 13import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle} 14import org.gjt.sp.jedit.jEdit 15 16 17object Syntax_Style 18{ 19 private val plain_range: Int = JEditToken.ID_COUNT 20 private val full_range = 6 * plain_range + 1 21 22 object Dummy_Extender extends SyntaxUtilities.StyleExtender 23 { 24 override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] = 25 { 26 val new_styles = new Array[SyntaxStyle](full_range) 27 for (i <- 0 until full_range) { 28 new_styles(i) = styles(i % plain_range) 29 } 30 new_styles 31 } 32 } 33 34 def set_style_extender(extender: SyntaxUtilities.StyleExtender) 35 { 36 SyntaxUtilities.setStyleExtender(extender) 37 GUI_Thread.later { jEdit.propertiesChanged } 38 } 39 40 def dummy_style_extender() { set_style_extender(Dummy_Extender) } 41} 42