src/Tools/jEdit/src/syntax_style.scala
changeset 67127 cf111622c9f8
parent 67125 361b3ef643a7
child 67128 4d91b6d5d49c
equal deleted inserted replaced
67126:143f0ba01415 67127:cf111622c9f8
    88               AffineTransform.getScaleInstance(1.0, font.getSize.toDouble)) })
    88               AffineTransform.getScaleInstance(1.0, font.getSize.toDouble)) })
    89       new_styles
    89       new_styles
    90     }
    90     }
    91   }
    91   }
    92 
    92 
       
    93   private def control_style(sym: String): Option[Byte => Byte] =
       
    94     if (sym == Symbol.sub_decoded) Some(subscript(_))
       
    95     else if (sym == Symbol.sup_decoded) Some(superscript(_))
       
    96     else if (sym == Symbol.bold_decoded) Some(bold(_))
       
    97     else None
       
    98 
    93   def extended(text: CharSequence): Map[Text.Offset, Byte => Byte] =
    99   def extended(text: CharSequence): Map[Text.Offset, Byte => Byte] =
    94   {
   100   {
    95     def control_style(sym: String): Option[Byte => Byte] =
       
    96       if (sym == Symbol.sub_decoded) Some(subscript(_))
       
    97       else if (sym == Symbol.sup_decoded) Some(superscript(_))
       
    98       else if (sym == Symbol.bold_decoded) Some(bold(_))
       
    99       else None
       
   100 
       
   101     var result = Map[Text.Offset, Byte => Byte]()
   101     var result = Map[Text.Offset, Byte => Byte]()
   102     def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte)
   102     def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte)
   103     {
   103     {
   104       for (i <- start until stop) result += (i -> style)
   104       for (i <- start until stop) result += (i -> style)
   105     }
   105     }
       
   106 
   106     var offset = 0
   107     var offset = 0
   107     var control = ""
   108     var control = ""
   108     for (sym <- Symbol.iterator(text)) {
   109     for (sym <- Symbol.iterator(text)) {
       
   110       val end_offset = offset + sym.length
       
   111 
   109       if (control_style(sym).isDefined) control = sym
   112       if (control_style(sym).isDefined) control = sym
   110       else if (control != "") {
   113       else if (control != "") {
   111         if (Symbol.is_controllable(sym) && !Symbol.fonts.isDefinedAt(sym)) {
   114         if (Symbol.is_controllable(sym) && !Symbol.fonts.isDefinedAt(sym)) {
   112           mark(offset - control.length, offset, _ => hidden)
   115           mark(offset - control.length, offset, _ => hidden)
   113           mark(offset, offset + sym.length, control_style(control).get)
   116           mark(offset, end_offset, control_style(control).get)
   114         }
   117         }
   115         control = ""
   118         control = ""
   116       }
   119       }
       
   120 
       
   121       if (Symbol.is_control_encoded(sym)) {
       
   122         val a = offset + Symbol.control_prefix.length
       
   123         val b = end_offset - Symbol.control_suffix.length
       
   124         mark(offset, a, _ => hidden)
       
   125         mark(a, b, _ => JEditToken.KEYWORD4)
       
   126         mark(b, end_offset, _ => hidden)
       
   127       }
       
   128 
   117       Symbol.lookup_font(sym) match {
   129       Symbol.lookup_font(sym) match {
   118         case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
   130         case Some(idx) => mark(offset, end_offset, user_font(idx, _))
   119         case _ =>
   131         case _ =>
   120       }
   132       }
   121       offset += sym.length
   133 
       
   134       offset = end_offset
   122     }
   135     }
       
   136 
   123     result
   137     result
   124   }
   138   }
   125 
   139 
   126 
   140 
   127   /* editing support for control symbols */
   141   /* editing support for control symbols */