src/Tools/jEdit/src/syntax_style.scala
author wenzelm
Mon Dec 04 22:52:16 2017 +0100 (10 months ago)
changeset 67130 b023f64e0d16
parent 67128 4d91b6d5d49c
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Tools/jEdit/src/syntax_style.scala
     2     Author:     Makarius
     3 
     4 Support for extended syntax styles: subscript, superscript, bold, user fonts.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.awt.{Font, Color}
    13 import java.awt.font.TextAttribute
    14 import java.awt.geom.AffineTransform
    15 
    16 import org.gjt.sp.util.SyntaxUtilities
    17 import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle}
    18 import org.gjt.sp.jedit.textarea.TextArea
    19 
    20 
    21 object Syntax_Style
    22 {
    23   /* extended syntax styles */
    24 
    25   private val plain_range: Int = JEditToken.ID_COUNT
    26   private def check_range(i: Int) { require(0 <= i && i < plain_range) }
    27 
    28   def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
    29   def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
    30   def bold(i: Byte): Byte = { check_range(i); (i + 3 * plain_range).toByte }
    31   def user_font(idx: Int, i: Byte): Byte = { check_range(i); (i + (4 + idx) * plain_range).toByte }
    32   val hidden: Byte = (6 * plain_range).toByte
    33   val control: Byte = (hidden + JEditToken.DIGIT).toByte
    34 
    35   private def font_style(style: SyntaxStyle, f: Font => Font): SyntaxStyle =
    36     new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, f(style.getFont))
    37 
    38   private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
    39   {
    40     font_style(style, font0 =>
    41       {
    42         import scala.collection.JavaConversions._
    43         val font1 = font0.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
    44 
    45         def shift(y: Float): Font =
    46           GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))
    47 
    48         val m0 = GUI.line_metrics(font0)
    49         val m1 = GUI.line_metrics(font1)
    50         val a = m1.getAscent - m0.getAscent
    51         val b = (m1.getDescent + m1.getLeading) - (m0.getDescent + m0.getLeading)
    52         if (a > 0.0f) shift(a)
    53         else if (b > 0.0f) shift(- b)
    54         else font1
    55       })
    56   }
    57 
    58   private def bold_style(style: SyntaxStyle): SyntaxStyle =
    59     font_style(style, font => font.deriveFont(if (font.isBold) Font.PLAIN else Font.BOLD))
    60 
    61   val hidden_color: Color = new Color(255, 255, 255, 0)
    62 
    63   object Extender extends SyntaxUtilities.StyleExtender
    64   {
    65     val max_user_fonts = 2
    66     if (Symbol.font_names.length > max_user_fonts)
    67       error("Too many user symbol fonts (" + max_user_fonts + " permitted): " +
    68         Symbol.font_names.mkString(", "))
    69 
    70     override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
    71     {
    72       val style0 = styles(0)
    73       val font0 = style0.getFont
    74 
    75       val new_styles = Array.fill[SyntaxStyle](java.lang.Byte.MAX_VALUE)(styles(0))
    76       for (i <- 0 until plain_range) {
    77         val style = styles(i)
    78         new_styles(i) = style
    79         new_styles(subscript(i.toByte)) = script_style(style, -1)
    80         new_styles(superscript(i.toByte)) = script_style(style, 1)
    81         new_styles(bold(i.toByte)) = bold_style(style)
    82         for (idx <- 0 until max_user_fonts)
    83           new_styles(user_font(idx, i.toByte)) = style
    84         for ((family, idx) <- Symbol.font_index)
    85           new_styles(user_font(idx, i.toByte)) = font_style(style, GUI.imitate_font(_, family))
    86       }
    87       new_styles(hidden) =
    88         new SyntaxStyle(hidden_color, null,
    89           GUI.transform_font(new Font(font0.getFamily, 0, 1),
    90             AffineTransform.getScaleInstance(1.0, font0.getSize.toDouble)))
    91       new_styles(control) =
    92         new SyntaxStyle(style0.getForegroundColor, style0.getBackgroundColor,
    93           { val font_style =
    94               (if (font0.isItalic) 0 else Font.ITALIC) |
    95               (if (font0.isBold) 0 else Font.BOLD)
    96             new Font(font0.getFamily, font_style, font0.getSize) })
    97       new_styles
    98     }
    99   }
   100 
   101   private def control_style(sym: String): Option[Byte => Byte] =
   102     if (sym == Symbol.sub_decoded) Some(subscript(_))
   103     else if (sym == Symbol.sup_decoded) Some(superscript(_))
   104     else if (sym == Symbol.bold_decoded) Some(bold(_))
   105     else None
   106 
   107   def extended(text: CharSequence): Map[Text.Offset, Byte => Byte] =
   108   {
   109     var result = Map[Text.Offset, Byte => Byte]()
   110     def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte)
   111     {
   112       for (i <- start until stop) result += (i -> style)
   113     }
   114 
   115     var offset = 0
   116     var control_sym = ""
   117     for (sym <- Symbol.iterator(text)) {
   118       val end_offset = offset + sym.length
   119 
   120       if (control_style(sym).isDefined) control_sym = sym
   121       else if (control_sym != "") {
   122         if (Symbol.is_controllable(sym) && !Symbol.fonts.isDefinedAt(sym)) {
   123           mark(offset - control_sym.length, offset, _ => hidden)
   124           mark(offset, end_offset, control_style(control_sym).get)
   125         }
   126         control_sym = ""
   127       }
   128 
   129       if (Symbol.is_control_encoded(sym)) {
   130         val a = offset + Symbol.control_prefix.length
   131         val b = end_offset - Symbol.control_suffix.length
   132         mark(offset, a, _ => hidden)
   133         mark(a, b, _ => control)
   134         mark(b, end_offset, _ => hidden)
   135       }
   136 
   137       Symbol.lookup_font(sym) match {
   138         case Some(idx) => mark(offset, end_offset, user_font(idx, _))
   139         case _ =>
   140       }
   141 
   142       offset = end_offset
   143     }
   144 
   145     result
   146   }
   147 
   148 
   149   /* editing support for control symbols */
   150 
   151   def edit_control_style(text_area: TextArea, control: String)
   152   {
   153     GUI_Thread.assert {}
   154 
   155     val buffer = text_area.getBuffer
   156 
   157     val control_decoded = Isabelle_Encoding.perhaps_decode(buffer, control)
   158 
   159     def update_style(text: String): String =
   160     {
   161       val result = new StringBuilder
   162       for (sym <- Symbol.iterator(text) if !HTML.is_control(sym)) {
   163         if (Symbol.is_controllable(sym)) result ++= control_decoded
   164         result ++= sym
   165       }
   166       result.toString
   167     }
   168 
   169     text_area.getSelection.foreach(sel => {
   170       val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
   171       JEdit_Lib.get_text(buffer, before) match {
   172         case Some(s) if HTML.is_control(s) =>
   173           text_area.extendSelection(before.start, before.stop)
   174         case _ =>
   175       }
   176     })
   177 
   178     text_area.getSelection.toList match {
   179       case Nil =>
   180         text_area.setSelectedText(control_decoded)
   181       case sels =>
   182         JEdit_Lib.buffer_edit(buffer) {
   183           sels.foreach(sel =>
   184             text_area.setSelectedText(sel, update_style(text_area.getSelectedText(sel))))
   185         }
   186     }
   187   }
   188 }