src/Pure/Thy/html.scala
author wenzelm
Tue, 30 Mar 2010 00:47:52 +0200
changeset 36016 4f5c7a19ebe0
parent 36012 0614676f14d4
child 37200 0f3edc64356a
permissions -rw-r--r--
recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Thy/html.scala
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
     3
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
     4
Basic HTML output.
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
     5
*/
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
     6
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
     7
package isabelle
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
     8
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
     9
import scala.collection.mutable.ListBuffer
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    10
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    11
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    12
object HTML
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    13
{
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    14
  // common elements and attributes
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    15
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    16
  val BODY = "body"
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    17
  val DIV = "div"
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    18
  val SPAN = "span"
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    19
  val BR = "br"
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    20
  val PRE = "pre"
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    21
  val CLASS = "class"
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    22
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    23
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    24
  // document markup
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    25
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    26
  def span(cls: String, body: List[XML.Tree]): XML.Elem =
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    27
    XML.Elem(SPAN, List((CLASS, cls)), body)
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    28
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    29
  def hidden(txt: String): XML.Elem =
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    30
    span(Markup.HIDDEN, List(XML.Text(txt)))
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    31
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    32
  def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    33
  def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    34
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    35
  def spans(tree: XML.Tree): List[XML.Tree] =
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    36
    tree match {
34046
8e743ca417b9 sealed XML.Tree;
wenzelm
parents: 34006
diff changeset
    37
      case XML.Elem(name, _, ts) =>
8e743ca417b9 sealed XML.Tree;
wenzelm
parents: 34006
diff changeset
    38
        List(XML.elem(Markup.DATA, List(tree, span(name, ts.flatMap(spans)))))
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    39
      case XML.Text(txt) =>
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    40
        val ts = new ListBuffer[XML.Tree]
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    41
        val t = new StringBuilder
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    42
        def flush() {
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    43
          if (!t.isEmpty) {
36012
0614676f14d4 replaced some deprecated methods;
wenzelm
parents: 36011
diff changeset
    44
            ts += XML.Text(t.toString)
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    45
            t.clear
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    46
          }
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    47
        }
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    48
        def add(elem: XML.Tree) {
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    49
          flush()
36012
0614676f14d4 replaced some deprecated methods;
wenzelm
parents: 36011
diff changeset
    50
          ts += elem
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    51
        }
36011
3ff725ac13a4 adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents: 34137
diff changeset
    52
        val syms = Symbol.iterator(txt).map(_.toString)
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    53
        while (syms.hasNext) {
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    54
          val s1 = syms.next
34006
bbd146caa6b2 avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents: 34004
diff changeset
    55
          def s2() = if (syms.hasNext) syms.next else ""
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    56
          s1 match {
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    57
            case "\n" => add(XML.elem(BR))
36016
4f5c7a19ebe0 recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents: 36012
diff changeset
    58
            case "\\<^bsub>" => t ++= s1  // FIXME
4f5c7a19ebe0 recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents: 36012
diff changeset
    59
            case "\\<^esub>" => t ++= s1  // FIXME
4f5c7a19ebe0 recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents: 36012
diff changeset
    60
            case "\\<^bsup>" => t ++= s1  // FIXME
4f5c7a19ebe0 recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents: 36012
diff changeset
    61
            case "\\<^esup>" => t ++= s1  // FIXME
34006
bbd146caa6b2 avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents: 34004
diff changeset
    62
            case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
bbd146caa6b2 avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents: 34004
diff changeset
    63
            case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
bbd146caa6b2 avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents: 34004
diff changeset
    64
            case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
bbd146caa6b2 avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents: 34004
diff changeset
    65
            case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
36016
4f5c7a19ebe0 recovered StringBuilder functionality after subtle change of + and ++ in Scala 2.8.0 Beta 1;
wenzelm
parents: 36012
diff changeset
    66
            case _ => t ++= s1
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    67
          }
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    68
        }
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    69
        flush()
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    70
        ts.toList
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    71
    }
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    72
}