author | wenzelm |
Tue, 05 Jul 2011 23:18:14 +0200 | |
changeset 43675 | 8252d51d70e2 |
parent 43661 | 39fdbd814c7f |
child 43695 | 5130dfe1b7be |
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" |
43490 | 40 |
val STYLE = "style" |
33984 | 41 |
|
42 |
||
43 |
// document markup |
|
44 |
||
38573 | 45 |
def span(cls: String, body: XML.Body): XML.Elem = |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37200
diff
changeset
|
46 |
XML.Elem(Markup(SPAN, List((CLASS, cls))), body) |
34002 | 47 |
|
43490 | 48 |
def user_font(font: String, txt: String): XML.Elem = |
49 |
XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt))) |
|
50 |
||
34002 | 51 |
def hidden(txt: String): XML.Elem = |
52 |
span(Markup.HIDDEN, List(XML.Text(txt))) |
|
53 |
||
54 |
def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt))) |
|
55 |
def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt))) |
|
43459 | 56 |
def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt))) |
34002 | 57 |
|
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43548
diff
changeset
|
58 |
def spans(input: XML.Tree, original_data: Boolean = false): XML.Body = |
38444
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
59 |
{ |
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43548
diff
changeset
|
60 |
val symbols = Isabelle_System.symbols |
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43548
diff
changeset
|
61 |
|
38573 | 62 |
def html_spans(tree: XML.Tree): XML.Body = |
38444
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
63 |
tree match { |
43548
f231a7594e54
type classes: entity markup instead of old-style token markup;
wenzelm
parents:
43511
diff
changeset
|
64 |
case XML.Elem(m @ Markup(name, props), ts) => |
f231a7594e54
type classes: entity markup instead of old-style token markup;
wenzelm
parents:
43511
diff
changeset
|
65 |
val span_class = |
f231a7594e54
type classes: entity markup instead of old-style token markup;
wenzelm
parents:
43511
diff
changeset
|
66 |
m match { case Markup.Entity(kind, _) => name + "_" + kind case _ => name } |
f231a7594e54
type classes: entity markup instead of old-style token markup;
wenzelm
parents:
43511
diff
changeset
|
67 |
val html_span = span(span_class, ts.flatMap(html_spans)) |
f231a7594e54
type classes: entity markup instead of old-style token markup;
wenzelm
parents:
43511
diff
changeset
|
68 |
if (original_data) List(XML.Elem(Markup.Data, List(tree, html_span))) |
f231a7594e54
type classes: entity markup instead of old-style token markup;
wenzelm
parents:
43511
diff
changeset
|
69 |
else List(html_span) |
38444
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
70 |
case XML.Text(txt) => |
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
71 |
val ts = new ListBuffer[XML.Tree] |
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
72 |
val t = new StringBuilder |
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
73 |
def flush() { |
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
74 |
if (!t.isEmpty) { |
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
75 |
ts += XML.Text(t.toString) |
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
76 |
t.clear |
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
77 |
} |
34000
1fecda948697
more robust treatment of line breaks -- Java "split" has off semantics;
wenzelm
parents:
33984
diff
changeset
|
78 |
} |
38444
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
79 |
def add(elem: XML.Tree) { |
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
80 |
flush() |
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
81 |
ts += elem |
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
82 |
} |
43675
8252d51d70e2
simplified Symbol.iterator: produce strings, which are mostly preallocated;
wenzelm
parents:
43661
diff
changeset
|
83 |
val syms = Symbol.iterator(txt) |
38444
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
84 |
while (syms.hasNext) { |
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
85 |
val s1 = syms.next |
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
86 |
def s2() = if (syms.hasNext) syms.next else "" |
43455 | 87 |
if (s1 == "\n") add(XML.elem(BR)) |
43511 | 88 |
else if (s1 == symbols.bsub_decoded) t ++= s1 // FIXME |
89 |
else if (s1 == symbols.esub_decoded) t ++= s1 // FIXME |
|
90 |
else if (s1 == symbols.bsup_decoded) t ++= s1 // FIXME |
|
91 |
else if (s1 == symbols.esup_decoded) t ++= s1 // FIXME |
|
43459 | 92 |
else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) } |
93 |
else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) } |
|
43511 | 94 |
else if (s1 == symbols.bold_decoded) { add(hidden(s1)); add(bold(s2())) } |
43490 | 95 |
else if (symbols.fonts.isDefinedAt(s1)) { add(user_font(symbols.fonts(s1), s1)) } |
43455 | 96 |
else t ++= s1 |
38444
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
97 |
} |
34002 | 98 |
flush() |
38444
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
99 |
ts.toList |
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
100 |
} |
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
101 |
html_spans(input) |
796904799f4d
HTML.spans: explicit flag for preservation of original data (which would be turned into org.w3c.dom user data in XML.document_node);
wenzelm
parents:
38231
diff
changeset
|
102 |
} |
33984 | 103 |
} |