author | wenzelm |
Sun, 30 May 2010 23:40:24 +0200 | |
changeset 37200 | 0f3edc64356a |
parent 36016 | 4f5c7a19ebe0 |
child 38230 | ed147003de4b |
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 |
{ |
|
37200
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
14 |
// encode text |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
15 |
|
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
16 |
def encode(text: String): String = |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
17 |
{ |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
18 |
val s = new StringBuilder |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
19 |
for (c <- text.iterator) c match { |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
20 |
case '<' => s ++= "<" |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
21 |
case '>' => s ++= ">" |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
22 |
case '&' => s ++= "&" |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
23 |
case '"' => s ++= """ |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
24 |
case '\'' => s ++= "'" |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
25 |
case '\n' => s ++= "<br/>" |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
26 |
case _ => s += c |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
27 |
} |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
28 |
s.toString |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
29 |
} |
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
30 |
|
0f3edc64356a
added HTML.encode (in Scala), similar to HTML.output in ML;
wenzelm
parents:
36016
diff
changeset
|
31 |
|
33984 | 32 |
// common elements and attributes |
33 |
||
34 |
val BODY = "body" |
|
35 |
val DIV = "div" |
|
36 |
val SPAN = "span" |
|
37 |
val BR = "br" |
|
34000
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
38 |
val PRE = "pre" |
33984 | 39 |
val CLASS = "class" |
40 |
||
41 |
||
42 |
// document markup |
|
43 |
||
34002 | 44 |
def span(cls: String, body: List[XML.Tree]): XML.Elem = |
45 |
XML.Elem(SPAN, List((CLASS, cls)), body) |
|
46 |
||
47 |
def hidden(txt: String): XML.Elem = |
|
48 |
span(Markup.HIDDEN, List(XML.Text(txt))) |
|
49 |
||
50 |
def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt))) |
|
51 |
def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt))) |
|
52 |
||
33984 | 53 |
def spans(tree: XML.Tree): List[XML.Tree] = |
54 |
tree match { |
|
34046 | 55 |
case XML.Elem(name, _, ts) => |
56 |
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
|
57 |
case XML.Text(txt) => |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
58 |
val ts = new ListBuffer[XML.Tree] |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
59 |
val t = new StringBuilder |
34002 | 60 |
def flush() { |
34000
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
61 |
if (!t.isEmpty) { |
36012 | 62 |
ts += XML.Text(t.toString) |
34000
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
63 |
t.clear |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
64 |
} |
33984 | 65 |
} |
34002 | 66 |
def add(elem: XML.Tree) { |
67 |
flush() |
|
36012 | 68 |
ts += elem |
34002 | 69 |
} |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34137
diff
changeset
|
70 |
val syms = Symbol.iterator(txt).map(_.toString) |
34002 | 71 |
while (syms.hasNext) { |
72 |
val s1 = syms.next |
|
34006
bbd146caa6b2
avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents:
34004
diff
changeset
|
73 |
def s2() = if (syms.hasNext) syms.next else "" |
34002 | 74 |
s1 match { |
75 |
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
|
76 |
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
|
77 |
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
|
78 |
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
|
79 |
case "\\<^esup>" => t ++= s1 // FIXME |
34006
bbd146caa6b2
avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents:
34004
diff
changeset
|
80 |
case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2())) |
bbd146caa6b2
avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents:
34004
diff
changeset
|
81 |
case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2())) |
bbd146caa6b2
avoid lazy val with side-effects -- spurious null pointers!?
wenzelm
parents:
34004
diff
changeset
|
82 |
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
|
83 |
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
|
84 |
case _ => t ++= s1 |
34000
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
85 |
} |
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
86 |
} |
34002 | 87 |
flush() |
34000
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
88 |
ts.toList |
33984 | 89 |
} |
90 |
} |