wenzelm@33984
|
1 |
/* Title: Pure/Thy/html.scala
|
wenzelm@33984
|
2 |
Author: Makarius
|
wenzelm@33984
|
3 |
|
wenzelm@33984
|
4 |
Basic HTML output.
|
wenzelm@33984
|
5 |
*/
|
wenzelm@33984
|
6 |
|
wenzelm@33984
|
7 |
package isabelle
|
wenzelm@33984
|
8 |
|
wenzelm@34009
|
9 |
import scala.collection.mutable.ListBuffer
|
wenzelm@34009
|
10 |
|
wenzelm@34009
|
11 |
|
wenzelm@33984
|
12 |
object HTML
|
wenzelm@33984
|
13 |
{
|
wenzelm@37201
|
14 |
// encode text
|
wenzelm@37201
|
15 |
|
wenzelm@37201
|
16 |
def encode(text: String): String =
|
wenzelm@37201
|
17 |
{
|
wenzelm@37201
|
18 |
val s = new StringBuilder
|
wenzelm@37201
|
19 |
for (c <- text.iterator) c match {
|
wenzelm@37201
|
20 |
case '<' => s ++= "<"
|
wenzelm@37201
|
21 |
case '>' => s ++= ">"
|
wenzelm@37201
|
22 |
case '&' => s ++= "&"
|
wenzelm@37201
|
23 |
case '"' => s ++= """
|
wenzelm@37201
|
24 |
case '\'' => s ++= "'"
|
wenzelm@37201
|
25 |
case '\n' => s ++= "<br/>"
|
wenzelm@37201
|
26 |
case _ => s += c
|
wenzelm@37201
|
27 |
}
|
wenzelm@37201
|
28 |
s.toString
|
wenzelm@37201
|
29 |
}
|
wenzelm@37201
|
30 |
|
wenzelm@37201
|
31 |
|
wenzelm@33984
|
32 |
// common elements and attributes
|
wenzelm@33984
|
33 |
|
wenzelm@33984
|
34 |
val BODY = "body"
|
wenzelm@33984
|
35 |
val DIV = "div"
|
wenzelm@33984
|
36 |
val SPAN = "span"
|
wenzelm@33984
|
37 |
val BR = "br"
|
wenzelm@34009
|
38 |
val PRE = "pre"
|
wenzelm@33984
|
39 |
val CLASS = "class"
|
wenzelm@44361
|
40 |
val STYLE = "style"
|
wenzelm@33984
|
41 |
|
wenzelm@33984
|
42 |
|
wenzelm@33984
|
43 |
// document markup
|
wenzelm@33984
|
44 |
|
wenzelm@38867
|
45 |
def span(cls: String, body: XML.Body): XML.Elem =
|
wenzelm@38486
|
46 |
XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
|
wenzelm@34011
|
47 |
|
wenzelm@44361
|
48 |
def user_font(font: String, txt: String): XML.Elem =
|
wenzelm@44361
|
49 |
XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))
|
wenzelm@44361
|
50 |
|
wenzelm@34011
|
51 |
def hidden(txt: String): XML.Elem =
|
wenzelm@34011
|
52 |
span(Markup.HIDDEN, List(XML.Text(txt)))
|
wenzelm@34011
|
53 |
|
wenzelm@34011
|
54 |
def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
|
wenzelm@34011
|
55 |
def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
|
wenzelm@44334
|
56 |
def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt)))
|
wenzelm@34011
|
57 |
|
wenzelm@44532
|
58 |
def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
|
wenzelm@38690
|
59 |
{
|
wenzelm@44532
|
60 |
val symbols = Isabelle_System.symbols
|
wenzelm@44532
|
61 |
|
wenzelm@38867
|
62 |
def html_spans(tree: XML.Tree): XML.Body =
|
wenzelm@38690
|
63 |
tree match {
|
wenzelm@44419
|
64 |
case XML.Elem(m @ Markup(name, props), ts) =>
|
wenzelm@44419
|
65 |
val span_class =
|
wenzelm@44419
|
66 |
m match { case Markup.Entity(kind, _) => name + "_" + kind case _ => name }
|
wenzelm@44419
|
67 |
val html_span = span(span_class, ts.flatMap(html_spans))
|
wenzelm@44419
|
68 |
if (original_data) List(XML.Elem(Markup.Data, List(tree, html_span)))
|
wenzelm@44419
|
69 |
else List(html_span)
|
wenzelm@38690
|
70 |
case XML.Text(txt) =>
|
wenzelm@38690
|
71 |
val ts = new ListBuffer[XML.Tree]
|
wenzelm@38690
|
72 |
val t = new StringBuilder
|
wenzelm@38690
|
73 |
def flush() {
|
wenzelm@38690
|
74 |
if (!t.isEmpty) {
|
wenzelm@38690
|
75 |
ts += XML.Text(t.toString)
|
wenzelm@38690
|
76 |
t.clear
|
wenzelm@38690
|
77 |
}
|
wenzelm@34009
|
78 |
}
|
wenzelm@38690
|
79 |
def add(elem: XML.Tree) {
|
wenzelm@38690
|
80 |
flush()
|
wenzelm@38690
|
81 |
ts += elem
|
wenzelm@38690
|
82 |
}
|
wenzelm@44360
|
83 |
val syms = Symbol.iterator_string(txt)
|
wenzelm@38690
|
84 |
while (syms.hasNext) {
|
wenzelm@38690
|
85 |
val s1 = syms.next
|
wenzelm@38690
|
86 |
def s2() = if (syms.hasNext) syms.next else ""
|
wenzelm@44330
|
87 |
if (s1 == "\n") add(XML.elem(BR))
|
wenzelm@44382
|
88 |
else if (s1 == symbols.bsub_decoded) t ++= s1 // FIXME
|
wenzelm@44382
|
89 |
else if (s1 == symbols.esub_decoded) t ++= s1 // FIXME
|
wenzelm@44382
|
90 |
else if (s1 == symbols.bsup_decoded) t ++= s1 // FIXME
|
wenzelm@44382
|
91 |
else if (s1 == symbols.esup_decoded) t ++= s1 // FIXME
|
wenzelm@44334
|
92 |
else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
|
wenzelm@44334
|
93 |
else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
|
wenzelm@44382
|
94 |
else if (s1 == symbols.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
|
wenzelm@44361
|
95 |
else if (symbols.fonts.isDefinedAt(s1)) { add(user_font(symbols.fonts(s1), s1)) }
|
wenzelm@44330
|
96 |
else t ++= s1
|
wenzelm@38690
|
97 |
}
|
wenzelm@34011
|
98 |
flush()
|
wenzelm@38690
|
99 |
ts.toList
|
wenzelm@38690
|
100 |
}
|
wenzelm@38690
|
101 |
html_spans(input)
|
wenzelm@38690
|
102 |
}
|
wenzelm@33984
|
103 |
}
|