wenzelm@33984: /*  Title:      Pure/Thy/html.scala
wenzelm@33984:     Author:     Makarius
wenzelm@33984: 
wenzelm@33984: Basic HTML output.
wenzelm@33984: */
wenzelm@33984: 
wenzelm@33984: package isabelle
wenzelm@33984: 
wenzelm@34009: import scala.collection.mutable.ListBuffer
wenzelm@34009: 
wenzelm@34009: 
wenzelm@33984: object HTML
wenzelm@33984: {
wenzelm@37201:   // encode text
wenzelm@37201: 
wenzelm@37201:   def encode(text: String): String =
wenzelm@37201:   {
wenzelm@37201:     val s = new StringBuilder
wenzelm@37201:     for (c <- text.iterator) c match {
wenzelm@37201:       case '<' => s ++= "&lt;"
wenzelm@37201:       case '>' => s ++= "&gt;"
wenzelm@37201:       case '&' => s ++= "&amp;"
wenzelm@37201:       case '"' => s ++= "&quot;"
wenzelm@37201:       case '\'' => s ++= "&#39;"
wenzelm@37201:       case '\n' => s ++= "<br/>"
wenzelm@37201:       case _ => s += c
wenzelm@37201:     }
wenzelm@37201:     s.toString
wenzelm@37201:   }
wenzelm@37201: 
wenzelm@37201: 
wenzelm@33984:   // common elements and attributes
wenzelm@33984: 
wenzelm@33984:   val BODY = "body"
wenzelm@33984:   val DIV = "div"
wenzelm@33984:   val SPAN = "span"
wenzelm@33984:   val BR = "br"
wenzelm@34009:   val PRE = "pre"
wenzelm@33984:   val CLASS = "class"
wenzelm@44361:   val STYLE = "style"
wenzelm@33984: 
wenzelm@33984: 
wenzelm@33984:   // document markup
wenzelm@33984: 
wenzelm@38867:   def span(cls: String, body: XML.Body): XML.Elem =
wenzelm@38486:     XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
wenzelm@34011: 
wenzelm@44361:   def user_font(font: String, txt: String): XML.Elem =
wenzelm@44361:     XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))
wenzelm@44361: 
wenzelm@34011:   def hidden(txt: String): XML.Elem =
wenzelm@34011:     span(Markup.HIDDEN, List(XML.Text(txt)))
wenzelm@34011: 
wenzelm@34011:   def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
wenzelm@34011:   def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
wenzelm@44334:   def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt)))
wenzelm@34011: 
wenzelm@44532:   def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
wenzelm@38690:   {
wenzelm@38867:     def html_spans(tree: XML.Tree): XML.Body =
wenzelm@38690:       tree match {
wenzelm@44419:         case XML.Elem(m @ Markup(name, props), ts) =>
wenzelm@44419:           val span_class =
wenzelm@44419:             m match { case Markup.Entity(kind, _) => name + "_" + kind case _ => name }
wenzelm@44419:           val html_span = span(span_class, ts.flatMap(html_spans))
wenzelm@44419:           if (original_data) List(XML.Elem(Markup.Data, List(tree, html_span)))
wenzelm@44419:           else List(html_span)
wenzelm@38690:         case XML.Text(txt) =>
wenzelm@38690:           val ts = new ListBuffer[XML.Tree]
wenzelm@38690:           val t = new StringBuilder
wenzelm@38690:           def flush() {
wenzelm@38690:             if (!t.isEmpty) {
wenzelm@38690:               ts += XML.Text(t.toString)
wenzelm@38690:               t.clear
wenzelm@38690:             }
wenzelm@34009:           }
wenzelm@38690:           def add(elem: XML.Tree) {
wenzelm@38690:             flush()
wenzelm@38690:             ts += elem
wenzelm@38690:           }
wenzelm@44550:           val syms = Symbol.iterator(txt)
wenzelm@38690:           while (syms.hasNext) {
wenzelm@38690:             val s1 = syms.next
wenzelm@38690:             def s2() = if (syms.hasNext) syms.next else ""
wenzelm@44330:             if (s1 == "\n") add(XML.elem(BR))
wenzelm@44569:             else if (Symbol.is_bsub_decoded(s1)) t ++= s1  // FIXME
wenzelm@44569:             else if (Symbol.is_esub_decoded(s1)) t ++= s1  // FIXME
wenzelm@44569:             else if (Symbol.is_bsup_decoded(s1)) t ++= s1  // FIXME
wenzelm@44569:             else if (Symbol.is_esup_decoded(s1)) t ++= s1  // FIXME
wenzelm@44569:             else if (Symbol.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
wenzelm@44569:             else if (Symbol.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
wenzelm@44569:             else if (Symbol.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) }
wenzelm@44569:             else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) }
wenzelm@44330:             else t ++= s1
wenzelm@38690:           }
wenzelm@34011:           flush()
wenzelm@38690:           ts.toList
wenzelm@38690:       }
wenzelm@38690:     html_spans(input)
wenzelm@38690:   }
wenzelm@33984: }