src/Pure/Thy/html.scala
author wenzelm
Mon, 07 Dec 2009 00:02:54 +0100
changeset 34006 bbd146caa6b2
parent 34004 30c8746074d0
child 34046 8e743ca417b9
permissions -rw-r--r--
avoid lazy val with side-effects -- spurious null pointers!?
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 {
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    37
      case XML.Elem(name, _, ts) => List(span(name, ts.flatMap(spans)))
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    38
      case XML.Text(txt) =>
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    39
        val ts = new ListBuffer[XML.Tree]
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    40
        val t = new StringBuilder
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    41
        def flush() {
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    42
          if (!t.isEmpty) {
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    43
            ts + XML.Text(t.toString)
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    44
            t.clear
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    45
          }
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    46
        }
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    47
        def add(elem: XML.Tree) {
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    48
          flush()
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    49
          ts + elem
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    50
        }
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    51
        val syms = Symbol.elements(txt)
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    52
        while (syms.hasNext) {
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    53
          val s1 = syms.next
34006
bbd146caa6b2 avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents: 34004
diff changeset
    54
          def s2() = if (syms.hasNext) syms.next else ""
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    55
          s1 match {
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    56
            case "\n" => add(XML.elem(BR))
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    57
            case "\\<^bsub>" => t ++ s1  // FIXME
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    58
            case "\\<^esub>" => t ++ s1  // FIXME
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    59
            case "\\<^bsup>" => t ++ s1  // FIXME
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    60
            case "\\<^esup>" => t ++ s1  // FIXME
34006
bbd146caa6b2 avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents: 34004
diff changeset
    61
            case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2()))
bbd146caa6b2 avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents: 34004
diff changeset
    62
            case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2()))
bbd146caa6b2 avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents: 34004
diff changeset
    63
            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
    64
            case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2()))))
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    65
            case _ => t ++ s1
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    66
          }
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    67
        }
34002
cbeeef3aebb3 basic treatment of special control symbols;
wenzelm
parents: 34000
diff changeset
    68
        flush()
34000
1fecda948697 more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents: 33984
diff changeset
    69
        ts.toList
33984
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    70
    }
c54498f88a77 Basic HTML output.
wenzelm
parents:
diff changeset
    71
}