# HG changeset patch
# User wenzelm
# Date 1308658369 -7200
# Node ID 5e6f76cacb93ba9e00b040aa63a630f1ba36f9f0
# Parent  132f99cc0a43614fb48b849d7ba24701b329ad7f
more uniform treatment of recode_set/recode_map;
HTML spans with user fonts;

diff -r 132f99cc0a43 -r 5e6f76cacb93 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Tue Jun 21 13:29:44 2011 +0200
+++ b/src/Pure/General/symbol.scala	Tue Jun 21 14:12:49 2011 +0200
@@ -103,7 +103,7 @@
     }
 
   private val char_symbols: Array[String] =
-    (0 to 127).iterator.map(i => new String(Array(i.toChar))).toArray
+    (0 until 128).iterator.map(i => new String(Array(i.toChar))).toArray
 
   private def make_string(sym: CharSequence): String =
     sym.length match {
@@ -257,20 +257,7 @@
           yield (sym -> props("abbrev"))): _*)
 
 
-    /* user fonts */
-
-    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): _*)
-
-    def lookup_font(sym: String): Option[Int] = fonts.get(sym).map(font_index(_))
-
-
-    /* main recoder methods */
+    /* recoding */
 
     private val (decoder, encoder) =
     {
@@ -295,19 +282,35 @@
     def decode(text: String): String = decoder.recode(text)
     def encode(text: String): String = encoder.recode(text)
 
+    private def recode_set(elems: String*): Set[String] =
+    {
+      val content = elems.toList
+      Set((content ::: content.map(decode)): _*)
+    }
+
+    private def recode_map[A](elems: (String, A)*): Map[String, A] =
+    {
+      val content = elems.toList
+      Map((content ::: content.map({ case (sym, a) => (decode(sym), a) })): _*)
+    }
+
+
+    /* user fonts */
+
+    val fonts: Map[String, String] =
+      recode_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): _*)
+
+    def lookup_font(sym: String): Option[Int] = fonts.get(sym).map(font_index(_))
+
 
     /* classification */
 
-    private object Decode_Set
-    {
-      def apply(elems: String*): Set[String] =
-      {
-        val content = elems.toList
-        Set((content ::: content.map(decode)): _*)
-      }
-    }
-
-    private val letters = Decode_Set(
+    private val letters = recode_set(
       "A", "B", "C", "D", "E", "F", "G", "H", "I", "J", "K", "L", "M",
       "N", "O", "P", "Q", "R", "S", "T", "U", "V", "W", "X", "Y", "Z",
       "a", "b", "c", "d", "e", "f", "g", "h", "i", "j", "k", "l", "m",
@@ -343,7 +346,7 @@
       "\\<^isub>", "\\<^isup>")
 
     private val blanks =
-      Decode_Set(space, "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
+      recode_set(space, "\t", "\n", "\u000B", "\f", "\r", "\\<spacespace>", "\\<^newline>")
 
     private val sym_chars =
       Set("!", "#", "$", "%", "&", "*", "+", "-", "/", "<", "=", ">", "?", "@", "^", "_", "|", "~")
diff -r 132f99cc0a43 -r 5e6f76cacb93 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Tue Jun 21 13:29:44 2011 +0200
+++ b/src/Pure/Thy/html.scala	Tue Jun 21 14:12:49 2011 +0200
@@ -37,6 +37,7 @@
   val BR = "br"
   val PRE = "pre"
   val CLASS = "class"
+  val STYLE = "style"
 
 
   // document markup
@@ -44,6 +45,9 @@
   def span(cls: String, body: XML.Body): XML.Elem =
     XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
 
+  def user_font(font: String, txt: String): XML.Elem =
+    XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))
+
   def hidden(txt: String): XML.Elem =
     span(Markup.HIDDEN, List(XML.Text(txt)))
 
@@ -85,6 +89,7 @@
             else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
             else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
             else if (symbols.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) }
+            else if (symbols.fonts.isDefinedAt(s1)) { add(user_font(symbols.fonts(s1), s1)) }
             else t ++= s1
           }
           flush()