diff options
| author | letouzey | 2001-12-19 11:42:11 +0000 |
|---|---|---|
| committer | letouzey | 2001-12-19 11:42:11 +0000 |
| commit | d14df293d2696f00a8de137bea9fe3a89e0bdeb0 (patch) | |
| tree | 3b7407ed3564a95ab2dfcbc42eb47c93ba75affd /contrib/xml/xml.ml | |
| parent | e45a0752bce5712945332a85b34d487db7407f59 (diff) | |
reparation du make depend et du .depend
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2334 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml/xml.ml')
| -rw-r--r-- | contrib/xml/xml.ml | 80 |
1 files changed, 0 insertions, 80 deletions
diff --git a/contrib/xml/xml.ml b/contrib/xml/xml.ml deleted file mode 100644 index 60e16ab19b..0000000000 --- a/contrib/xml/xml.ml +++ /dev/null @@ -1,80 +0,0 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* A tactic to print Coq objects in XML *) -(* *) -(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *) -(* 18/10/2000 *) -(* *) -(* This module defines a pretty-printer and the stream of commands to the pp *) -(* *) -(******************************************************************************) - - -(* the type token for XML cdata, empty elements and not-empty elements *) -(* Usage: *) -(* Str cdata *) -(* Empty (element_name, [attrname1, value1 ; ... ; attrnamen, valuen] *) -(* NEmpty (element_name, [attrname1, value2 ; ... ; attrnamen, valuen], *) -(* content *) -type token = Str of string - | Empty of string * (string * string) list - | NEmpty of string * (string * string) list * token Stream.t -;; - -(* currified versions of the constructors make the code more readable *) -let xml_empty name attrs = [< 'Empty(name,attrs) >] -let xml_nempty name attrs content = [< 'NEmpty(name,attrs,content) >] -let xml_cdata str = [< 'Str str >] - -(* Usage: *) -(* pp tokens None pretty prints the output on stdout *) -(* pp tokens (Some filename) pretty prints the output on the file filename *) -let pp strm fn = - let channel = ref stdout in - let rec pp_r m = - parser - [< 'Str a ; s >] -> - print_spaces m ; - fprint_string (a ^ "\n") ; - pp_r m s - | [< 'Empty(n,l) ; s >] -> - print_spaces m ; - fprint_string ("<" ^ n) ; - List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l; - fprint_string "/>\n" ; - pp_r m s - | [< 'NEmpty(n,l,c) ; s >] -> - print_spaces m ; - fprint_string ("<" ^ n) ; - List.iter (function (n,v) -> fprint_string (" " ^ n ^ "=\"" ^ v ^ "\"")) l; - fprint_string ">\n" ; - pp_r (m+1) c ; - print_spaces m ; - fprint_string ("</" ^ n ^ ">\n") ; - pp_r m s - | [< >] -> () - and print_spaces m = - for i = 1 to m do fprint_string " " done - and fprint_string str = - output_string !channel str - in - match fn with - Some filename -> - let filename = filename ^ ".xml" in - channel := open_out filename ; - pp_r 0 strm ; - close_out !channel ; - print_string ("\nWriting on file \"" ^ filename ^ "\" was succesfull\n"); - flush stdout - | None -> - pp_r 0 strm -;; |