author | wenzelm |
Sun, 06 Dec 2009 22:23:31 +0100 | |
changeset 34000 | 1fecda948697 |
parent 33984 | c54498f88a77 |
child 34002 | cbeeef3aebb3 |
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 |
||
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))) |
|
34000
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
30 |
case XML.Text(txt) => |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
31 |
val ts = new ListBuffer[XML.Tree] |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
32 |
val t = new StringBuilder |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
33 |
def flush_text() { |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
34 |
if (!t.isEmpty) { |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
35 |
ts + XML.Text(t.toString) |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
36 |
t.clear |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
37 |
} |
33984 | 38 |
} |
34000
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
39 |
for (sym <- Symbol.elements(txt)) { |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
40 |
sym match { |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
41 |
case "\n" => |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
42 |
flush_text() |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
43 |
ts + XML.elem(BR) |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
44 |
case _ => |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
45 |
t ++ sym.toString |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
46 |
} |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
47 |
} |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
48 |
flush_text() |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
49 |
ts.toList |
33984 | 50 |
} |
51 |
} |