From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 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 00000000..40ab4ce9
--- /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 puts = Buffer.add_string tmp in
+  let putc = Buffer.add_char tmp in
+  let l = String.length text in
+  for p = 0 to l-1 do
+    match text.[p] with
+      | ' ' -> puts "&nbsp;";
+      | '>' -> puts "&gt;"
+      | '<' -> puts "&lt;"
+      | '&' ->
+        if p < l - 1 && text.[p + 1] = '#' then
+          putc '&'
+        else
+          puts "&amp;"
+      | '\'' -> puts "&apos;"
+      | '"' -> puts "&quot;"
+      | c -> putc c
+  done
+
+let buffer_attr tmp (n,v) =
+  let puts = Buffer.add_string tmp in
+  let putc = Buffer.add_char tmp in
+  putc ' ';
+  puts n;
+  puts "=\"";
+  let l = String.length v in
+  for p = 0 to l - 1 do
+    match v.[p] with
+      | '\\' -> puts "\\\\"
+      | '"' -> puts "\\\""
+      | '<' -> puts "&lt;"
+      | '&' -> puts "&amp;"
+      | c -> putc c
+  done;
+  putc '"'
+
+let to_buffer tmp x =
+  let pcdata = ref false in
+  let puts = Buffer.add_string tmp in
+  let putc = Buffer.add_char tmp in
+  let rec loop = function
+    | Element (tag,alist,[]) ->
+      putc '<';
+      puts tag;
+      List.iter (buffer_attr tmp) alist;
+      puts "/>";
+      pcdata := false;
+    | Element (tag,alist,l) ->
+      putc '<';
+      puts tag;
+      List.iter (buffer_attr tmp) alist;
+      putc '>';
+      pcdata := false;
+      List.iter loop l;
+      puts "</";
+      puts tag;
+      putc '>';
+      pcdata := false;
+    | PCData text ->
+      if !pcdata then putc ' ';
+      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 puts = Buffer.add_string tmp in
+  let putc = Buffer.add_char tmp in
+  let rec loop ?(newl=false) tab = function
+    | Element (tag, alist, []) ->
+      puts tab;
+      putc '<';
+      puts tag;
+      List.iter (buffer_attr tmp) alist;
+      puts "/>";
+      if newl then putc '\n';
+    | Element (tag, alist, [PCData text]) ->
+      puts tab;
+      putc '<';
+      puts tag;
+      List.iter (buffer_attr tmp) alist;
+      puts ">";
+      buffer_pcdata tmp text;
+      puts "</";
+      puts tag;
+      putc '>';
+      if newl then putc '\n';
+    | Element (tag, alist, l) ->
+      puts tab;
+      putc '<';
+      puts tag;
+      List.iter (buffer_attr tmp) alist;
+      puts ">\n";
+      List.iter (loop ~newl:true (tab^"  ")) l;
+      puts tab;
+      puts "</";
+      puts tag;
+      putc '>';
+      if newl then putc '\n';
+    | PCData text ->
+      buffer_pcdata tmp text;
+      if newl then putc '\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