Move ide serialization libraries from lib/ to ide/

This makes the core free from particular protocol choices.

It should help with the ppx serialization project and shrinks clib.cma a
bit.

9 files changed, 0 insertions, 1036 deletions

diff --git a/lib/clib.mllib b/lib/clib.mllib
index c3ec4a696e..95007c52ab 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -21,7 +21,6 @@ Control
 Loc
 CList
 CString
-Serialize
 Deque
 CObj
 CArray
@@ -33,9 +32,6 @@ Ppstyle
 Xml_datatype
 Richpp
 Feedback
-Xml_lexer
-Xml_parser
-Xml_printer
 CUnix
 Envars
 Aux_file
diff --git a/lib/serialize.ml b/lib/serialize.ml
deleted file mode 100644
index 685ec6049c..0000000000
--- a/lib/serialize.ml
+++ /dev/null
@@ -1,120 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Xml_datatype
-
-exception Marshal_error
-
-(** Utility functions *)
-
-let rec get_attr attr = function
-  | [] -> raise Not_found
-  | (k, v) :: l when CString.equal k attr -> v
-  | _ :: l -> get_attr attr l
-
-let massoc x l =
-  try get_attr x l
-  with Not_found -> raise Marshal_error
-
-let constructor t c args = Element (t, ["val", c], args)
-let do_match t mf = function
-  | Element (s, attrs, args) when CString.equal s t ->
-      let c = massoc "val" attrs in
-      mf c args
-  | _ -> raise Marshal_error
-
-let singleton = function
-  | [x] -> x
-  | _ -> raise Marshal_error
-
-let raw_string = function
-  | [] -> ""
-  | [PCData s] -> s
-  | _ -> raise Marshal_error
-
-(** Base types *)
-
-let of_unit () = Element ("unit", [], [])
-let to_unit : xml -> unit = function
-  | Element ("unit", [], []) -> ()
-  | _ -> raise Marshal_error
-
-let of_bool (b : bool) : xml =
-  if b then constructor "bool" "true" []
-  else constructor "bool" "false" []
-let to_bool : xml -> bool = do_match "bool" (fun s _ -> match s with
-  | "true" -> true
-  | "false" -> false
-  | _ -> raise Marshal_error)
-
-let of_list (f : 'a -> xml) (l : 'a list) =
-  Element ("list", [], List.map f l)
-let to_list (f : xml -> 'a) : xml -> 'a list = function
-  | Element ("list", [], l) -> List.map f l
-  | _ -> raise Marshal_error
-
-let of_option (f : 'a -> xml) : 'a option -> xml = function
-  | None -> Element ("option", ["val", "none"], [])
-  | Some x -> Element ("option", ["val", "some"], [f x])
-let to_option (f : xml -> 'a) : xml -> 'a option = function
-  | Element ("option", ["val", "none"], []) -> None
-  | Element ("option", ["val", "some"], [x]) -> Some (f x)
-  | _ -> raise Marshal_error
-
-let of_string (s : string) : xml = Element ("string", [], [PCData s])
-let to_string : xml -> string = function
-  | Element ("string", [], l) -> raw_string l
-  | _ -> raise Marshal_error
-
-let of_int (i : int) : xml = Element ("int", [], [PCData (string_of_int i)])
-let to_int : xml -> int = function
-  | Element ("int", [], [PCData s]) ->
-    (try int_of_string s with Failure _ -> raise Marshal_error)
-  | _ -> raise Marshal_error
-
-let of_pair (f : 'a -> xml) (g : 'b -> xml) (x : 'a * 'b) : xml =
-  Element ("pair", [], [f (fst x); g (snd x)])
-let to_pair (f : xml -> 'a) (g : xml -> 'b) : xml -> 'a * 'b = function
-  | Element ("pair", [], [x; y]) -> (f x, g y)
-  | _ -> raise Marshal_error
-
-let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) CSig.union -> xml = function
-  | CSig.Inl x -> Element ("union", ["val","in_l"], [f x])
-  | CSig.Inr x -> Element ("union", ["val","in_r"], [g x])
-let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) CSig.union = function
-  | Element ("union", ["val","in_l"], [x]) -> CSig.Inl (f x)
-  | Element ("union", ["val","in_r"], [x]) -> CSig.Inr (g x)
-  | _ -> raise Marshal_error
-
-(** More elaborate types *)
-
-let of_edit_id i = Element ("edit_id",["val",string_of_int i],[])
-let to_edit_id = function
-  | Element ("edit_id",["val",i],[]) ->
-      let id = int_of_string i in
-      assert (id <= 0 );
-      id
-  | _ -> raise Marshal_error
-
-let of_loc loc =
-  let start, stop = Loc.unloc loc in
-  Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[])
-let to_loc xml =
-  match xml with
-  | Element ("loc", l,[]) ->
-      (try
-        let start = massoc "start" l in
-        let stop = massoc "stop" l in
-        Loc.make_loc (int_of_string start, int_of_string stop)
-      with Not_found | Invalid_argument _ -> raise Marshal_error)
-  | _ -> raise Marshal_error
-
-let of_xml x = Element ("xml", [], [x])
-let to_xml xml = match xml with
-| Element ("xml", [], [x]) -> x
-| _ -> raise Marshal_error
diff --git a/lib/serialize.mli b/lib/serialize.mli
deleted file mode 100644
index d7c14e7e73..0000000000
--- a/lib/serialize.mli
+++ /dev/null
@@ -1,39 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Xml_datatype
-
-exception Marshal_error
-
-val massoc: string -> (string * string) list -> string
-val constructor: string -> string -> xml list -> xml
-val do_match: string -> (string -> xml list -> 'b) -> xml -> 'b
-val singleton: 'a list -> 'a
-val raw_string: xml list -> string
-val of_unit: unit -> xml
-val to_unit: xml -> unit
-val of_bool: bool -> xml
-val to_bool: xml -> bool
-val of_list: ('a -> xml) -> 'a list -> xml
-val to_list: (xml -> 'a) -> xml -> 'a list
-val of_option: ('a -> xml) -> 'a option -> xml
-val to_option: (xml -> 'a) -> xml -> 'a option
-val of_string: string -> xml
-val to_string: xml -> string
-val of_int: int -> xml
-val to_int: xml -> int
-val of_pair: ('a -> xml) -> ('b -> xml) -> 'a * 'b -> xml
-val to_pair: (xml -> 'a) -> (xml -> 'b) -> xml -> 'a * 'b
-val of_union: ('a -> xml) -> ('b -> xml) -> ('a, 'b) CSig.union -> xml
-val to_union: (xml -> 'a) -> (xml -> 'b) -> xml -> ('a, 'b) CSig.union
-val of_edit_id: int -> xml
-val to_edit_id: xml -> int
-val of_loc : Loc.t -> xml
-val to_loc : xml -> Loc.t
-val of_xml : xml -> xml
-val to_xml : xml -> xml
diff --git a/lib/xml_lexer.mli b/lib/xml_lexer.mli
deleted file mode 100644
index e61cb055f7..0000000000
--- a/lib/xml_lexer.mli
+++ /dev/null
@@ -1,44 +0,0 @@
-(*
- * Xml Light, an small Xml parser/printer with DTD support.
- * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License as published by the Free Software Foundation; either
- * version 2.1 of the License, or (at your option) any later version.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this library; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
- *)
-
-type error =
-	| EUnterminatedComment
-	| EUnterminatedString
-	| EIdentExpected
-	| ECloseExpected
-	| ENodeExpected
-	| EAttributeNameExpected
-	| EAttributeValueExpected
-	| EUnterminatedEntity
-
-exception Error of error
-
-type token =
-	| Tag of string * (string * string) list * bool
-	| PCData of string
-	| Endtag of string
-	| Eof
-
-type pos = int * int * int * int
-
-val init : Lexing.lexbuf -> unit 
-val close : unit -> unit
-val token : Lexing.lexbuf -> token
-val pos : Lexing.lexbuf -> pos
-val restore : pos -> unit
diff --git a/lib/xml_lexer.mll b/lib/xml_lexer.mll
deleted file mode 100644
index 290f2c89ab..0000000000
--- a/lib/xml_lexer.mll
+++ /dev/null
@@ -1,317 +0,0 @@
-{(*
- * Xml Light, an small Xml parser/printer with DTD support.
- * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License as published by the Free Software Foundation; either
- * version 2.1 of the License, or (at your option) any later version.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this library; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
- *)
-
-open Lexing
-
-type error =
-        | EUnterminatedComment
-        | EUnterminatedString
-        | EIdentExpected
-        | ECloseExpected
-        | ENodeExpected
-        | EAttributeNameExpected
-        | EAttributeValueExpected
-        | EUnterminatedEntity
-
-exception Error of error
-
-type pos = int * int * int * int
-
-type token =
-        | Tag of string * (string * string) list * bool
-        | PCData of string
-        | Endtag of string
-        | Eof
-
-let last_pos = ref 0
-and current_line = ref 0
-and current_line_start = ref 0
-
-let tmp = Buffer.create 200
-
-let idents = Hashtbl.create 0
-
-let _ = begin
-        Hashtbl.add idents "nbsp;" " ";
-        Hashtbl.add idents "gt;" ">";
-        Hashtbl.add idents "lt;" "<";
-        Hashtbl.add idents "amp;" "&";
-        Hashtbl.add idents "apos;" "'";
-        Hashtbl.add idents "quot;" "\"";
-end
-
-let init lexbuf =
-        current_line := 1;
-        current_line_start := lexeme_start lexbuf;
-        last_pos := !current_line_start
-
-let close lexbuf =
-        Buffer.reset tmp
-
-let pos lexbuf =
-        !current_line , !current_line_start ,
-        !last_pos ,
-        lexeme_start lexbuf
-
-let restore (cl,cls,lp,_) =
-        current_line := cl;
-        current_line_start := cls;
-        last_pos := lp
-
-let newline lexbuf =
-        incr current_line;
-        last_pos := lexeme_end lexbuf;
-        current_line_start := !last_pos
-
-let error lexbuf e =
-        last_pos := lexeme_start lexbuf;
-        raise (Error e)
-
-}
-
-let newline = ['\n']
-let break = ['\r']
-let space = [' ' '\t']
-let identchar =  ['A'-'Z' 'a'-'z' '_' '0'-'9' ':' '-' '.']
-let ident = ['A'-'Z' 'a'-'z' '_' ':'] identchar*
-let entitychar = ['A'-'Z' 'a'-'z']
-let pcchar = [^ '\r' '\n' '<' '>' '&']
-
-rule token = parse
-        | newline | (newline break) | break
-                {
-                        newline lexbuf;
-                        PCData "\n"
-                }
-        | "<!--"
-                {
-                        last_pos := lexeme_start lexbuf;
-                        comment lexbuf;
-                        token lexbuf
-                }
-        | "<?"
-                {
-                        last_pos := lexeme_start lexbuf;
-                        header lexbuf;
-                        token lexbuf;
-                }
-        | '<' space* '/' space*
-                {
-                        last_pos := lexeme_start lexbuf;
-                        let tag = ident_name lexbuf in
-                        ignore_spaces lexbuf;
-                        close_tag lexbuf;
-                        Endtag tag
-                }
-        | '<' space*
-                {
-                        last_pos := lexeme_start lexbuf;
-                        let tag = ident_name lexbuf in
-                        ignore_spaces lexbuf;
-                        let attribs, closed = attributes lexbuf in
-                        Tag(tag, attribs, closed)
-                }
-        | "&#"
-                {
-                        last_pos := lexeme_start lexbuf;
-                        Buffer.reset tmp;
-                        Buffer.add_string tmp (lexeme lexbuf);
-                        PCData (pcdata lexbuf)
-                }
-        | '&'
-                {
-                        last_pos := lexeme_start lexbuf;
-                        Buffer.reset tmp;
-                        Buffer.add_string tmp (entity lexbuf);
-                        PCData (pcdata lexbuf)
-                }
-        | pcchar+
-                {
-                        last_pos := lexeme_start lexbuf;
-                        Buffer.reset tmp;
-                        Buffer.add_string tmp (lexeme lexbuf);
-                        PCData (pcdata lexbuf)
-                }
-        | eof { Eof }
-        | _
-                { error lexbuf ENodeExpected }
-
-and ignore_spaces = parse
-        | newline | (newline break) | break
-                {
-                        newline lexbuf;
-                        ignore_spaces lexbuf
-                }
-        | space +
-                { ignore_spaces lexbuf }
-        | ""
-                { () }
-
-and comment = parse
-        | newline | (newline break) | break
-                {
-                        newline lexbuf;
-                        comment lexbuf
-                }
-        | "-->"
-                { () }
-        | eof
-                { raise (Error EUnterminatedComment) }
-        | _
-                { comment lexbuf }
-
-and header = parse
-        | newline | (newline break) | break
-                {
-                        newline lexbuf;
-                        header lexbuf
-                }
-        | "?>"
-                { () }
-        | eof
-                { error lexbuf ECloseExpected }
-        | _
-                { header lexbuf }
-
-and pcdata = parse
-        | newline | (newline break) | break
-                {
-                        Buffer.add_char tmp '\n';
-                        newline lexbuf;
-                        pcdata lexbuf
-                }
-        | pcchar+
-                {
-                        Buffer.add_string tmp (lexeme lexbuf);
-                        pcdata lexbuf
-                }
-        | "&#"
-                {
-                        Buffer.add_string tmp (lexeme lexbuf);
-                        pcdata lexbuf;
-                }
-        | '&'
-                {
-                        Buffer.add_string tmp (entity lexbuf);
-                        pcdata lexbuf
-                }
-        | ""
-                { Buffer.contents tmp }
-
-and entity = parse
-        | entitychar+ ';'
-                {
-                        let ident = lexeme lexbuf in
-                        try
-                                Hashtbl.find idents (String.lowercase ident)
-                        with
-                                Not_found -> "&" ^ ident
-                }
-        | _ | eof
-                { raise (Error EUnterminatedEntity) }
-
-and ident_name = parse
-        | ident
-                { lexeme lexbuf }
-        | _ | eof
-                { error lexbuf EIdentExpected }
-
-and close_tag = parse
-        | '>'
-                { () }
-        | _ | eof
-                { error lexbuf ECloseExpected }
-
-and attributes = parse
-        | '>'
-                { [], false }
-        | "/>"
-                { [], true }
-        | "" (* do not read a char ! *)
-                {
-                        let key = attribute lexbuf in
-                        let data = attribute_data lexbuf in
-                        ignore_spaces lexbuf;
-                        let others, closed = attributes lexbuf in
-                        (key, data) :: others, closed
-                }
-
-and attribute = parse
-        | ident
-                { lexeme lexbuf }
-        | _ | eof
-                { error lexbuf EAttributeNameExpected }
-
-and attribute_data = parse
-        | space* '=' space* '"'
-                {
-                        Buffer.reset tmp;
-                        last_pos := lexeme_end lexbuf;
-                        dq_string lexbuf
-                }
-        | space* '=' space* '\''
-                {
-                        Buffer.reset tmp;
-                        last_pos := lexeme_end lexbuf;
-                        q_string lexbuf
-                }
-        | _ | eof
-                { error lexbuf EAttributeValueExpected }
-
-and dq_string = parse
-        | '"'
-                { Buffer.contents tmp }
-        | '\\' [ '"' '\\' ]
-                {
-                        Buffer.add_char tmp (lexeme_char lexbuf 1);
-                        dq_string lexbuf
-                }
-        | '&'
-                {
-                        Buffer.add_string tmp (entity lexbuf);
-                        dq_string lexbuf
-                }
-        | eof
-                { raise (Error EUnterminatedString) }
-        | _
-                {
-                        Buffer.add_char tmp (lexeme_char lexbuf 0);
-                        dq_string lexbuf
-                }
-
-and q_string = parse
-        | '\''
-                { Buffer.contents tmp }
-        | '\\' [ '\'' '\\' ]
-                {
-                        Buffer.add_char tmp (lexeme_char lexbuf 1);
-                        q_string lexbuf
-                }
-        | '&'
-                {
-                        Buffer.add_string tmp (entity lexbuf);
-                        q_string lexbuf
-                }
-        | eof
-                { raise (Error EUnterminatedString) }
-        | _
-                {
-                        Buffer.add_char tmp (lexeme_char lexbuf 0);
-                        q_string lexbuf
-                }
diff --git a/lib/xml_parser.ml b/lib/xml_parser.ml
deleted file mode 100644
index 8db3f9e8ba..0000000000
--- a/lib/xml_parser.ml
+++ /dev/null
@@ -1,232 +0,0 @@
-(*
- * Xml Light, an small Xml parser/printer with DTD support.
- * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
- * Copyright (C) 2003 Jacques Garrigue
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License as published by the Free Software Foundation; either
- * version 2.1 of the License, or (at your option) any later version.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this library; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
- *)
-
-open Printf
-open Xml_datatype
-
-type xml = Xml_datatype.xml
-
-type error_pos = {
-  eline : int;
-  eline_start : int;
-  emin : int;
-  emax : int;
-}
-
-type error_msg =
-  | UnterminatedComment
-  | UnterminatedString
-  | UnterminatedEntity
-  | IdentExpected
-  | CloseExpected
-  | NodeExpected
-  | AttributeNameExpected
-  | AttributeValueExpected
-  | EndOfTagExpected of string
-  | EOFExpected
-  | Empty
-
-type error = error_msg * error_pos
-
-exception Error of error
-
-exception File_not_found of string
-
-type t = {
-  mutable check_eof : bool;
-  mutable concat_pcdata : bool;
-  source : Lexing.lexbuf;
-  stack : Xml_lexer.token Stack.t;
-}
-
-type source =
-  | SChannel of in_channel
-  | SString of string
-  | SLexbuf of Lexing.lexbuf
-
-exception Internal_error of error_msg
-exception NoMoreData
-
-let xml_error = ref (fun _ -> assert false)
-let file_not_found = ref (fun _ -> assert false)
-
-let is_blank s =
-  let len = String.length s in
-  let break = ref true in
-  let i = ref 0 in
-  while !break && !i < len do
-    let c = s.[!i] in
-    (* no '\r' because we replaced them in the lexer *)
-    if c = ' ' || c = '\n' || c = '\t' then incr i
-    else break := false
-  done;
-  !i = len
-
-let _raises e f =
-  xml_error := e;
-  file_not_found := f
-
-let make source =
-  let source = match source with
-    | SChannel chan -> Lexing.from_channel chan
-    | SString s -> Lexing.from_string s
-    | SLexbuf lexbuf -> lexbuf
-  in
-  let () = Xml_lexer.init source in
-  {
-    check_eof = false;
-    concat_pcdata = true;
-    source = source;
-    stack = Stack.create ();
-  }
-
-let check_eof p v = p.check_eof <- v
-
-let pop s =
-  try
-    Stack.pop s.stack
-  with
-      Stack.Empty ->
-        Xml_lexer.token s.source
-
-let push t s =
-  Stack.push t s.stack
-
-let canonicalize l =
-  let has_elt = List.exists (function Element _ -> true | _ -> false) l in
-  if has_elt then List.filter (function PCData s -> not (is_blank s) | _ -> true) l
-  else l
-
-let rec read_xml do_not_canonicalize s =
-  let rec read_node s =
-    match pop s with
-      | Xml_lexer.PCData s -> PCData s
-      | Xml_lexer.Tag (tag, attr, true) -> Element (tag, attr, [])
-      | Xml_lexer.Tag (tag, attr, false) ->
-        let elements = read_elems tag s in
-        let elements =
-          if do_not_canonicalize then elements else canonicalize elements
-        in
-        Element (tag, attr, elements)
-      | t ->
-        push t s;
-        raise NoMoreData
-
-  and read_elems tag s =
-    let elems = ref [] in
-    (try
-       while true do
-         let node = read_node s in
-         match node, !elems with
-           | PCData c , (PCData c2) :: q ->
-             elems := PCData (c2 ^ c) :: q
-           | _, l ->
-             elems := node :: l
-       done
-     with
-         NoMoreData -> ());
-    match pop s with
-      | Xml_lexer.Endtag s when s = tag -> List.rev !elems
-      | t -> raise (Internal_error (EndOfTagExpected tag))
-  in
-  match read_node s with
-    | (Element _) as node ->
-      node
-    | PCData c ->
-      if is_blank c then
-        read_xml do_not_canonicalize s
-      else
-        raise (Xml_lexer.Error Xml_lexer.ENodeExpected)
-
-let convert = function
-  | Xml_lexer.EUnterminatedComment -> UnterminatedComment
-  | Xml_lexer.EUnterminatedString -> UnterminatedString
-  | Xml_lexer.EIdentExpected -> IdentExpected
-  | Xml_lexer.ECloseExpected -> CloseExpected
-  | Xml_lexer.ENodeExpected -> NodeExpected
-  | Xml_lexer.EAttributeNameExpected -> AttributeNameExpected
-  | Xml_lexer.EAttributeValueExpected -> AttributeValueExpected
-  | Xml_lexer.EUnterminatedEntity ->      UnterminatedEntity
-
-let error_of_exn xparser = function
-  | NoMoreData when pop xparser = Xml_lexer.Eof -> Empty
-  | NoMoreData -> NodeExpected
-  | Internal_error e -> e
-  | Xml_lexer.Error e -> convert e
-  | e ->
-    (*let e = Errors.push e in: We do not record backtrace here. *)
-    raise e
-
-let do_parse do_not_canonicalize xparser =
-  try
-    Xml_lexer.init xparser.source;
-    let x = read_xml do_not_canonicalize xparser in
-    if xparser.check_eof && pop xparser <> Xml_lexer.Eof then raise (Internal_error EOFExpected);
-    Xml_lexer.close ();
-    x
-  with any ->
-    Xml_lexer.close ();
-    raise (!xml_error (error_of_exn xparser any) xparser.source)
-
-let parse ?(do_not_canonicalize=false) p =
-  do_parse do_not_canonicalize p
-
-let error_msg = function
-  | UnterminatedComment -> "Unterminated comment"
-  | UnterminatedString -> "Unterminated string"
-  | UnterminatedEntity -> "Unterminated entity"
-  | IdentExpected -> "Ident expected"
-  | CloseExpected -> "Element close expected"
-  | NodeExpected -> "Xml node expected"
-  | AttributeNameExpected -> "Attribute name expected"
-  | AttributeValueExpected -> "Attribute value expected"
-  | EndOfTagExpected tag -> sprintf "End of tag expected : '%s'" tag
-  | EOFExpected -> "End of file expected"
-  | Empty -> "Empty"
-
-let error (msg,pos) =
-  if pos.emin = pos.emax then
-    sprintf "%s line %d character %d" (error_msg msg) pos.eline
-      (pos.emin - pos.eline_start)
-  else
-    sprintf "%s line %d characters %d-%d" (error_msg msg) pos.eline
-      (pos.emin - pos.eline_start) (pos.emax - pos.eline_start)
-
-let line e = e.eline
-
-let range e =
-  e.emin - e.eline_start , e.emax - e.eline_start
-
-let abs_range e =
-  e.emin , e.emax
-
-let pos source =
-  let line, lstart, min, max = Xml_lexer.pos source in
-  {
-    eline = line;
-    eline_start = lstart;
-    emin = min;
-    emax = max;
-  }
-
-let () = _raises (fun x p ->
-        (* local cast : Xml.error_msg -> error_msg *)
-  Error (x, pos p))
-  (fun f -> File_not_found f)
diff --git a/lib/xml_parser.mli b/lib/xml_parser.mli
deleted file mode 100644
index ac2eab352f..0000000000
--- a/lib/xml_parser.mli
+++ /dev/null
@@ -1,106 +0,0 @@
-(*
- * Xml Light, an small Xml parser/printer with DTD support.
- * Copyright (C) 2003 Nicolas Cannasse (ncannasse@motion-twin.com)
- *
- * This library is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public
- * License as published by the Free Software Foundation; either
- * version 2.1 of the License, or (at your option) any later version.
- *
- * This library is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this library; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
- *)
-
-(** Xml Light Parser
-
- While basic parsing functions can be used in the {!Xml} module, this module
- is providing a way to create, configure and run an Xml parser.
-
-*)
-
-
-(** An Xml node is either
-        [Element (tag-name, attributes, children)] or [PCData text] *)
-type xml = Xml_datatype.xml
-
-(** Abstract type for an Xml parser. *)
-type t
-
-(** {6:exc Xml Exceptions} *)
-
-(** Several exceptions can be raised when parsing an Xml document : {ul
-        {li {!Xml.Error} is raised when an xml parsing error occurs. the
-                {!Xml.error_msg} tells you which error occurred during parsing
-                and the {!Xml.error_pos} can be used to retrieve the document
-                location where the error occurred at.}
-        {li {!Xml.File_not_found} is raised when an error occurred while
-                opening a file with the {!Xml.parse_file} function.}
-        }
- *)
-
-type error_pos
-
-type error_msg =
-        | UnterminatedComment
-        | UnterminatedString
-        | UnterminatedEntity
-        | IdentExpected
-        | CloseExpected
-        | NodeExpected
-        | AttributeNameExpected
-        | AttributeValueExpected
-        | EndOfTagExpected of string
-        | EOFExpected
-        | Empty
-
-type error = error_msg * error_pos
-
-exception Error of error
-
-exception File_not_found of string
-
-(** Get a full error message from an Xml error. *)
-val error : error -> string
-
-(** Get the Xml error message as a string. *)
-val error_msg : error_msg -> string
-
-(** Get the line the error occurred at. *)
-val line : error_pos -> int
-
-(** Get the relative character range (in current line) the error occurred at.*)
-val range : error_pos -> int * int
-
-(** Get the absolute character range the error occurred at. *)
-val abs_range : error_pos -> int * int
-
-val pos : Lexing.lexbuf -> error_pos
-
-(** Several kind of resources can contain Xml documents. *)
-type source =
-| SChannel of in_channel
-| SString of string
-| SLexbuf of Lexing.lexbuf
-
-(** This function returns a new parser with default options. *)
-val make : source -> t
-
-(** When a Xml document is parsed, the parser may check that the end of the
- document is reached, so for example parsing ["<A/><B/>"] will fail instead
- of returning only the A element. You can turn on this check by setting
- [check_eof] to [true] {i (by default, check_eof is false, unlike
- in the original Xmllight)}. *)
-val check_eof : t -> bool -> unit
-
-(** Once the parser is configured, you can run the parser on a any kind
-    of xml document source to parse its contents into an Xml data structure.
-
-    When [do_not_canonicalize] is set, the XML document is given as
-    is, without trying to remove blank PCDATA elements. *)
-val parse : ?do_not_canonicalize:bool -> t -> xml
diff --git a/lib/xml_printer.ml b/lib/xml_printer.ml
deleted file mode 100644
index e7e4d0cebc..0000000000
--- a/lib/xml_printer.ml
+++ /dev/null
@@ -1,145 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Xml_datatype
-
-type xml = Xml_datatype.xml
-
-type target = TChannel of out_channel | TBuffer of Buffer.t
-
-type t = target
-
-let make x = x
-
-let buffer_pcdata tmp text =
-  let output = Buffer.add_string tmp in
-  let output' = Buffer.add_char tmp in
-  let l = String.length text in
-  for p = 0 to l-1 do
-    match text.[p] with
-      | ' ' -> output "&nbsp;";
-      | '>' -> output "&gt;"
-      | '<' -> output "&lt;"
-      | '&' ->
-        if p < l - 1 && text.[p + 1] = '#' then
-          output' '&'
-        else
-          output "&amp;"
-      | '\'' -> output "&apos;"
-      | '"' -> output "&quot;"
-      | c -> output' c
-  done
-
-let buffer_attr tmp (n,v) =
-  let output = Buffer.add_string tmp in
-  let output' = Buffer.add_char tmp in
-  output' ' ';
-  output n;
-  output "=\"";
-  let l = String.length v in
-  for p = 0 to l - 1 do
-    match v.[p] with
-      | '\\' -> output "\\\\"
-      | '"' -> output "\\\""
-      | '<' -> output "&lt;"
-      | '&' -> output "&amp;"
-      | c -> output' c
-  done;
-  output' '"'
-
-let to_buffer tmp x =
-  let pcdata = ref false in
-  let output = Buffer.add_string tmp in
-  let output' = Buffer.add_char tmp in
-  let rec loop = function
-    | Element (tag,alist,[]) ->
-      output' '<';
-      output tag;
-      List.iter (buffer_attr tmp) alist;
-      output "/>";
-      pcdata := false;
-    | Element (tag,alist,l) ->
-      output' '<';
-      output tag;
-      List.iter (buffer_attr tmp) alist;
-      output' '>';
-      pcdata := false;
-      List.iter loop l;
-      output "</";
-      output tag;
-      output' '>';
-      pcdata := false;
-    | PCData text ->
-      if !pcdata then output' ' ';
-      buffer_pcdata tmp text;
-      pcdata := true;
-  in
-  loop x
-
-let pcdata_to_string s =
-  let b = Buffer.create 13 in
-  buffer_pcdata b s;
-  Buffer.contents b
-
-let to_string x =
-  let b = Buffer.create 200 in
-  to_buffer b x;
-  Buffer.contents b
-
-let to_string_fmt x =
-  let tmp = Buffer.create 200 in
-  let output = Buffer.add_string tmp in
-  let output' = Buffer.add_char tmp in
-  let rec loop ?(newl=false) tab = function
-    | Element (tag, alist, []) ->
-      output tab;
-      output' '<';
-      output tag;
-      List.iter (buffer_attr tmp) alist;
-      output "/>";
-      if newl then output' '\n';
-    | Element (tag, alist, [PCData text]) ->
-      output tab;
-      output' '<';
-      output tag;
-      List.iter (buffer_attr tmp) alist;
-      output ">";
-      buffer_pcdata tmp text;
-      output "</";
-      output tag;
-      output' '>';
-      if newl then output' '\n';
-    | Element (tag, alist, l) ->
-      output tab;
-      output' '<';
-      output tag;
-      List.iter (buffer_attr tmp) alist;
-      output ">\n";
-      List.iter (loop ~newl:true (tab^"  ")) l;
-      output tab;
-      output "</";
-      output tag;
-      output' '>';
-      if newl then output' '\n';
-    | PCData text ->
-      buffer_pcdata tmp text;
-      if newl then output' '\n';
-  in
-  loop "" x;
-  Buffer.contents tmp
-
-let print t xml =
-  let tmp, flush = match t with
-    | TChannel oc ->
-      let b = Buffer.create 200 in
-      b, (fun () -> Buffer.output_buffer oc b; flush oc)
-    | TBuffer b ->
-      b, (fun () -> ())
-  in
-  to_buffer tmp xml;
-  flush ()
diff --git a/lib/xml_printer.mli b/lib/xml_printer.mli
deleted file mode 100644
index f24f51fff5..0000000000
--- a/lib/xml_printer.mli
+++ /dev/null
@@ -1,29 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-type xml = Xml_datatype.xml
-
-type t
-type target = TChannel of out_channel | TBuffer of Buffer.t
-
-val make : target -> t
-
-(** Print the xml data structure to a source into a compact xml string (without
- any user-readable formating ). *)
-val print : t -> xml -> unit
-
-(** Print the xml data structure into a compact xml string (without
- any user-readable formating ). *)
-val to_string : xml -> string
-
-(** Print the xml data structure into an user-readable string with
- tabs and lines break between different nodes. *)
-val to_string_fmt : xml -> string
-
-(** Print PCDATA as a string by escaping XML entities. *)
-val pcdata_to_string : string -> string