author  wenzelm 
Sat, 07 Aug 2010 22:43:57 +0200  
changeset 38231  968844caaff9 
parent 38230  ed147003de4b 
child 38444  796904799f4d 
permissions  rwrr 
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 = 
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37200
diff
changeset

45 
XML.Elem(Markup(SPAN, List((CLASS, cls))), body) 
34002  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 { 

38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37200
diff
changeset

55 
case XML.Elem(Markup(name, _), ts) => 
38231  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 sideeffects  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 sideeffects  spurious null pointers!?
wenzelm
parents:
34004
diff
changeset

80 
case "\\<^sub>"  "\\<^isub>" => add(hidden(s1)); add(sub(s2())) 
bbd146caa6b2
avoid lazy val with sideeffects  spurious null pointers!?
wenzelm
parents:
34004
diff
changeset

81 
case "\\<^sup>"  "\\<^isup>" => add(hidden(s1)); add(sup(s2())) 
bbd146caa6b2
avoid lazy val with sideeffects  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 sideeffects  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 
} 