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 (* Usage:                                                                   *)
  57 (*  pp tokens None     pretty prints the output on stdout                   *)
  58 (*  pp tokens (Some filename) pretty prints the output on the file filename *)
  59 let pp ?(quiet=false) strm fn =
  60  let channel = ref stdout in
  61  let rec pp_r m =
  62   parser
  63     [< 'Str a ; s >] ->
  64       print_spaces m ;
  65       fprint_string (a ^ "\n") ;
  66       pp_r m s
  67   | [< 'Empty(n,l) ; s >] ->
  68       print_spaces m ;
  69       fprint_string ("<" ^ n) ;
  70       List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
  71       fprint_string "/>\n" ;
  72       pp_r m s
  73   | [< 'NEmpty(n,l,c) ; s >] ->
  74       print_spaces m ;
  75       fprint_string ("<" ^ n) ;
  76       List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l;
  77       fprint_string ">\n" ;
  78       pp_r (m+1) c ;
  79       print_spaces m ;
  80       fprint_string ("</" ^ n ^ ">\n") ;
  81       pp_r m s
  82   | [< >] -> ()
  83  and print_spaces m =
  84   for i = 1 to m do fprint_string "  " done
  85  and fprint_string str =
  86   output_string !channel str
  87  in
  88   match fn with
  89      Some filename ->
  90        channel := open_out filename ;
  91        pp_r 0 strm ;
  92        close_out !channel ;
  93        if not quiet then
  94         begin
  95          print_string ("\nWriting on file \"" ^ filename ^
  96           "\" was succesfull\n");
  97          flush stdout
  98         end
  99    | None ->
 100        pp_r 0 strm
 101 ;;