src/Tools/jEdit/src-base/syntax_style.scala
changeset 66555 39257f39c7da
child 66602 180b2e72601f
equal deleted inserted replaced
66554:19bf4d5966dc 66555:39257f39c7da
       
     1 /*  Title:      Tools/jEdit/src-base/syntax_style.scala
       
     2     Author:     Makarius
       
     3 
       
     4 Extended syntax styles: dummy version.
       
     5 */
       
     6 
       
     7 package isabelle.jedit_base
       
     8 
       
     9 
       
    10 import isabelle._
       
    11 
       
    12 import org.gjt.sp.util.SyntaxUtilities
       
    13 import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle}
       
    14 
       
    15 
       
    16 object Syntax_Style
       
    17 {
       
    18   private val plain_range: Int = JEditToken.ID_COUNT
       
    19   private val full_range = 6 * plain_range + 1
       
    20 
       
    21   object Dummy_Extender extends SyntaxUtilities.StyleExtender
       
    22   {
       
    23     override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
       
    24     {
       
    25       val new_styles = new Array[SyntaxStyle](full_range)
       
    26       for (i <- 0 until full_range) {
       
    27         new_styles(i) = styles(i % plain_range)
       
    28       }
       
    29       new_styles
       
    30     }
       
    31   }
       
    32 }