some support for user symbol fonts;
authorwenzelm
Tue Jun 21 01:08:15 2011 +0200 (2011-06-21)
changeset 4348798cd7e83fc5b
parent 43486 4a1ef71fbf5f
child 43488 39035276927c
some support for user symbol fonts;
src/Pure/General/symbol.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/General/symbol.scala	Mon Jun 20 23:25:39 2011 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Tue Jun 21 01:08:15 2011 +0200
     1.3 @@ -234,6 +234,14 @@
     1.4        Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
     1.5      }
     1.6  
     1.7 +    val fonts: Map[String, String] =
     1.8 +      Map((
     1.9 +        for ((sym, props) <- symbols if props.isDefinedAt("font"))
    1.10 +          yield (sym -> props("font"))): _*)
    1.11 +
    1.12 +    val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList
    1.13 +    val font_index: Map[String, Int] = Map((font_names zip (0 until font_names.length).toList): _*)
    1.14 +
    1.15      val abbrevs: Map[String, String] =
    1.16        Map((
    1.17          for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Jun 20 23:25:39 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Jun 21 01:08:15 2011 +0200
     2.3 @@ -396,7 +396,7 @@
     2.4      Isabelle.system = new Isabelle_System
     2.5      Isabelle.system.install_fonts()
     2.6      Isabelle.session = new Session(Isabelle.system)
     2.7 -    SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
     2.8 +    SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender(Isabelle.system.symbols))
     2.9      ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
    2.10      Isabelle.session.phase_changed += session_manager
    2.11    }
     3.1 --- a/src/Tools/jEdit/src/token_markup.scala	Mon Jun 20 23:25:39 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Tue Jun 21 01:08:15 2011 +0200
     3.3 @@ -25,27 +25,33 @@
     3.4    /* extended syntax styles */
     3.5  
     3.6    private val plain_range: Int = JEditToken.ID_COUNT
     3.7 -  private val full_range: Int = 4 * plain_range + 1
     3.8    private def check_range(i: Int) { require(0 <= i && i < plain_range) }
     3.9  
    3.10    def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
    3.11    def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
    3.12    def bold(i: Byte): Byte = { check_range(i); (i + 3 * plain_range).toByte }
    3.13 -  val hidden: Byte = (4 * plain_range).toByte
    3.14 +  def user_font(idx: Int, i: Byte): Byte = { check_range(i); (i + (4 + idx) * plain_range).toByte }
    3.15 +  val hidden: Byte = (6 * plain_range).toByte
    3.16 +
    3.17 +  private def font_style(style: SyntaxStyle, f: Font => Font): SyntaxStyle =
    3.18 +    new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, f(style.getFont))
    3.19  
    3.20    private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
    3.21    {
    3.22      import scala.collection.JavaConversions._
    3.23 -    val font = style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
    3.24 -    new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, font)
    3.25 +    font_style(style, font =>
    3.26 +      style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i))))
    3.27    }
    3.28  
    3.29    private def bold_style(style: SyntaxStyle): SyntaxStyle =
    3.30 -    new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor,
    3.31 -      style.getFont.deriveFont(Font.BOLD))
    3.32 +    font_style(style, _.deriveFont(Font.BOLD))
    3.33  
    3.34 -  class Style_Extender extends SyntaxUtilities.StyleExtender
    3.35 +  class Style_Extender(symbols: Symbol.Interpretation) extends SyntaxUtilities.StyleExtender
    3.36    {
    3.37 +    if (symbols.font_names.length > 2)
    3.38 +      error("Too many user symbol fonts (max 2 permitted): " + symbols.font_names.mkString(", "))
    3.39 +    private val full_range: Int = (4 + symbols.font_names.length) * plain_range + 1
    3.40 +
    3.41      override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
    3.42      {
    3.43        val new_styles = new Array[SyntaxStyle](full_range)
    3.44 @@ -55,6 +61,11 @@
    3.45          new_styles(subscript(i.toByte)) = script_style(style, -1)
    3.46          new_styles(superscript(i.toByte)) = script_style(style, 1)
    3.47          new_styles(bold(i.toByte)) = bold_style(style)
    3.48 +        for ((family, idx) <- symbols.font_index) {
    3.49 +          // FIXME adjust size
    3.50 +          new_styles(user_font(idx, i.toByte)) =
    3.51 +            font_style(style, font => new Font(family, font.getStyle, font.getSize))
    3.52 +        }
    3.53        }
    3.54        new_styles(hidden) =
    3.55          new SyntaxStyle(Color.white, null, new Font(styles(0).getFont.getFamily, 0, 1))
    3.56 @@ -62,7 +73,7 @@
    3.57      }
    3.58    }
    3.59  
    3.60 -  private def extended_styles(symbols: Symbol.Interpretation, text: CharSequence)
    3.61 +  def extended_styles(symbols: Symbol.Interpretation, text: CharSequence)
    3.62      : Map[Text.Offset, Byte => Byte] =
    3.63    {
    3.64      // FIXME \\<^bsub> \\<^esub> \\<^bsup> \\<^esup>
    3.65 @@ -82,12 +93,18 @@
    3.66      for (sym <- Symbol.iterator(text).map(_.toString)) {
    3.67        if (ctrl_style(sym).isDefined) ctrl = sym
    3.68        else if (ctrl != "") {
    3.69 -        if (symbols.is_controllable(sym) && sym != "\"") {
    3.70 +        if (symbols.is_controllable(sym) && sym != "\"" && !symbols.fonts.isDefinedAt(sym)) {
    3.71            mark(offset - ctrl.length, offset, _ => hidden)
    3.72            mark(offset, offset + sym.length, ctrl_style(ctrl).get)
    3.73          }
    3.74          ctrl = ""
    3.75        }
    3.76 +      // FIXME avoid symbols.encode!?
    3.77 +      symbols.fonts.get(symbols.encode(sym)) match {
    3.78 +        case Some(font) =>
    3.79 +          mark(offset, offset + sym.length, user_font(symbols.font_index(font), _))
    3.80 +        case _ =>
    3.81 +      }
    3.82        offset += sym.length
    3.83      }
    3.84      result