1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145
(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \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 ()