clarified control style;
authorwenzelm
Mon Dec 04 18:30:28 2017 +0100 (7 weeks ago)
changeset 671284d91b6d5d49c
parent 67127 cf111622c9f8
child 67129 0262a378d5d6
clarified control style;
src/Tools/jEdit/src/syntax_style.scala
     1.1 --- a/src/Tools/jEdit/src/syntax_style.scala	Mon Dec 04 17:37:26 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/syntax_style.scala	Mon Dec 04 18:30:28 2017 +0100
     1.3 @@ -23,7 +23,6 @@
     1.4    /* extended syntax styles */
     1.5  
     1.6    private val plain_range: Int = JEditToken.ID_COUNT
     1.7 -  private val full_range = 6 * plain_range + 1
     1.8    private def check_range(i: Int) { require(0 <= i && i < plain_range) }
     1.9  
    1.10    def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
    1.11 @@ -31,6 +30,7 @@
    1.12    def bold(i: Byte): Byte = { check_range(i); (i + 3 * plain_range).toByte }
    1.13    def user_font(idx: Int, i: Byte): Byte = { check_range(i); (i + (4 + idx) * plain_range).toByte }
    1.14    val hidden: Byte = (6 * plain_range).toByte
    1.15 +  val control: Byte = (hidden + JEditToken.DIGIT).toByte
    1.16  
    1.17    private def font_style(style: SyntaxStyle, f: Font => Font): SyntaxStyle =
    1.18      new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, f(style.getFont))
    1.19 @@ -69,7 +69,10 @@
    1.20  
    1.21      override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
    1.22      {
    1.23 -      val new_styles = new Array[SyntaxStyle](full_range)
    1.24 +      val style0 = styles(0)
    1.25 +      val font0 = style0.getFont
    1.26 +
    1.27 +      val new_styles = Array.fill[SyntaxStyle](java.lang.Byte.MAX_VALUE)(styles(0))
    1.28        for (i <- 0 until plain_range) {
    1.29          val style = styles(i)
    1.30          new_styles(i) = style
    1.31 @@ -83,9 +86,14 @@
    1.32        }
    1.33        new_styles(hidden) =
    1.34          new SyntaxStyle(hidden_color, null,
    1.35 -          { val font = styles(0).getFont
    1.36 -            GUI.transform_font(new Font(font.getFamily, 0, 1),
    1.37 -              AffineTransform.getScaleInstance(1.0, font.getSize.toDouble)) })
    1.38 +          GUI.transform_font(new Font(font0.getFamily, 0, 1),
    1.39 +            AffineTransform.getScaleInstance(1.0, font0.getSize.toDouble)))
    1.40 +      new_styles(control) =
    1.41 +        new SyntaxStyle(style0.getForegroundColor, style0.getBackgroundColor,
    1.42 +          { val font_style =
    1.43 +              (if (font0.isItalic) 0 else Font.ITALIC) |
    1.44 +              (if (font0.isBold) 0 else Font.BOLD)
    1.45 +            new Font(font0.getFamily, font_style, font0.getSize) })
    1.46        new_styles
    1.47      }
    1.48    }
    1.49 @@ -105,24 +113,24 @@
    1.50      }
    1.51  
    1.52      var offset = 0
    1.53 -    var control = ""
    1.54 +    var control_sym = ""
    1.55      for (sym <- Symbol.iterator(text)) {
    1.56        val end_offset = offset + sym.length
    1.57  
    1.58 -      if (control_style(sym).isDefined) control = sym
    1.59 -      else if (control != "") {
    1.60 +      if (control_style(sym).isDefined) control_sym = sym
    1.61 +      else if (control_sym != "") {
    1.62          if (Symbol.is_controllable(sym) && !Symbol.fonts.isDefinedAt(sym)) {
    1.63 -          mark(offset - control.length, offset, _ => hidden)
    1.64 -          mark(offset, end_offset, control_style(control).get)
    1.65 +          mark(offset - control_sym.length, offset, _ => hidden)
    1.66 +          mark(offset, end_offset, control_style(control_sym).get)
    1.67          }
    1.68 -        control = ""
    1.69 +        control_sym = ""
    1.70        }
    1.71  
    1.72        if (Symbol.is_control_encoded(sym)) {
    1.73          val a = offset + Symbol.control_prefix.length
    1.74          val b = end_offset - Symbol.control_suffix.length
    1.75          mark(offset, a, _ => hidden)
    1.76 -        mark(a, b, _ => JEditToken.KEYWORD4)
    1.77 +        mark(a, b, _ => control)
    1.78          mark(b, end_offset, _ => hidden)
    1.79        }
    1.80