--- a/src/Pure/General/xml.ML Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/General/xml.ML Tue Jul 12 10:44:30 2011 +0200
@@ -4,6 +4,21 @@
Simple XML tree values.
*)
+signature XML_DATA_OPS =
+sig
+ type 'a T
+ val properties: Properties.T T
+ val string: string T
+ val int: int T
+ val bool: bool T
+ val unit: unit T
+ val pair: 'a T -> 'b T -> ('a * 'b) T
+ val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
+ val list: 'a T -> 'a list T
+ val option: 'a T -> 'a option T
+ val variant: 'a T list -> 'a T
+end;
+
signature XML =
sig
type attributes = Properties.T
@@ -24,6 +39,10 @@
val parse_element: string list -> tree * string list
val parse_document: string list -> tree * string list
val parse: string -> tree
+ exception XML_ATOM of string
+ exception XML_BODY of body
+ structure Encode: XML_DATA_OPS where type 'a T = 'a -> body
+ structure Decode: XML_DATA_OPS where type 'a T = body -> 'a
end;
structure XML: XML =
@@ -190,4 +209,124 @@
end;
+
+
+(** XML as data representation language **)
+
+exception XML_ATOM of string;
+exception XML_BODY of tree list;
+
+
+structure Encode =
+struct
+
+type 'a T = 'a -> body;
+
+
+(* basic values *)
+
+fun int_atom i = signed_string_of_int i;
+
+fun bool_atom false = "0"
+ | bool_atom true = "1";
+
+fun unit_atom () = "";
+
+
+(* structural nodes *)
+
+fun node ts = Elem ((":", []), ts);
+
+fun tagged (tag, ts) = Elem ((int_atom tag, []), ts);
+
+
+(* representation of standard types *)
+
+fun properties props = [Elem ((":", props), [])];
+
+fun string "" = []
+ | string s = [Text s];
+
+val int = string o int_atom;
+
+val bool = string o bool_atom;
+
+val unit = string o unit_atom;
+
+fun pair f g (x, y) = [node (f x), node (g y)];
+
+fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
+
+fun list f xs = map (node o f) xs;
+
+fun option _ NONE = []
+ | option f (SOME x) = [node (f x)];
+
+fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
+
end;
+
+
+structure Decode =
+struct
+
+type 'a T = body -> 'a;
+
+
+(* basic values *)
+
+fun int_atom s =
+ (case Int.fromString s of
+ SOME i => i
+ | NONE => raise XML_ATOM s);
+
+fun bool_atom "0" = false
+ | bool_atom "1" = true
+ | bool_atom s = raise XML_ATOM s;
+
+fun unit_atom "" = ()
+ | unit_atom s = raise XML_ATOM s;
+
+
+(* structural nodes *)
+
+fun node (Elem ((":", []), ts)) = ts
+ | node t = raise XML_BODY [t];
+
+fun tagged (Elem ((s, []), ts)) = (int_atom s, ts)
+ | tagged t = raise XML_BODY [t];
+
+
+(* representation of standard types *)
+
+fun properties [Elem ((":", props), [])] = props
+ | properties ts = raise XML_BODY ts;
+
+fun string [] = ""
+ | string [Text s] = s
+ | string ts = raise XML_BODY ts;
+
+val int = int_atom o string;
+
+val bool = bool_atom o string;
+
+val unit = unit_atom o string;
+
+fun pair f g [t1, t2] = (f (node t1), g (node t2))
+ | pair _ _ ts = raise XML_BODY ts;
+
+fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
+ | triple _ _ _ ts = raise XML_BODY ts;
+
+fun list f ts = map (f o node) ts;
+
+fun option _ [] = NONE
+ | option f [t] = SOME (f (node t))
+ | option _ ts = raise XML_BODY ts;
+
+fun variant fs [t] = uncurry (nth fs) (tagged t)
+ | variant _ ts = raise XML_BODY ts;
+
+end;
+
+end;
--- a/src/Pure/General/xml.scala Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/General/xml.scala Tue Jul 12 10:44:30 2011 +0200
@@ -16,6 +16,8 @@
object XML
{
+ /** XML trees **/
+
/* datatype representation */
type Attributes = List[(String, String)]
@@ -174,7 +176,8 @@
}
- /* document object model (W3C DOM) */
+
+ /** document object model (W3C DOM) **/
def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
node.getUserData(Markup.Data.name) match {
@@ -200,4 +203,166 @@
}
DOM(tree)
}
+
+
+
+ /** XML as data representation language **/
+
+ class XML_Atom(s: String) extends Exception(s)
+ class XML_Body(body: XML.Body) extends Exception
+
+ object Encode
+ {
+ type T[A] = A => XML.Body
+
+
+ /* basic values */
+
+ private def long_atom(i: Long): String = i.toString
+
+ private def int_atom(i: Int): String = i.toString
+
+ private def bool_atom(b: Boolean): String = if (b) "1" else "0"
+
+ private def unit_atom(u: Unit) = ""
+
+
+ /* structural nodes */
+
+ private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
+
+ private def tagged(tag: Int, ts: XML.Body): XML.Tree =
+ XML.Elem(Markup(int_atom(tag), Nil), ts)
+
+
+ /* representation of standard types */
+
+ val properties: T[List[(String, String)]] =
+ (props => List(XML.Elem(Markup(":", props), Nil)))
+
+ val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
+
+ val long: T[Long] = (x => string(long_atom(x)))
+
+ val int: T[Int] = (x => string(int_atom(x)))
+
+ val bool: T[Boolean] = (x => string(bool_atom(x)))
+
+ val unit: T[Unit] = (x => string(unit_atom(x)))
+
+ def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
+ (x => List(node(f(x._1)), node(g(x._2))))
+
+ def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
+ (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
+
+ def list[A](f: T[A]): T[List[A]] =
+ (xs => xs.map((x: A) => node(f(x))))
+
+ def option[A](f: T[A]): T[Option[A]] =
+ {
+ case None => Nil
+ case Some(x) => List(node(f(x)))
+ }
+
+ def variant[A](fs: List[PartialFunction[A, XML.Body]]): T[A] =
+ {
+ case x =>
+ val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
+ List(tagged(tag, f(x)))
+ }
+ }
+
+ object Decode
+ {
+ type T[A] = XML.Body => A
+
+
+ /* basic values */
+
+ private def long_atom(s: String): Long =
+ try { java.lang.Long.parseLong(s) }
+ catch { case e: NumberFormatException => throw new XML_Atom(s) }
+
+ private def int_atom(s: String): Int =
+ try { Integer.parseInt(s) }
+ catch { case e: NumberFormatException => throw new XML_Atom(s) }
+
+ private def bool_atom(s: String): Boolean =
+ if (s == "1") true
+ else if (s == "0") false
+ else throw new XML_Atom(s)
+
+ private def unit_atom(s: String): Unit =
+ if (s == "") () else throw new XML_Atom(s)
+
+
+ /* structural nodes */
+
+ private def node(t: XML.Tree): XML.Body =
+ t match {
+ case XML.Elem(Markup(":", Nil), ts) => ts
+ case _ => throw new XML_Body(List(t))
+ }
+
+ private def tagged(t: XML.Tree): (Int, XML.Body) =
+ t match {
+ case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
+ case _ => throw new XML_Body(List(t))
+ }
+
+
+ /* representation of standard types */
+
+ val properties: T[List[(String, String)]] =
+ {
+ case List(XML.Elem(Markup(":", props), Nil)) => props
+ case ts => throw new XML_Body(ts)
+ }
+
+ val string: T[String] =
+ {
+ case Nil => ""
+ case List(XML.Text(s)) => s
+ case ts => throw new XML_Body(ts)
+ }
+
+ val long: T[Long] = (x => long_atom(string(x)))
+
+ val int: T[Int] = (x => int_atom(string(x)))
+
+ val bool: T[Boolean] = (x => bool_atom(string(x)))
+
+ val unit: T[Unit] = (x => unit_atom(string(x)))
+
+ def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
+ {
+ case List(t1, t2) => (f(node(t1)), g(node(t2)))
+ case ts => throw new XML_Body(ts)
+ }
+
+ def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
+ {
+ case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
+ case ts => throw new XML_Body(ts)
+ }
+
+ def list[A](f: T[A]): T[List[A]] =
+ (ts => ts.map(t => f(node(t))))
+
+ def option[A](f: T[A]): T[Option[A]] =
+ {
+ case Nil => None
+ case List(t) => Some(f(node(t)))
+ case ts => throw new XML_Body(ts)
+ }
+
+ def variant[A](fs: List[T[A]]): T[A] =
+ {
+ case List(t) =>
+ val (tag, ts) = tagged(t)
+ fs(tag)(ts)
+ case ts => throw new XML_Body(ts)
+ }
+ }
}
--- a/src/Pure/General/xml_data.ML Tue Jul 12 16:00:05 2011 +0900
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,154 +0,0 @@
-(* Title: Pure/General/xml_data.ML
- Author: Makarius
-
-XML as basic data representation language.
-*)
-
-signature XML_DATA_OPS =
-sig
- type 'a T
- val properties: Properties.T T
- val string: string T
- val int: int T
- val bool: bool T
- val unit: unit T
- val pair: 'a T -> 'b T -> ('a * 'b) T
- val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
- val list: 'a T -> 'a list T
- val option: 'a T -> 'a option T
- val variant: 'a T list -> 'a T
-end;
-
-signature XML_DATA =
-sig
- structure Encode: XML_DATA_OPS where type 'a T = 'a -> XML.body
- exception XML_ATOM of string
- exception XML_BODY of XML.body
- structure Decode: XML_DATA_OPS where type 'a T = XML.body -> 'a
-end;
-
-structure XML_Data: XML_DATA =
-struct
-
-(** encode **)
-
-structure Encode =
-struct
-
-type 'a T = 'a -> XML.body;
-
-
-(* basic values *)
-
-fun int_atom i = signed_string_of_int i;
-
-fun bool_atom false = "0"
- | bool_atom true = "1";
-
-fun unit_atom () = "";
-
-
-(* structural nodes *)
-
-fun node ts = XML.Elem ((":", []), ts);
-
-fun tagged (tag, ts) = XML.Elem ((int_atom tag, []), ts);
-
-
-(* representation of standard types *)
-
-fun properties props = [XML.Elem ((":", props), [])];
-
-fun string "" = []
- | string s = [XML.Text s];
-
-val int = string o int_atom;
-
-val bool = string o bool_atom;
-
-val unit = string o unit_atom;
-
-fun pair f g (x, y) = [node (f x), node (g y)];
-
-fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
-
-fun list f xs = map (node o f) xs;
-
-fun option _ NONE = []
- | option f (SOME x) = [node (f x)];
-
-fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
-
-end;
-
-
-
-(** decode **)
-
-exception XML_ATOM of string;
-exception XML_BODY of XML.tree list;
-
-structure Decode =
-struct
-
-type 'a T = XML.body -> 'a;
-
-
-(* basic values *)
-
-fun int_atom s =
- (case Int.fromString s of
- SOME i => i
- | NONE => raise XML_ATOM s);
-
-fun bool_atom "0" = false
- | bool_atom "1" = true
- | bool_atom s = raise XML_ATOM s;
-
-fun unit_atom "" = ()
- | unit_atom s = raise XML_ATOM s;
-
-
-(* structural nodes *)
-
-fun node (XML.Elem ((":", []), ts)) = ts
- | node t = raise XML_BODY [t];
-
-fun tagged (XML.Elem ((s, []), ts)) = (int_atom s, ts)
- | tagged t = raise XML_BODY [t];
-
-
-(* representation of standard types *)
-
-fun properties [XML.Elem ((":", props), [])] = props
- | properties ts = raise XML_BODY ts;
-
-fun string [] = ""
- | string [XML.Text s] = s
- | string ts = raise XML_BODY ts;
-
-val int = int_atom o string;
-
-val bool = bool_atom o string;
-
-val unit = unit_atom o string;
-
-fun pair f g [t1, t2] = (f (node t1), g (node t2))
- | pair _ _ ts = raise XML_BODY ts;
-
-fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
- | triple _ _ _ ts = raise XML_BODY ts;
-
-fun list f ts = map (f o node) ts;
-
-fun option _ [] = NONE
- | option f [t] = SOME (f (node t))
- | option _ ts = raise XML_BODY ts;
-
-fun variant fs [t] = uncurry (nth fs) (tagged t)
- | variant _ ts = raise XML_BODY ts;
-
-end;
-
-end;
-
--- a/src/Pure/General/xml_data.scala Tue Jul 12 16:00:05 2011 +0900
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,176 +0,0 @@
-/* Title: Pure/General/xml_data.scala
- Author: Makarius
-
-XML as basic data representation language.
-*/
-
-package isabelle
-
-
-
-object XML_Data
-{
- /** encode **/
-
- object Encode
- {
- type T[A] = A => XML.Body
-
-
- /* basic values */
-
- private def long_atom(i: Long): String = i.toString
-
- private def int_atom(i: Int): String = i.toString
-
- private def bool_atom(b: Boolean): String = if (b) "1" else "0"
-
- private def unit_atom(u: Unit) = ""
-
-
- /* structural nodes */
-
- private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
-
- private def tagged(tag: Int, ts: XML.Body): XML.Tree =
- XML.Elem(Markup(int_atom(tag), Nil), ts)
-
-
- /* representation of standard types */
-
- val properties: T[List[(String, String)]] =
- (props => List(XML.Elem(Markup(":", props), Nil)))
-
- val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
-
- val long: T[Long] = (x => string(long_atom(x)))
-
- val int: T[Int] = (x => string(int_atom(x)))
-
- val bool: T[Boolean] = (x => string(bool_atom(x)))
-
- val unit: T[Unit] = (x => string(unit_atom(x)))
-
- def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
- (x => List(node(f(x._1)), node(g(x._2))))
-
- def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
- (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
-
- def list[A](f: T[A]): T[List[A]] =
- (xs => xs.map((x: A) => node(f(x))))
-
- def option[A](f: T[A]): T[Option[A]] =
- {
- case None => Nil
- case Some(x) => List(node(f(x)))
- }
-
- def variant[A](fs: List[PartialFunction[A, XML.Body]]): T[A] =
- {
- case x =>
- val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
- List(tagged(tag, f(x)))
- }
- }
-
-
-
- /** decode **/
-
- class XML_Atom(s: String) extends Exception(s)
- class XML_Body(body: XML.Body) extends Exception
-
- object Decode
- {
- type T[A] = XML.Body => A
-
-
- /* basic values */
-
- private def long_atom(s: String): Long =
- try { java.lang.Long.parseLong(s) }
- catch { case e: NumberFormatException => throw new XML_Atom(s) }
-
- private def int_atom(s: String): Int =
- try { Integer.parseInt(s) }
- catch { case e: NumberFormatException => throw new XML_Atom(s) }
-
- private def bool_atom(s: String): Boolean =
- if (s == "1") true
- else if (s == "0") false
- else throw new XML_Atom(s)
-
- private def unit_atom(s: String): Unit =
- if (s == "") () else throw new XML_Atom(s)
-
-
- /* structural nodes */
-
- private def node(t: XML.Tree): XML.Body =
- t match {
- case XML.Elem(Markup(":", Nil), ts) => ts
- case _ => throw new XML_Body(List(t))
- }
-
- private def tagged(t: XML.Tree): (Int, XML.Body) =
- t match {
- case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
- case _ => throw new XML_Body(List(t))
- }
-
-
- /* representation of standard types */
-
- val properties: T[List[(String, String)]] =
- {
- case List(XML.Elem(Markup(":", props), Nil)) => props
- case ts => throw new XML_Body(ts)
- }
-
- val string: T[String] =
- {
- case Nil => ""
- case List(XML.Text(s)) => s
- case ts => throw new XML_Body(ts)
- }
-
- val long: T[Long] = (x => long_atom(string(x)))
-
- val int: T[Int] = (x => int_atom(string(x)))
-
- val bool: T[Boolean] = (x => bool_atom(string(x)))
-
- val unit: T[Unit] = (x => unit_atom(string(x)))
-
- def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
- {
- case List(t1, t2) => (f(node(t1)), g(node(t2)))
- case ts => throw new XML_Body(ts)
- }
-
- def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
- {
- case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
- case ts => throw new XML_Body(ts)
- }
-
- def list[A](f: T[A]): T[List[A]] =
- (ts => ts.map(t => f(node(t))))
-
- def option[A](f: T[A]): T[Option[A]] =
- {
- case Nil => None
- case List(t) => Some(f(node(t)))
- case ts => throw new XML_Body(ts)
- }
-
- def variant[A](fs: List[T[A]]): T[A] =
- {
- case List(t) =>
- val (tag, ts) = tagged(t)
- fs(tag)(ts)
- case ts => throw new XML_Body(ts)
- }
- }
-}
--- a/src/Pure/IsaMakefile Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/IsaMakefile Tue Jul 12 10:44:30 2011 +0200
@@ -104,7 +104,6 @@
General/timing.ML \
General/url.ML \
General/xml.ML \
- General/xml_data.ML \
General/yxml.ML \
Isar/args.ML \
Isar/attrib.ML \
--- a/src/Pure/PIDE/isar_document.ML Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/PIDE/isar_document.ML Tue Jul 12 10:44:30 2011 +0200
@@ -18,10 +18,10 @@
val old_id = Document.parse_id old_id_string;
val new_id = Document.parse_id new_id_string;
val edits = YXML.parse_body edits_yxml |>
- let open XML_Data.Decode
+ let open XML.Decode
in list (pair string (option (list (pair (option int) (option int))))) end;
val headers = YXML.parse_body headers_yxml |>
- let open XML_Data.Decode
+ let open XML.Decode
in list (pair string (triple string (list string) (list string))) end;
val await_cancellation = Document.cancel_execution state;
--- a/src/Pure/PIDE/isar_document.scala Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/PIDE/isar_document.scala Tue Jul 12 10:44:30 2011 +0200
@@ -143,12 +143,12 @@
edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)])
{
val arg1 =
- { import XML_Data.Encode._
+ { import XML.Encode._
list(pair(string, option(list(pair(option(long), option(long))))))(edits) }
val arg2 =
- { import XML_Data.Encode._
- list(pair(string, Thy_Header.encode_xml_data))(headers) }
+ { import XML.Encode._
+ list(pair(string, Thy_Header.xml_encode))(headers) }
input("Isar_Document.edit_version",
Document.ID(old_id), Document.ID(new_id),
--- a/src/Pure/ROOT.ML Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/ROOT.ML Tue Jul 12 10:44:30 2011 +0200
@@ -53,7 +53,6 @@
use "General/linear_set.ML";
use "General/buffer.ML";
use "General/xml.ML";
-use "General/xml_data.ML";
use "General/pretty.ML";
use "General/path.ML";
use "General/url.ML";
--- a/src/Pure/Thy/thy_header.scala Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/Thy/thy_header.scala Tue Jul 12 10:44:30 2011 +0200
@@ -31,10 +31,10 @@
Header(f(name), imports.map(f), uses.map(f))
}
- val encode_xml_data: XML_Data.Encode.T[Header] =
+ val xml_encode: XML.Encode.T[Header] =
{
case Header(name, imports, uses) =>
- import XML_Data.Encode._
+ import XML.Encode._
triple(string, list(string), list(string))(name, imports, uses)
}
--- a/src/Pure/Tools/find_theorems.ML Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/Tools/find_theorems.ML Tue Jul 12 10:44:30 2011 +0200
@@ -139,8 +139,8 @@
|> (if rem_dups then cons ("rem_dups", "") else I)
|> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I);
in
- XML.Elem (("Query", properties), XML_Data.Encode.list
- (XML_Data.Encode.pair XML_Data.Encode.bool (single o xml_of_criterion)) criteria)
+ XML.Elem (("Query", properties), XML.Encode.list
+ (XML.Encode.pair XML.Encode.bool (single o xml_of_criterion)) criteria)
end
| xml_of_query _ = raise Fail "cannot serialize goal";
@@ -149,7 +149,7 @@
val rem_dups = Properties.defined properties "rem_dups";
val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
val criteria =
- XML_Data.Decode.list (XML_Data.Decode.pair XML_Data.Decode.bool
+ XML.Decode.list (XML.Decode.pair XML.Decode.bool
(criterion_of_xml o the_single)) body;
in
{goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
@@ -190,12 +190,12 @@
val properties =
if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
in
- XML.Elem (("Result", properties), XML_Data.Encode.list (single o xml_of_theorem) theorems)
+ XML.Elem (("Result", properties), XML.Encode.list (single o xml_of_theorem) theorems)
end;
fun result_of_xml (XML.Elem (("Result", properties), body)) =
(Properties.get properties "found" |> Option.map Markup.parse_int,
- XML_Data.Decode.list (theorem_of_xml o the_single) body)
+ XML.Decode.list (theorem_of_xml o the_single) body)
| result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
--- a/src/Pure/build-jars Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/build-jars Tue Jul 12 10:44:30 2011 +0200
@@ -24,7 +24,6 @@
General/sha1.scala
General/symbol.scala
General/xml.scala
- General/xml_data.scala
General/yxml.scala
Isar/keyword.scala
Isar/outer_syntax.scala
--- a/src/Pure/term.scala Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/term.scala Tue Jul 12 10:44:30 2011 +0200
@@ -43,7 +43,7 @@
object Encode
{
- import XML_Data.Encode._
+ import XML.Encode._
val indexname: T[Indexname] = pair(string, int)
@@ -67,7 +67,7 @@
object Decode
{
- import XML_Data.Decode._
+ import XML.Decode._
val indexname: T[Indexname] = pair(string, int)
--- a/src/Pure/term_xml.ML Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/term_xml.ML Tue Jul 12 10:44:30 2011 +0200
@@ -15,8 +15,8 @@
signature TERM_XML =
sig
- structure Encode: TERM_XML_OPS where type 'a T = 'a XML_Data.Encode.T
- structure Decode: TERM_XML_OPS where type 'a T = 'a XML_Data.Decode.T
+ structure Encode: TERM_XML_OPS where type 'a T = 'a XML.Encode.T
+ structure Decode: TERM_XML_OPS where type 'a T = 'a XML.Decode.T
end;
structure Term_XML: TERM_XML =
@@ -27,7 +27,7 @@
structure Encode =
struct
-open XML_Data.Encode;
+open XML.Encode;
val indexname = pair string int;
@@ -54,7 +54,7 @@
structure Decode =
struct
-open XML_Data.Decode;
+open XML.Decode;
val indexname = pair string int;