src/Pure/Thy/html.scala
author wenzelm
Sun Dec 06 22:23:31 2009 +0100 (2009-12-06 ago)
changeset 34000 1fecda948697
parent 33984 c54498f88a77
child 34002 cbeeef3aebb3
permissions -rw-r--r--
more robust treatment of line breaks -- Java "split" has off semantics;
     1 /*  Title:      Pure/Thy/html.scala
     2     Author:     Makarius
     3 
     4 Basic HTML output.
     5 */
     6 
     7 package isabelle
     8 
     9 import scala.collection.mutable.ListBuffer
    10 
    11 
    12 object HTML
    13 {
    14   // common elements and attributes
    15 
    16   val BODY = "body"
    17   val DIV = "div"
    18   val SPAN = "span"
    19   val BR = "br"
    20   val PRE = "pre"
    21   val CLASS = "class"
    22 
    23 
    24   // document markup
    25 
    26   def spans(tree: XML.Tree): List[XML.Tree] =
    27     tree match {
    28       case XML.Elem(name, _, ts) =>
    29         List(XML.Elem(SPAN, List((CLASS, name)), ts.flatMap(spans)))
    30       case XML.Text(txt) =>
    31         val ts = new ListBuffer[XML.Tree]
    32         val t = new StringBuilder
    33         def flush_text() {
    34           if (!t.isEmpty) {
    35             ts + XML.Text(t.toString)
    36             t.clear
    37           }
    38         }
    39         for (sym <- Symbol.elements(txt)) {
    40           sym match {
    41             case "\n" =>
    42               flush_text()
    43               ts + XML.elem(BR)
    44             case _ =>
    45               t ++ sym.toString
    46           }
    47         }
    48         flush_text()
    49         ts.toList
    50     }
    51 }