diff options
| author | sacerdot | 2000-10-25 09:15:24 +0000 |
|---|---|---|
| committer | sacerdot | 2000-10-25 09:15:24 +0000 |
| commit | ff249870a9db77a6cbf20bcd839a346b2b749fec (patch) | |
| tree | 965eb5b28c1904571b9acaa223e6a60901ae5121 /contrib/xml/xml.mli | |
| parent | 0f754594a7452e9157b6fb1fdb9842d85e171f2f (diff) | |
xml contribution created.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@756 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml/xml.mli')
| -rw-r--r-- | contrib/xml/xml.mli | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/contrib/xml/xml.mli b/contrib/xml/xml.mli new file mode 100644 index 0000000000..a82c582f69 --- /dev/null +++ b/contrib/xml/xml.mli @@ -0,0 +1,35 @@ +(******************************************************************************) +(* *) +(* 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 *) +(* *) +(******************************************************************************) + +(* Tokens 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 token constructors make the code more readable *) +val xml_empty : string -> (string * string) list -> token Stream.t +val xml_nempty : + string -> (string * string) list -> token Stream.t -> token Stream.t +val xml_cdata : string -> token Stream.t + +(* The pretty printer for streams of token *) +(* Usage: *) +(* pp tokens None pretty prints the output on stdout *) +(* pp tokens (Some filename) pretty prints the output on the file filename *) +val pp : token Stream.t -> string option -> unit |
