diff options
Diffstat (limited to 'ide/xml_printer.ml')
-rw-r--r-- | ide/xml_printer.ml | 145 |
1 files changed, 145 insertions, 0 deletions
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 " "; + | '>' -> puts ">" + | '<' -> puts "<" + | '&' -> + if p < l - 1 && text.[p + 1] = '#' then + putc '&' + else + puts "&" + | '\'' -> puts "'" + | '"' -> puts """ + | 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 "<" + | '&' -> puts "&" + | 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 () |