aboutsummaryrefslogtreecommitdiff
path: root/ide/protocol/xml_printer.ml
diff options
context:
space:
mode:
authorMaxime Dénès2020-05-16 17:07:37 +0200
committerMaxime Dénès2020-06-02 18:53:33 +0200
commit33021618a06a94563d28691940f02a55bd9d358d (patch)
tree9d0cab0e9ffc2f1499ec1d49b142a758d7f80fee /ide/protocol/xml_printer.ml
parentdb768e6828af62e06eb03d36509be6f8fc1efbf3 (diff)
Move CoqIDE to its own folder
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
Diffstat (limited to 'ide/protocol/xml_printer.ml')
-rw-r--r--ide/protocol/xml_printer.ml147
1 files changed, 0 insertions, 147 deletions
diff --git a/ide/protocol/xml_printer.ml b/ide/protocol/xml_printer.ml
deleted file mode 100644
index f526618a6e..0000000000
--- a/ide/protocol/xml_printer.ml
+++ /dev/null
@@ -1,147 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * Copyright INRIA, CNRS and contributors *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-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 ()