# HG changeset patch
# User wenzelm
# Date 1308653635 -7200
# Node ID 39035276927c57f0d5c81c728c4d1b8f8a1d4ea0
# Parent  98cd7e83fc5b43ec4416e31c8867301949ce7c52
Symbol.is_ctrl: handle decoded version as well;
clarified user font font index handling;

diff -r 98cd7e83fc5b -r 39035276927c src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Tue Jun 21 01:08:15 2011 +0200
+++ b/src/Pure/General/symbol.scala	Tue Jun 21 12:53:55 2011 +0200
@@ -234,6 +234,14 @@
       Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
     }
 
+    val abbrevs: Map[String, String] =
+      Map((
+        for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
+          yield (sym -> props("abbrev"))): _*)
+
+
+    /* user fonts */
+
     val fonts: Map[String, String] =
       Map((
         for ((sym, props) <- symbols if props.isDefinedAt("font"))
@@ -242,10 +250,7 @@
     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"))
-          yield (sym -> props("abbrev"))): _*)
+    def lookup_font(sym: String): Option[Int] = fonts.get(sym).map(font_index(_))
 
 
     /* main recoder methods */
@@ -336,10 +341,16 @@
       sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
 
 
-    /* special control symbols */
+    /* control symbols */
+
+    private val ctrl_decoded: Set[String] =
+      Set((for ((sym, _) <- symbols if sym.startsWith("\\<^")) yield decode(sym)): _*)
+
+    def is_ctrl(sym: String): Boolean =
+      sym.startsWith("\\<^") || ctrl_decoded.contains(sym)
 
     def is_controllable(sym: String): Boolean =
-      !is_blank(sym) && !sym.startsWith("\\<^") && !is_malformed(sym)
+      !is_blank(sym) && !is_ctrl(sym) && !is_malformed(sym)
 
     private val subscript_decoded = Set(decode("\\<^sub>"), decode("\\<^isub>"))
     private val superscript_decoded = Set(decode("\\<^sup>"), decode("\\<^isup>"))
diff -r 98cd7e83fc5b -r 39035276927c src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Tue Jun 21 01:08:15 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Jun 21 12:53:55 2011 +0200
@@ -25,6 +25,7 @@
   /* extended syntax styles */
 
   private val plain_range: Int = JEditToken.ID_COUNT
+  private val full_range = 6 * 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 }
@@ -50,7 +51,6 @@
   {
     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] =
     {
@@ -99,10 +99,8 @@
         }
         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), _))
+      symbols.lookup_font(sym) match {
+        case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
         case _ =>
       }
       offset += sym.length