From 7c22a0f4b7865e692076a6531de9fdab14ead99f Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 9 May 2013 10:31:24 +0000
Subject: Xml_datatype.mli ships the xml type

This breaks the dependency of Xml_parser, Xml_printer and Xml_utils
on Serialize.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16493 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/serialize.ml     |  5 +----
 lib/serialize.mli    |  5 +----
 lib/xml_datatype.mli | 12 ++++++++++++
 lib/xml_parser.ml    |  2 +-
 lib/xml_parser.mli   |  2 +-
 lib/xml_printer.ml   |  2 +-
 lib/xml_printer.mli  |  2 +-
 lib/xml_utils.ml     |  2 +-
 lib/xml_utils.mli    |  2 +-
 9 files changed, 20 insertions(+), 14 deletions(-)
 create mode 100644 lib/xml_datatype.mli

(limited to 'lib')

diff --git a/lib/serialize.ml b/lib/serialize.ml
index 186c3dc890..9fbd5683dc 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -15,10 +15,7 @@ let protocol_version = "20120710"
 (** * Interface of calls to Coq by CoqIde *)
 
 open Interface
-
-type xml =
-        | Element of (string * (string * string) list * xml list)
-        | PCData of string
+open Xml_datatype
 
 (** We use phantom types and GADT to protect ourselves against wild casts *)
 
diff --git a/lib/serialize.mli b/lib/serialize.mli
index 4af4d09749..48c699a2f4 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -9,10 +9,7 @@
 (** * Applicative part of the interface of CoqIde calls to Coq *)
 
 open Interface
-
-type xml =
-        | Element of (string * (string * string) list * xml list)
-        | PCData of string
+open Xml_datatype
 
 type 'a call
 
diff --git a/lib/xml_datatype.mli b/lib/xml_datatype.mli
new file mode 100644
index 0000000000..7b18c73bfb
--- /dev/null
+++ b/lib/xml_datatype.mli
@@ -0,0 +1,12 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+type xml =
+        | Element of (string * (string * string) list * xml list)
+        | PCData of string
+
diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml
index 630992eb5f..b9990c75a6 100644
--- a/lib/xml_parser.ml
+++ b/lib/xml_parser.ml
@@ -20,7 +20,7 @@
 
 open Printf
 
-type xml = Serialize.xml =
+type xml = Xml_datatype.xml =
         | Element of (string * (string * string) list * xml list)
         | PCData of string
 
diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli
index d48e892561..74a7693ac8 100644
--- a/lib/xml_parser.mli
+++ b/lib/xml_parser.mli
@@ -27,7 +27,7 @@
 
 (** An Xml node is either
         [Element (tag-name, attributes, children)] or [PCData text] *)
-type xml = Serialize.xml
+type xml = Xml_datatype.xml
 
 (** Abstract type for an Xml parser. *)
 type t
diff --git a/lib/xml_printer.ml b/lib/xml_printer.ml
index ae4d34c773..001b48ed9d 100644
--- a/lib/xml_printer.ml
+++ b/lib/xml_printer.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-type xml = Serialize.xml =
+type xml = Xml_datatype.xml =
         | Element of (string * (string * string) list * xml list)
         | PCData of string
 
diff --git a/lib/xml_printer.mli b/lib/xml_printer.mli
index b19e189432..a18aaed1bf 100644
--- a/lib/xml_printer.mli
+++ b/lib/xml_printer.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-type xml = Serialize.xml
+type xml = Xml_datatype.xml
 
 type t
 type target = TChannel of out_channel | TBuffer of Buffer.t
diff --git a/lib/xml_utils.ml b/lib/xml_utils.ml
index 53e694c7a0..89407be194 100644
--- a/lib/xml_utils.ml
+++ b/lib/xml_utils.ml
@@ -17,7 +17,7 @@
  * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
  *)
 
-open Serialize
+open Xml_datatype
 
 exception Not_element of xml
 exception Not_pcdata of xml
diff --git a/lib/xml_utils.mli b/lib/xml_utils.mli
index 67cd5cb93a..a9574e1f06 100644
--- a/lib/xml_utils.mli
+++ b/lib/xml_utils.mli
@@ -29,7 +29,7 @@
   {i (c)Copyright 2002-2003 Nicolas Cannasse}
 *)
 
-open Serialize
+open Xml_datatype
 
 (** {6 Xml Functions} *)
 
-- 
cgit v1.2.3