# HG changeset patch
# User wenzelm
# Date 1308611295 -7200
# Node ID 98cd7e83fc5b43ec4416e31c8867301949ce7c52
# Parent  4a1ef71fbf5f376650a747415d039fb7d31fb536
some support for user symbol fonts;

diff -r 4a1ef71fbf5f -r 98cd7e83fc5b src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Mon Jun 20 23:25:39 2011 +0200
+++ b/src/Pure/General/symbol.scala	Tue Jun 21 01:08:15 2011 +0200
@@ -234,6 +234,14 @@
       Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
     }
 
+    val fonts: Map[String, String] =
+      Map((
+        for ((sym, props) <- symbols if props.isDefinedAt("font"))
+          yield (sym -> props("font"))): _*)
+
+    val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList
+    val font_index: Map[String, Int] = Map((font_names zip (0 until font_names.length).toList): _*)
+
     val abbrevs: Map[String, String] =
       Map((
         for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
diff -r 4a1ef71fbf5f -r 98cd7e83fc5b src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Jun 20 23:25:39 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Jun 21 01:08:15 2011 +0200
@@ -396,7 +396,7 @@
     Isabelle.system = new Isabelle_System
     Isabelle.system.install_fonts()
     Isabelle.session = new Session(Isabelle.system)
-    SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
+    SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender(Isabelle.system.symbols))
     ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
     Isabelle.session.phase_changed += session_manager
   }
diff -r 4a1ef71fbf5f -r 98cd7e83fc5b src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Mon Jun 20 23:25:39 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Jun 21 01:08:15 2011 +0200
@@ -25,27 +25,33 @@
   /* extended syntax styles */
 
   private val plain_range: Int = JEditToken.ID_COUNT
-  private val full_range: Int = 4 * plain_range + 1
   private def check_range(i: Int) { require(0 <= i && i < plain_range) }
 
   def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
   def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
   def bold(i: Byte): Byte = { check_range(i); (i + 3 * plain_range).toByte }
-  val hidden: Byte = (4 * plain_range).toByte
+  def user_font(idx: Int, i: Byte): Byte = { check_range(i); (i + (4 + idx) * plain_range).toByte }
+  val hidden: Byte = (6 * plain_range).toByte
+
+  private def font_style(style: SyntaxStyle, f: Font => Font): SyntaxStyle =
+    new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, f(style.getFont))
 
   private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
   {
     import scala.collection.JavaConversions._
-    val font = style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
-    new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, font)
+    font_style(style, font =>
+      style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i))))
   }
 
   private def bold_style(style: SyntaxStyle): SyntaxStyle =
-    new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor,
-      style.getFont.deriveFont(Font.BOLD))
+    font_style(style, _.deriveFont(Font.BOLD))
 
-  class Style_Extender extends SyntaxUtilities.StyleExtender
+  class Style_Extender(symbols: Symbol.Interpretation) extends SyntaxUtilities.StyleExtender
   {
+    if (symbols.font_names.length > 2)
+      error("Too many user symbol fonts (max 2 permitted): " + symbols.font_names.mkString(", "))
+    private val full_range: Int = (4 + symbols.font_names.length) * plain_range + 1
+
     override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
     {
       val new_styles = new Array[SyntaxStyle](full_range)
@@ -55,6 +61,11 @@
         new_styles(subscript(i.toByte)) = script_style(style, -1)
         new_styles(superscript(i.toByte)) = script_style(style, 1)
         new_styles(bold(i.toByte)) = bold_style(style)
+        for ((family, idx) <- symbols.font_index) {
+          // FIXME adjust size
+          new_styles(user_font(idx, i.toByte)) =
+            font_style(style, font => new Font(family, font.getStyle, font.getSize))
+        }
       }
       new_styles(hidden) =
         new SyntaxStyle(Color.white, null, new Font(styles(0).getFont.getFamily, 0, 1))
@@ -62,7 +73,7 @@
     }
   }
 
-  private def extended_styles(symbols: Symbol.Interpretation, text: CharSequence)
+  def extended_styles(symbols: Symbol.Interpretation, text: CharSequence)
     : Map[Text.Offset, Byte => Byte] =
   {
     // FIXME \\<^bsub> \\<^esub> \\<^bsup> \\<^esup>
@@ -82,12 +93,18 @@
     for (sym <- Symbol.iterator(text).map(_.toString)) {
       if (ctrl_style(sym).isDefined) ctrl = sym
       else if (ctrl != "") {
-        if (symbols.is_controllable(sym) && sym != "\"") {
+        if (symbols.is_controllable(sym) && sym != "\"" && !symbols.fonts.isDefinedAt(sym)) {
           mark(offset - ctrl.length, offset, _ => hidden)
           mark(offset, offset + sym.length, ctrl_style(ctrl).get)
         }
         ctrl = ""
       }
+      // FIXME avoid symbols.encode!?
+      symbols.fonts.get(symbols.encode(sym)) match {
+        case Some(font) =>
+          mark(offset, offset + sym.length, user_font(symbols.font_index(font), _))
+        case _ =>
+      }
       offset += sym.length
     }
     result