helm/ocaml/xml/xml.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                     A tactic to print Coq objects in XML                   *)
  31 (*                                                                            *)
  32 (*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
  33 (*                                 18/10/2000                                 *)
  34 (*                                                                            *)
  35 (* This module defines a pretty-printer and the stream of commands to the pp  *)
  36 (*                                                                            *)
  37 (******************************************************************************)
  38
  39
  40 (* the type token for XML cdata, empty elements and not-empty elements *)
  41 (* Usage:                                                                *)
  42 (*  Str cdata                                                            *)
  43 (*  Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen]   *)
  44 (*  NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *)
  45 (*          content                                                      *)
  46 type token = Str of string
  47            | Empty of string * (string * string) list
  48            | NEmpty of string * (string * string) list * token Stream.t
  49 ;;
  50
  51 (* currified versions of the constructors make the code more readable *)
  52 let xml_empty name attrs = [< 'Empty(name,attrs) >]
  53 let xml_nempty name attrs content = [< 'NEmpty(name,attrs,content) >]
  54 let xml_cdata str = [< 'Str str >]
  55
  56 (** low level for other PPs: pretty print each token of strm applying 'f' to a
  57 canonical string representation of each token *)
  58 let pp_gen f strm =
  59  let rec pp_r m =
  60   parser
  61   | [< 'Str a ; s >] ->
  62       print_spaces m ;
  63       f (a ^ "\n") ;
  64       pp_r m s
  65   | [< 'Empty(n,l) ; s >] ->
  66       print_spaces m ;
  67       f ("<" ^ n) ;
  68       List.iter (fun (n,v) -> f (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
  69       f "/>\n" ;
  70       pp_r m s
  71   | [< 'NEmpty(n,l,c) ; s >] ->
  72       print_spaces m ;
  73       f ("<" ^ n) ;
  74       List.iter (fun (n,v) -> f (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
  75       f ">\n" ;
  76       pp_r (m+1) c ;
  77       print_spaces m ;
  78       f ("</" ^ n ^ ">\n") ;
  79       pp_r m s
  80   | [< >] -> ()
  81  and print_spaces m =
  82   for i = 1 to m do f "  " done
  83  in
  84  pp_r 0 strm
  85 ;;
  86
  87 (** pretty printer on output channels *)
  88 let pp_to_outchan strm oc =
  89   pp_gen (fun s -> output_string oc s) strm;
  90   flush oc
  91 ;;
  92
  93 (** pretty printer to string *)
  94 let pp_to_string strm =
  95   let buf = Buffer.create 10240 in
  96   pp_gen (Buffer.add_string buf) strm;
  97   Buffer.contents buf
  98 ;;
  99
 100 (** pretty printer to file *)
 101 (* Usage:                                                                   *)
 102 (*  pp tokens None     pretty prints the output on stdout                   *)
 103 (*  pp tokens (Some filename) pretty prints the output on the file filename *)
 104 let pp ?(quiet=false) strm fn =
 105   match fn with
 106   | Some filename ->
 107       let outchan = open_out filename in
 108       (try
 109         pp_to_outchan strm outchan;
 110       with e ->
 111         close_out outchan;
 112         raise e);
 113       close_out outchan;
 114       if not quiet then
 115         begin
 116           print_string ("\nWriting on file \"" ^ filename ^
 117             "\" was succesfull\n");
 118           flush stdout
 119         end
 120   | None -> pp_to_outchan strm stdout
 121 ;;