src/Pure/Thy/html.scala
changeset 43490 5e6f76cacb93
parent 43489 132f99cc0a43
child 43511 d138e7482a1b
     1.1 --- a/src/Pure/Thy/html.scala	Tue Jun 21 13:29:44 2011 +0200
     1.2 +++ b/src/Pure/Thy/html.scala	Tue Jun 21 14:12:49 2011 +0200
     1.3 @@ -37,6 +37,7 @@
     1.4    val BR = "br"
     1.5    val PRE = "pre"
     1.6    val CLASS = "class"
     1.7 +  val STYLE = "style"
     1.8  
     1.9  
    1.10    // document markup
    1.11 @@ -44,6 +45,9 @@
    1.12    def span(cls: String, body: XML.Body): XML.Elem =
    1.13      XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
    1.14  
    1.15 +  def user_font(font: String, txt: String): XML.Elem =
    1.16 +    XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))
    1.17 +
    1.18    def hidden(txt: String): XML.Elem =
    1.19      span(Markup.HIDDEN, List(XML.Text(txt)))
    1.20  
    1.21 @@ -85,6 +89,7 @@
    1.22              else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
    1.23              else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
    1.24              else if (symbols.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) }
    1.25 +            else if (symbols.fonts.isDefinedAt(s1)) { add(user_font(symbols.fonts(s1), s1)) }
    1.26              else t ++= s1
    1.27            }
    1.28            flush()