author | wenzelm |
Sun, 06 Dec 2009 23:08:43 +0100 | |
changeset 34002 | cbeeef3aebb3 |
parent 34000 | 1fecda948697 |
child 34004 | 30c8746074d0 |
permissions | -rw-r--r-- |
33984 | 1 |
/* Title: Pure/Thy/html.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Basic HTML output. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
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 | 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" |
|
34000
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
20 |
val PRE = "pre" |
33984 | 21 |
val CLASS = "class" |
22 |
||
23 |
||
24 |
// document markup |
|
25 |
||
34002 | 26 |
def span(cls: String, body: List[XML.Tree]): XML.Elem = |
27 |
XML.Elem(SPAN, List((CLASS, cls)), body) |
|
28 |
||
29 |
def hidden(txt: String): XML.Elem = |
|
30 |
span(Markup.HIDDEN, List(XML.Text(txt))) |
|
31 |
||
32 |
def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt))) |
|
33 |
def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt))) |
|
34 |
||
33984 | 35 |
def spans(tree: XML.Tree): List[XML.Tree] = |
36 |
tree match { |
|
34002 | 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 | 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 | 46 |
} |
34002 | 47 |
def add(elem: XML.Tree) { |
48 |
flush() |
|
49 |
ts + elem |
|
50 |
} |
|
51 |
val syms = Symbol.elements(txt) |
|
52 |
while (syms.hasNext) { |
|
53 |
val s1 = syms.next |
|
54 |
lazy val s2 = if (syms.hasNext) syms.next else "" |
|
55 |
s1 match { |
|
56 |
case "\n" => add(XML.elem(BR)) |
|
57 |
case "\\<^bsub>" => t ++ s1 // FIXME |
|
58 |
case "\\<^esub>" => t ++ s1 // FIXME |
|
59 |
case "\\<^bsup>" => t ++ s1 // FIXME |
|
60 |
case "\\<^esup>" => t ++ s1 // FIXME |
|
61 |
case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2)) |
|
62 |
case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2)) |
|
63 |
case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2)))) |
|
64 |
case "\\<^loc>" => add(hidden(s2)); add(span("loc", List(XML.Text(s2)))) |
|
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 | 68 |
flush() |
34000
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
69 |
ts.toList |
33984 | 70 |
} |
71 |
} |