From 318fc2c04df1e73cc8a178d4fc1ce8bf5543649b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 1 Jun 2016 17:06:25 +0200
Subject: 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.
---
 ide/xml_printer.ml | 145 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 145 insertions(+)
 create mode 100644 ide/xml_printer.ml

(limited to 'ide/xml_printer.ml')

diff --git a/ide/xml_printer.ml b/ide/xml_printer.ml
new file mode 100644
index 0000000000..e7e4d0cebc
--- /dev/null
+++ b/ide/xml_printer.ml
@@ -0,0 +1,145 @@
+(************************************************************************)
+(*  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 ()
-- 
cgit v1.2.3