author | wenzelm |
Wed, 11 Aug 2010 00:42:40 +0200 | |
changeset 38269 | cd6906d9199f |
parent 38267 | e50c283dd125 |
child 38355 | 8cb265fb12fe |
permissions | -rw-r--r-- |
38267
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/General/xml_data.scala |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
3 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
4 |
XML as basic data representation language. |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
5 |
*/ |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
6 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
8 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
9 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
10 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
11 |
object XML_Data |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
12 |
{ |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
13 |
/* basic values */ |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
14 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
15 |
class XML_Atom(s: String) extends Exception(s) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
16 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
17 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
18 |
private def make_int_atom(i: Int): String = i.toString |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
19 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
20 |
private def dest_int_atom(s: String): Int = |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
21 |
try { Integer.parseInt(s) } |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
22 |
catch { case e: NumberFormatException => throw new XML_Atom(s) } |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
23 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
24 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
25 |
private def make_bool_atom(b: Boolean): String = if (b) "1" else "0" |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
26 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
27 |
private def dest_bool_atom(s: String): Boolean = |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
28 |
if (s == "1") true |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
29 |
else if (s == "0") false |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
30 |
else throw new XML_Atom(s) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
31 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
32 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
33 |
private def make_unit_atom(u: Unit) = "" |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
34 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
35 |
private def dest_unit_atom(s: String): Unit = |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
36 |
if (s == "") () else throw new XML_Atom(s) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
37 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
38 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
39 |
/* structural nodes */ |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
40 |
|
38269 | 41 |
class XML_Body(body: XML.Body) extends Exception |
38267
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
42 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
43 |
private def make_node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
44 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
45 |
private def dest_node(t: XML.Tree): XML.Body = |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
46 |
t match { |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
47 |
case XML.Elem(Markup(":", Nil), ts) => ts |
38269 | 48 |
case _ => throw new XML_Body(List(t)) |
38267
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
49 |
} |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
50 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
51 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
52 |
/* representation of standard types */ |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
53 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
54 |
def make_properties(props: List[(String, String)]): XML.Body = |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
55 |
List(XML.Elem(Markup(":", props), Nil)) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
56 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
57 |
def dest_properties(ts: XML.Body): List[(String, String)] = |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
58 |
ts match { |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
59 |
case List(XML.Elem(Markup(":", props), Nil)) => props |
38269 | 60 |
case _ => throw new XML_Body(ts) |
38267
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
61 |
} |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
62 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
63 |
|
38269 | 64 |
def make_string(s: String): XML.Body = if (s.isEmpty) Nil else List(XML.Text(s)) |
38267
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
65 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
66 |
def dest_string(ts: XML.Body): String = |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
67 |
ts match { |
38269 | 68 |
case Nil => "" |
38267
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
69 |
case List(XML.Text(s)) => s |
38269 | 70 |
case _ => throw new XML_Body(ts) |
38267
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
71 |
} |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
72 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
73 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
74 |
def make_int(i: Int): XML.Body = make_string(make_int_atom(i)) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
75 |
def dest_int(ts: XML.Body): Int = dest_int_atom(dest_string(ts)) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
76 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
77 |
def make_bool(b: Boolean): XML.Body = make_string(make_bool_atom(b)) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
78 |
def dest_bool(ts: XML.Body) = dest_bool_atom(dest_string(ts)) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
79 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
80 |
def make_unit(u: Unit): XML.Body = make_string(make_unit_atom(u)) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
81 |
def dest_unit(ts: XML.Body): Unit = dest_unit_atom(dest_string(ts)) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
82 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
83 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
84 |
def make_pair[A, B](make1: A => XML.Body)(make2: B => XML.Body)(p: (A, B)): XML.Body = |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
85 |
List(make_node(make1(p._1)), make_node(make2(p._2))) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
86 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
87 |
def dest_pair[A, B](dest1: XML.Body => A)(dest2: XML.Body => B)(ts: XML.Body): (A, B) = |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
88 |
ts match { |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
89 |
case List(t1, t2) => (dest1(dest_node(t1)), dest2(dest_node(t2))) |
38269 | 90 |
case _ => throw new XML_Body(ts) |
38267
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
91 |
} |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
92 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
93 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
94 |
def make_triple[A, B, C](make1: A => XML.Body)(make2: B => XML.Body)(make3: C => XML.Body) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
95 |
(p: (A, B, C)): XML.Body = |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
96 |
List(make_node(make1(p._1)), make_node(make2(p._2)), make_node(make3(p._3))) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
97 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
98 |
def dest_triple[A, B, C](dest1: XML.Body => A)(dest2: XML.Body => B)(dest3: XML.Body => C) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
99 |
(ts: XML.Body): (A, B, C) = |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
100 |
ts match { |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
101 |
case List(t1, t2, t3) => (dest1(dest_node(t1)), dest2(dest_node(t2)), dest3(dest_node(t3))) |
38269 | 102 |
case _ => throw new XML_Body(ts) |
38267
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
103 |
} |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
104 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
105 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
106 |
def make_list[A](make: A => XML.Body)(xs: List[A]): XML.Body = |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
107 |
xs.map((x: A) => make_node(make(x))) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
108 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
109 |
def dest_list[A](dest: XML.Body => A)(ts: XML.Body): List[A] = |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
110 |
ts.map((t: XML.Tree) => dest(dest_node(t))) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
111 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
112 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
113 |
def make_option[A](make: A => XML.Body)(opt: Option[A]): XML.Body = |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
114 |
opt match { |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
115 |
case None => make_list(make)(Nil) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
116 |
case Some(x) => make_list(make)(List(x)) |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
117 |
} |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
118 |
|
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
119 |
def dest_option[A](dest: XML.Body => A)(ts: XML.Body): Option[A] = |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
120 |
dest_list(dest)(ts) match { |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
121 |
case Nil => None |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
122 |
case List(x) => Some(x) |
38269 | 123 |
case _ => throw new XML_Body(ts) |
38267
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
124 |
} |
e50c283dd125
type XML.Body as basic data representation language (Scala version);
wenzelm
parents:
diff
changeset
|
125 |
} |