]> matita.cs.unibo.it Git - helm.git/commitdiff
This commit was manufactured by cvs2svn to create branch 'helm'.
authorno author <no.author@nowhere.it>
Wed, 10 Jan 2001 09:25:50 +0000 (09:25 +0000)
committerno author <no.author@nowhere.it>
Wed, 10 Jan 2001 09:25:50 +0000 (09:25 +0000)
17 files changed:
helm/DEVEL/mlminidom/.cvsignore [new file with mode: 0644]
helm/DEVEL/mlminidom/AUTHORS [new file with mode: 0644]
helm/DEVEL/mlminidom/COPYING [new file with mode: 0644]
helm/DEVEL/mlminidom/ChangeLog [new file with mode: 0644]
helm/DEVEL/mlminidom/Makefile.in [new file with mode: 0644]
helm/DEVEL/mlminidom/NEWS [new file with mode: 0644]
helm/DEVEL/mlminidom/README [new file with mode: 0644]
helm/DEVEL/mlminidom/configure.in [new file with mode: 0644]
helm/DEVEL/mlminidom/minidom.ml [new file with mode: 0644]
helm/DEVEL/mlminidom/minidom.mli [new file with mode: 0644]
helm/DEVEL/mlminidom/ml_minidom.c [new file with mode: 0644]
helm/DEVEL/mlminidom/ml_minidom.h [new file with mode: 0644]
helm/DEVEL/mlminidom/mlminidom-0.0.1-1.spec [new file with mode: 0644]
helm/DEVEL/mlminidom/ominidom.ml [new file with mode: 0644]
helm/DEVEL/mlminidom/ominidom.mli [new file with mode: 0644]
helm/DEVEL/mlminidom/test.ml [new file with mode: 0644]
helm/DEVEL/mlminidom/test.xml [new file with mode: 0644]

diff --git a/helm/DEVEL/mlminidom/.cvsignore b/helm/DEVEL/mlminidom/.cvsignore
new file mode 100644 (file)
index 0000000..90e9bb4
--- /dev/null
@@ -0,0 +1,6 @@
+*.cmi *.cmo *.cmx test test.opt
+configure
+config.status
+config.log
+config.cache
+Makefile
diff --git a/helm/DEVEL/mlminidom/AUTHORS b/helm/DEVEL/mlminidom/AUTHORS
new file mode 100644 (file)
index 0000000..3598094
--- /dev/null
@@ -0,0 +1,2 @@
+Luca Padovani <luca.padovani@cs.unibo.it>
+Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>
diff --git a/helm/DEVEL/mlminidom/COPYING b/helm/DEVEL/mlminidom/COPYING
new file mode 100644 (file)
index 0000000..d60c31a
--- /dev/null
@@ -0,0 +1,340 @@
+                   GNU GENERAL PUBLIC LICENSE
+                      Version 2, June 1991
+
+ Copyright (C) 1989, 1991 Free Software Foundation, Inc.
+     59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+                           Preamble
+
+  The licenses for most software are designed to take away your
+freedom to share and change it.  By contrast, the GNU General Public
+License is intended to guarantee your freedom to share and change free
+software--to make sure the software is free for all its users.  This
+General Public License applies to most of the Free Software
+Foundation's software and to any other program whose authors commit to
+using it.  (Some other Free Software Foundation software is covered by
+the GNU Library General Public License instead.)  You can apply it to
+your programs, too.
+
+  When we speak of free software, we are referring to freedom, not
+price.  Our General Public Licenses are designed to make sure that you
+have the freedom to distribute copies of free software (and charge for
+this service if you wish), that you receive source code or can get it
+if you want it, that you can change the software or use pieces of it
+in new free programs; and that you know you can do these things.
+
+  To protect your rights, we need to make restrictions that forbid
+anyone to deny you these rights or to ask you to surrender the rights.
+These restrictions translate to certain responsibilities for you if you
+distribute copies of the software, or if you modify it.
+
+  For example, if you distribute copies of such a program, whether
+gratis or for a fee, you must give the recipients all the rights that
+you have.  You must make sure that they, too, receive or can get the
+source code.  And you must show them these terms so they know their
+rights.
+
+  We protect your rights with two steps: (1) copyright the software, and
+(2) offer you this license which gives you legal permission to copy,
+distribute and/or modify the software.
+
+  Also, for each author's protection and ours, we want to make certain
+that everyone understands that there is no warranty for this free
+software.  If the software is modified by someone else and passed on, we
+want its recipients to know that what they have is not the original, so
+that any problems introduced by others will not reflect on the original
+authors' reputations.
+
+  Finally, any free program is threatened constantly by software
+patents.  We wish to avoid the danger that redistributors of a free
+program will individually obtain patent licenses, in effect making the
+program proprietary.  To prevent this, we have made it clear that any
+patent must be licensed for everyone's free use or not licensed at all.
+
+  The precise terms and conditions for copying, distribution and
+modification follow.
+\f
+                   GNU GENERAL PUBLIC LICENSE
+   TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
+
+  0. This License applies to any program or other work which contains
+a notice placed by the copyright holder saying it may be distributed
+under the terms of this General Public License.  The "Program", below,
+refers to any such program or work, and a "work based on the Program"
+means either the Program or any derivative work under copyright law:
+that is to say, a work containing the Program or a portion of it,
+either verbatim or with modifications and/or translated into another
+language.  (Hereinafter, translation is included without limitation in
+the term "modification".)  Each licensee is addressed as "you".
+
+Activities other than copying, distribution and modification are not
+covered by this License; they are outside its scope.  The act of
+running the Program is not restricted, and the output from the Program
+is covered only if its contents constitute a work based on the
+Program (independent of having been made by running the Program).
+Whether that is true depends on what the Program does.
+
+  1. You may copy and distribute verbatim copies of the Program's
+source code as you receive it, in any medium, provided that you
+conspicuously and appropriately publish on each copy an appropriate
+copyright notice and disclaimer of warranty; keep intact all the
+notices that refer to this License and to the absence of any warranty;
+and give any other recipients of the Program a copy of this License
+along with the Program.
+
+You may charge a fee for the physical act of transferring a copy, and
+you may at your option offer warranty protection in exchange for a fee.
+
+  2. You may modify your copy or copies of the Program or any portion
+of it, thus forming a work based on the Program, and copy and
+distribute such modifications or work under the terms of Section 1
+above, provided that you also meet all of these conditions:
+
+    a) You must cause the modified files to carry prominent notices
+    stating that you changed the files and the date of any change.
+
+    b) You must cause any work that you distribute or publish, that in
+    whole or in part contains or is derived from the Program or any
+    part thereof, to be licensed as a whole at no charge to all third
+    parties under the terms of this License.
+
+    c) If the modified program normally reads commands interactively
+    when run, you must cause it, when started running for such
+    interactive use in the most ordinary way, to print or display an
+    announcement including an appropriate copyright notice and a
+    notice that there is no warranty (or else, saying that you provide
+    a warranty) and that users may redistribute the program under
+    these conditions, and telling the user how to view a copy of this
+    License.  (Exception: if the Program itself is interactive but
+    does not normally print such an announcement, your work based on
+    the Program is not required to print an announcement.)
+\f
+These requirements apply to the modified work as a whole.  If
+identifiable sections of that work are not derived from the Program,
+and can be reasonably considered independent and separate works in
+themselves, then this License, and its terms, do not apply to those
+sections when you distribute them as separate works.  But when you
+distribute the same sections as part of a whole which is a work based
+on the Program, the distribution of the whole must be on the terms of
+this License, whose permissions for other licensees extend to the
+entire whole, and thus to each and every part regardless of who wrote it.
+
+Thus, it is not the intent of this section to claim rights or contest
+your rights to work written entirely by you; rather, the intent is to
+exercise the right to control the distribution of derivative or
+collective works based on the Program.
+
+In addition, mere aggregation of another work not based on the Program
+with the Program (or with a work based on the Program) on a volume of
+a storage or distribution medium does not bring the other work under
+the scope of this License.
+
+  3. You may copy and distribute the Program (or a work based on it,
+under Section 2) in object code or executable form under the terms of
+Sections 1 and 2 above provided that you also do one of the following:
+
+    a) Accompany it with the complete corresponding machine-readable
+    source code, which must be distributed under the terms of Sections
+    1 and 2 above on a medium customarily used for software interchange; or,
+
+    b) Accompany it with a written offer, valid for at least three
+    years, to give any third party, for a charge no more than your
+    cost of physically performing source distribution, a complete
+    machine-readable copy of the corresponding source code, to be
+    distributed under the terms of Sections 1 and 2 above on a medium
+    customarily used for software interchange; or,
+
+    c) Accompany it with the information you received as to the offer
+    to distribute corresponding source code.  (This alternative is
+    allowed only for noncommercial distribution and only if you
+    received the program in object code or executable form with such
+    an offer, in accord with Subsection b above.)
+
+The source code for a work means the preferred form of the work for
+making modifications to it.  For an executable work, complete source
+code means all the source code for all modules it contains, plus any
+associated interface definition files, plus the scripts used to
+control compilation and installation of the executable.  However, as a
+special exception, the source code distributed need not include
+anything that is normally distributed (in either source or binary
+form) with the major components (compiler, kernel, and so on) of the
+operating system on which the executable runs, unless that component
+itself accompanies the executable.
+
+If distribution of executable or object code is made by offering
+access to copy from a designated place, then offering equivalent
+access to copy the source code from the same place counts as
+distribution of the source code, even though third parties are not
+compelled to copy the source along with the object code.
+\f
+  4. You may not copy, modify, sublicense, or distribute the Program
+except as expressly provided under this License.  Any attempt
+otherwise to copy, modify, sublicense or distribute the Program is
+void, and will automatically terminate your rights under this License.
+However, parties who have received copies, or rights, from you under
+this License will not have their licenses terminated so long as such
+parties remain in full compliance.
+
+  5. You are not required to accept this License, since you have not
+signed it.  However, nothing else grants you permission to modify or
+distribute the Program or its derivative works.  These actions are
+prohibited by law if you do not accept this License.  Therefore, by
+modifying or distributing the Program (or any work based on the
+Program), you indicate your acceptance of this License to do so, and
+all its terms and conditions for copying, distributing or modifying
+the Program or works based on it.
+
+  6. Each time you redistribute the Program (or any work based on the
+Program), the recipient automatically receives a license from the
+original licensor to copy, distribute or modify the Program subject to
+these terms and conditions.  You may not impose any further
+restrictions on the recipients' exercise of the rights granted herein.
+You are not responsible for enforcing compliance by third parties to
+this License.
+
+  7. If, as a consequence of a court judgment or allegation of patent
+infringement or for any other reason (not limited to patent issues),
+conditions are imposed on you (whether by court order, agreement or
+otherwise) that contradict the conditions of this License, they do not
+excuse you from the conditions of this License.  If you cannot
+distribute so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you
+may not distribute the Program at all.  For example, if a patent
+license would not permit royalty-free redistribution of the Program by
+all those who receive copies directly or indirectly through you, then
+the only way you could satisfy both it and this License would be to
+refrain entirely from distribution of the Program.
+
+If any portion of this section is held invalid or unenforceable under
+any particular circumstance, the balance of the section is intended to
+apply and the section as a whole is intended to apply in other
+circumstances.
+
+It is not the purpose of this section to induce you to infringe any
+patents or other property right claims or to contest validity of any
+such claims; this section has the sole purpose of protecting the
+integrity of the free software distribution system, which is
+implemented by public license practices.  Many people have made
+generous contributions to the wide range of software distributed
+through that system in reliance on consistent application of that
+system; it is up to the author/donor to decide if he or she is willing
+to distribute software through any other system and a licensee cannot
+impose that choice.
+
+This section is intended to make thoroughly clear what is believed to
+be a consequence of the rest of this License.
+\f
+  8. If the distribution and/or use of the Program is restricted in
+certain countries either by patents or by copyrighted interfaces, the
+original copyright holder who places the Program under this License
+may add an explicit geographical distribution limitation excluding
+those countries, so that distribution is permitted only in or among
+countries not thus excluded.  In such case, this License incorporates
+the limitation as if written in the body of this License.
+
+  9. The Free Software Foundation may publish revised and/or new versions
+of the General Public License from time to time.  Such new versions will
+be similar in spirit to the present version, but may differ in detail to
+address new problems or concerns.
+
+Each version is given a distinguishing version number.  If the Program
+specifies a version number of this License which applies to it and "any
+later version", you have the option of following the terms and conditions
+either of that version or of any later version published by the Free
+Software Foundation.  If the Program does not specify a version number of
+this License, you may choose any version ever published by the Free Software
+Foundation.
+
+  10. If you wish to incorporate parts of the Program into other free
+programs whose distribution conditions are different, write to the author
+to ask for permission.  For software which is copyrighted by the Free
+Software Foundation, write to the Free Software Foundation; we sometimes
+make exceptions for this.  Our decision will be guided by the two goals
+of preserving the free status of all derivatives of our free software and
+of promoting the sharing and reuse of software generally.
+
+                           NO WARRANTY
+
+  11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY
+FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW.  EXCEPT WHEN
+OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES
+PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED
+OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
+MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.  THE ENTIRE RISK AS
+TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU.  SHOULD THE
+PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,
+REPAIR OR CORRECTION.
+
+  12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING
+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR
+REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,
+INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING
+OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED
+TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY
+YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER
+PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGES.
+
+                    END OF TERMS AND CONDITIONS
+\f
+           How to Apply These Terms to Your New Programs
+
+  If you develop a new program, and you want it to be of the greatest
+possible use to the public, the best way to achieve this is to make it
+free software which everyone can redistribute and change under these terms.
+
+  To do so, attach the following notices to the program.  It is safest
+to attach them to the start of each source file to most effectively
+convey the exclusion of warranty; and each file should have at least
+the "copyright" line and a pointer to where the full notice is found.
+
+    <one line to give the program's name and a brief idea of what it does.>
+    Copyright (C) <year>  <name of author>
+
+    This program is free software; you can redistribute it and/or modify
+    it under the terms of the GNU General Public License as published by
+    the Free Software Foundation; either version 2 of the License, or
+    (at your option) any later version.
+
+    This program is distributed in the hope that it will be useful,
+    but WITHOUT ANY WARRANTY; without even the implied warranty of
+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+    GNU General Public License for more details.
+
+    You should have received a copy of the GNU General Public License
+    along with this program; if not, write to the Free Software
+    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
+
+
+Also add information on how to contact you by electronic and paper mail.
+
+If the program is interactive, make it output a short notice like this
+when it starts in an interactive mode:
+
+    Gnomovision version 69, Copyright (C) year  name of author
+    Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'.
+    This is free software, and you are welcome to redistribute it
+    under certain conditions; type `show c' for details.
+
+The hypothetical commands `show w' and `show c' should show the appropriate
+parts of the General Public License.  Of course, the commands you use may
+be called something other than `show w' and `show c'; they could even be
+mouse-clicks or menu items--whatever suits your program.
+
+You should also get your employer (if you work as a programmer) or your
+school, if any, to sign a "copyright disclaimer" for the program, if
+necessary.  Here is a sample; alter the names:
+
+  Yoyodyne, Inc., hereby disclaims all copyright interest in the program
+  `Gnomovision' (which makes passes at compilers) written by James Hacker.
+
+  <signature of Ty Coon>, 1 April 1989
+  Ty Coon, President of Vice
+
+This General Public License does not permit incorporating your program into
+proprietary programs.  If your program is a subroutine library, you may
+consider it more useful to permit linking proprietary applications with the
+library.  If this is what you want to do, use the GNU Library General
+Public License instead of this License.
diff --git a/helm/DEVEL/mlminidom/ChangeLog b/helm/DEVEL/mlminidom/ChangeLog
new file mode 100644 (file)
index 0000000..e69de29
diff --git a/helm/DEVEL/mlminidom/Makefile.in b/helm/DEVEL/mlminidom/Makefile.in
new file mode 100644 (file)
index 0000000..e311c5e
--- /dev/null
@@ -0,0 +1,69 @@
+PACKAGE = @PACKAGE@
+VERSION = @MLMINIDOM_VERSION@
+LIBDIR = @OCAML_ROOT@
+INSTALLDIR = $(LIBDIR)/mlminidom
+OBJECTS = minidom.cmi minidom.cmo ml_minidom.o ominidom.cmi ominidom.cmo
+OBJECTS_OPT = minidom.cmx ominidom.cmx
+INST = minidom.o ominidom.o ml_minidom.h minidom.mli
+DIST_FILES = Makefile.in configure.in configure *.ml *.mli test.xml ml_minidom.c ml_minidom.h
+DOC_FILES = AUTHORS COPYING ChangeLog NEWS README
+
+all: $(OBJECTS) test
+
+opt: $(OBJECTS_OPT) test.opt
+
+dist:
+       rm -rf $(PACKAGE)-$(VERSION)
+       mkdir $(PACKAGE)-$(VERSION)
+       cp $(DIST_FILES) $(DOC_FILES) $(PACKAGE)-$(VERSION)
+       tar cvfz $(PACKAGE)-$(VERSION).tar.gz $(PACKAGE)-$(VERSION)
+       rm -rf $(PACKAGE)-$(VERSION)
+       
+ml_minidom.o: ml_minidom.c
+       gcc -c -I$(LIBDIR)/caml/ `glib-config --cflags` `minidom-config --cflags` $<
+
+minidom.cmi: minidom.mli
+       ocamlc -c $<
+
+minidom.cmo: minidom.ml minidom.cmi
+       ocamlc -c $<
+
+minidom.cmx: minidom.ml minidom.cmi
+       ocamlopt -c $<
+
+ominidom.cmi: ominidom.mli
+       ocamlc -c $<
+
+ominidom.cmo: ominidom.ml
+       ocamlc -c $<
+
+ominidom.cmx: ominidom.ml
+       ocamlopt -c $<
+
+test.cmo: test.ml minidom.cmo
+       ocamlc -c test.ml
+
+test.cmx: test.ml minidom.cmx
+       ocamlopt -c test.ml
+
+test: test.cmo minidom.cmo ml_minidom.o
+       ocamlc -custom -o test minidom.cmo test.cmo ml_minidom.o \
+        -cclib "`glib-config --libs` `minidom-config --libs`"
+
+test.opt: test.cmx minidom.cmx ml_minidom.o
+       ocamlopt -o test.opt minidom.cmx test.cmx ml_minidom.o \
+        -cclib "`glib-config --libs` `minidom-config --libs`"
+
+install:
+       if test -d $(INSTALLDIR); then : ; else mkdir -p $(INSTALLDIR); fi
+       cp $(OBJECTS) $(OBJECTS_OPT) $(INST) $(INSTALLDIR)
+
+uninstall:
+       rm -rf $(INSTALLDIR)
+
+clean:
+       rm -f *.o *.cm? test test.opt
+
+distclean: clean
+       rm -f configure config.log config.cache config.status Makefile
+
diff --git a/helm/DEVEL/mlminidom/NEWS b/helm/DEVEL/mlminidom/NEWS
new file mode 100644 (file)
index 0000000..e69de29
diff --git a/helm/DEVEL/mlminidom/README b/helm/DEVEL/mlminidom/README
new file mode 100644 (file)
index 0000000..c74b582
--- /dev/null
@@ -0,0 +1,9 @@
+This is the Ocaml binding for minidom.
+
+To compile and install:
+
+       ./configure
+       make
+       make opt
+       make install
+
diff --git a/helm/DEVEL/mlminidom/configure.in b/helm/DEVEL/mlminidom/configure.in
new file mode 100644 (file)
index 0000000..2f76115
--- /dev/null
@@ -0,0 +1,33 @@
+AC_INIT(minidom.ml)
+
+PACKAGE=mlminidom
+
+MLMINIDOM_MAJOR_VERSION=0
+MLMINIDOM_MINOR_VERSION=0
+MLMINIDOM_MICRO_VERSION=1
+MLMINIDOM_VERSION=$MLMINIDOM_MAJOR_VERSION.$MLMINIDOM_MINOR_VERSION.$MLMINIDOM_MICRO_VERSION
+
+AC_CHECK_PROG(HAVE_GLIB, glib-config, yes, no)
+if test $HAVE_GLIB = "no"; then
+  AC_MSG_ERROR(could not font glib configuration script, please make sure glib (dev) is installed)
+fi
+
+AC_CHECK_PROG(HAVE_MINIDOM, minidom-config, yes, no)
+if test $HAVE_MINIDOM = "no"; then
+  AC_MSG_ERROR(could not find minidom configuration script, please make sure minidom is installed)
+fi
+
+AC_CHECK_PROG(HAVE_OCAMLC, ocamlc, yes, no)
+if test $HAVE_OCAMLC = "no"; then
+  AC_MSG_ERROR(could not find ocamlc in PATH, please make sure ocaml is installed)
+fi
+
+AC_MSG_CHECKING("for the ocaml library dir")
+OCAML_ROOT=`ocamlc -v | grep "^Standard" | sed 's/^.*: *//'`
+AC_MSG_RESULT($OCAML_ROOT)
+
+AC_SUBST(PACKAGE)
+AC_SUBST(MLMINIDOM_VERSION)
+AC_SUBST(OCAML_ROOT)
+
+AC_OUTPUT([Makefile])
diff --git a/helm/DEVEL/mlminidom/minidom.ml b/helm/DEVEL/mlminidom/minidom.ml
new file mode 100644 (file)
index 0000000..118b0d0
--- /dev/null
@@ -0,0 +1,81 @@
+(* Copyright (C) 2000, Luca Padovani <luca.padovani@cs.unibo.it>.
+ *
+ * This file is part of mlminidom, the Ocaml binding for minidom.
+ * 
+ * mlminidom is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * mlminidom is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with mlminidom; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
+ * 
+ * For details, send a mail to the author.
+ *)
+
+type mDOMString
+type mDOMDoc
+type mDOMNode
+type mDOMAttr
+type mDOMEntity
+
+external string_of_mDOMString : mDOMString -> string = "ml_string_of_mDOMString"
+external mDOMString_of_string : string -> mDOMString = "ml_mDOMString_of_string"
+external mDOMString_eq : string -> string -> bool = "ml_mDOMString_eq"
+
+external doc_load : string -> mDOMDoc = "ml_doc_load"
+external doc_unload : mDOMDoc -> unit = "ml_doc_unload"
+
+external doc_new : mDOMString -> mDOMDoc = "ml_doc_new"
+external doc_get_root_node : mDOMDoc -> mDOMNode = "ml_doc_get_root_node"
+
+external doc_add_entity : mDOMDoc -> mDOMString -> mDOMString -> mDOMEntity = "ml_doc_add_entity"
+external doc_get_entity : mDOMDoc -> mDOMString -> mDOMEntity option = "ml_doc_get_entity"
+external doc_get_predefined_entity : mDOMDoc -> mDOMString -> mDOMEntity option = "ml_doc_get_predefined_entity"
+external entity_get_content : mDOMEntity -> mDOMString = "ml_entity_get_content"
+
+external node_is_text  : mDOMNode -> bool = "ml_node_is_text"
+external node_is_element : mDOMNode -> bool = "ml_node_is_element"
+external node_is_blank : mDOMNode -> bool = "ml_node_is_blank"
+external node_is_entity_ref : mDOMNode -> bool = "ml_node_is_entity_ref"
+external node_get_type : mDOMNode -> int = "ml_node_get_type"
+external node_get_name : mDOMNode -> mDOMString option = "ml_node_get_name"
+external node_get_ns_uri : mDOMNode -> mDOMString option = "ml_node_get_ns_uri"
+external node_get_attribute : mDOMNode -> mDOMString -> mDOMString option = "ml_node_get_attribute"
+external node_get_attribute_ns : mDOMNode -> mDOMString -> mDOMString -> mDOMString option = "ml_node_get_attribute_ns"
+external node_get_content : mDOMNode -> mDOMString option = "ml_node_get_content"
+external node_get_parent : mDOMNode -> mDOMNode option = "ml_node_get_parent"
+external node_get_prev_sibling : mDOMNode -> mDOMNode option = "ml_node_get_prev_sibling"
+external node_get_next_sibling : mDOMNode -> mDOMNode option = "ml_node_get_next_sibling"
+external node_get_first_child : mDOMNode -> mDOMNode option = "ml_node_get_first_child"
+external node_get_first_attribute : mDOMNode -> mDOMAttr option = "ml_node_get_first_attribute"
+external node_is_first : mDOMNode -> bool = "ml_node_is_first"
+external node_is_last : mDOMNode -> bool = "ml_node_is_last"
+
+external attr_get_name : mDOMAttr -> mDOMString option = "ml_attr_get_name"
+external attr_get_ns_uri : mDOMAttr -> mDOMString option = "ml_attr_get_ns_uri"
+external attr_get_value : mDOMAttr -> mDOMString option = "ml_attr_get_value"
+external attr_get_prev_sibling : mDOMAttr -> mDOMAttr option = "ml_attr_get_prev_sibling"
+external attr_get_next_sibling : mDOMAttr -> mDOMAttr option = "ml_attr_get_next_sibling"
+external attr_get_parent : mDOMAttr -> mDOMNode option = "ml_attr_get_parent"
+
+let rec node_list_of_node_first =
+  function None -> []
+  |        Some node -> node :: (node_list_of_node_first (node_get_next_sibling node))
+
+let rec attr_list_of_attr_first =
+  function None -> []
+  |        Some attr -> attr :: (attr_list_of_attr_first (attr_get_next_sibling attr))
+  
+let node_get_children node =
+  (node_list_of_node_first (node_get_first_child node))
+
+let node_get_attributes node =
+  (attr_list_of_attr_first (node_get_first_attribute node))
+
diff --git a/helm/DEVEL/mlminidom/minidom.mli b/helm/DEVEL/mlminidom/minidom.mli
new file mode 100644 (file)
index 0000000..36355af
--- /dev/null
@@ -0,0 +1,70 @@
+(* Copyright (C) 2000, Luca Padovani <luca.padovani@cs.unibo.it>.
+ *
+ * This file is part of mlminidom, the Ocaml binding for minidom.
+ * 
+ * mlminidom is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * mlminidom is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with mlminidom; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
+ * 
+ * For details, send a mail to the author.
+ *)
+
+type mDOMString
+type mDOMDoc
+type mDOMNode
+type mDOMAttr
+type mDOMEntity
+
+external string_of_mDOMString : mDOMString -> string = "ml_string_of_mDOMString"
+external mDOMString_of_string : string -> mDOMString = "ml_mDOMString_of_string"
+external mDOMString_eq : string -> string -> bool = "ml_mDOMString_eq"
+
+external doc_load : string -> mDOMDoc = "ml_doc_load"
+external doc_unload : mDOMDoc -> unit = "ml_doc_unload"
+
+external doc_new : mDOMString -> mDOMDoc = "ml_doc_new"
+external doc_get_root_node : mDOMDoc -> mDOMNode = "ml_doc_get_root_node"
+
+external doc_add_entity : doc:mDOMDoc -> name:mDOMString -> content:mDOMString -> mDOMEntity = "ml_doc_add_entity"
+external doc_get_entity : doc:mDOMDoc -> name:mDOMString -> mDOMEntity option = "ml_doc_get_entity"
+external doc_get_predefined_entity : doc:mDOMDoc -> name:mDOMString -> mDOMEntity option = "ml_doc_get_predefined_entity"
+external entity_get_content : mDOMEntity -> mDOMString = "ml_entity_get_content"
+
+external node_is_text  : mDOMNode -> bool = "ml_node_is_text"
+external node_is_element : mDOMNode -> bool = "ml_node_is_element"
+external node_is_blank : mDOMNode -> bool = "ml_node_is_blank"
+external node_is_entity_ref : mDOMNode -> bool = "ml_node_is_entity_ref"
+external node_get_type : mDOMNode -> int = "ml_node_get_type"
+external node_get_name : mDOMNode -> mDOMString option = "ml_node_get_name"
+external node_get_ns_uri : mDOMNode -> mDOMString option = "ml_node_get_ns_uri"
+external node_get_attribute : node:mDOMNode -> name:mDOMString -> mDOMString option = "ml_node_get_attribute"
+external node_get_attribute_ns : node:mDOMNode -> name:mDOMString -> ns_uri:mDOMString -> mDOMString option = "ml_node_get_attribute_ns"
+external node_get_content : mDOMNode -> mDOMString option = "ml_node_get_content"
+external node_get_parent : mDOMNode -> mDOMNode option = "ml_node_get_parent"
+external node_get_prev_sibling : mDOMNode -> mDOMNode option = "ml_node_get_prev_sibling"
+external node_get_next_sibling : mDOMNode -> mDOMNode option = "ml_node_get_next_sibling"
+external node_get_first_child : mDOMNode -> mDOMNode option = "ml_node_get_first_child"
+external node_get_first_attribute : mDOMNode -> mDOMAttr option = "ml_node_get_first_attribute"
+external node_is_first : mDOMNode -> bool = "ml_node_is_first"
+external node_is_last : mDOMNode -> bool = "ml_node_is_last"
+
+external attr_get_name : mDOMAttr -> mDOMString option = "ml_attr_get_name"
+external attr_get_ns_uri : mDOMAttr -> mDOMString option = "ml_attr_get_ns_uri"
+external attr_get_value : mDOMAttr -> mDOMString option = "ml_attr_get_value"
+external attr_get_prev_sibling : mDOMAttr -> mDOMAttr option = "ml_attr_get_prev_sibling"
+external attr_get_next_sibling : mDOMAttr -> mDOMAttr option = "ml_attr_get_next_sibling"
+external attr_get_parent : mDOMAttr -> mDOMNode option = "ml_attr_get_parent"
+
+val node_get_children : mDOMNode -> mDOMNode list
+val node_get_attributes : mDOMNode -> mDOMAttr list
+
diff --git a/helm/DEVEL/mlminidom/ml_minidom.c b/helm/DEVEL/mlminidom/ml_minidom.c
new file mode 100644 (file)
index 0000000..7e304cc
--- /dev/null
@@ -0,0 +1,308 @@
+/* Copyright (C) 2000, Luca Padovani <luca.padovani@cs.unibo.it>.
+ *
+ * This file is part of mlminidom, the Ocaml binding for minidom.
+ * 
+ * mlminidom is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * mlminidom is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with mlminidom; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
+ * 
+ * For details, send a mail to the author.
+ */
+
+#include <assert.h>
+#include <mlvalues.h>
+#include <memory.h>
+
+#include "minidom.h"
+
+#define Val_ptr(p)        ((value) (p))
+#define Val_option(p,f)   ((p != NULL) ? ml_some(f(p)) : Val_unit)
+#define Val_mDOMString(s) (copy_string((char*) (s)))
+#define mDOMString_val(v) ((mDOMStringRef) String_val(v))
+
+static value
+ml_some(value v)
+{
+  CAMLparam1(v);
+  value ret = alloc_small(1,0);
+  Field(ret,0) = v;
+  CAMLreturn(ret);
+}
+
+value
+ml_string_of_mDOMString(value s)
+{
+  CAMLparam1(s);
+  CAMLreturn(s);
+}
+
+value
+ml_mDOMString_of_string(value s)
+{
+  CAMLparam1(s);
+  CAMLreturn(s);
+}
+
+value
+ml_doc_load(value file_name)
+{
+  mDOMDocRef doc_ref;
+
+  CAMLparam1(file_name);
+
+  doc_ref = mdom_load(String_val(file_name), FALSE, NULL);
+  if (doc_ref == NULL) failwith("minidom: could not load document");
+
+  CAMLreturn((value) doc_ref);
+}
+
+value
+ml_doc_unload(value doc)
+{
+  CAMLparam1(doc);
+
+  mdom_unload((mDOMDocRef) doc);
+
+  CAMLreturn(Val_unit);
+}
+
+value
+ml_doc_new(value s)
+{
+  mDOMDocRef doc_ref;
+
+  CAMLparam1(s);
+
+  doc_ref = mdom_doc_new(mDOMString_val(s));
+  if (doc_ref == NULL) failwith("minidom: could not create new document");
+
+  CAMLreturn((value) doc_ref);
+}
+
+
+value
+ml_doc_get_root_node(value doc)
+{
+  mDOMNodeRef root;
+
+  CAMLparam1(doc);
+  root = mdom_doc_get_root_node((mDOMDocRef) doc);
+  if (root == NULL) failwith("minidom: document has no root node!");
+
+  CAMLreturn((value) root);
+}
+
+value
+ml_doc_add_entity(value doc, value name, value content)
+{
+  mDOMEntityRef ent;
+
+  CAMLparam3(doc, name, content);
+  ent = mdom_doc_add_entity((mDOMDocRef) doc, mDOMString_val(name), mDOMString_val(content));
+  if (ent == NULL) failwith("minidom: could not add entity");
+
+  CAMLreturn((value) ent);
+}
+
+value
+ml_doc_get_entity(value doc, value name)
+{
+  mDOMEntityRef ent;
+
+  CAMLparam2(doc, name);
+  ent = mdom_doc_get_entity((mDOMDocRef) doc, mDOMString_val(name));
+
+  CAMLreturn(Val_option(ent, Val_ptr));
+}
+
+value
+ml_doc_get_predefined_entity(value name)
+{
+  mDOMEntityRef ent;
+
+  CAMLparam1(name);
+  ent = mdom_get_predefined_entity(mDOMString_val(name));
+
+  CAMLreturn(Val_option(ent, Val_ptr));
+}
+
+value
+ml_entity_get_content(value ent)
+{
+  CAMLparam1(ent);
+  CAMLreturn(Val_mDOMString(mdom_entity_get_content((mDOMEntityRef) ent)));
+}
+
+value
+ml_node_is_text(value node)
+{
+  CAMLparam1(node);
+  CAMLreturn(Val_bool(mdom_node_is_text((mDOMNodeRef) node)));
+}
+
+value
+ml_node_is_element(value node)
+{
+  CAMLparam1(node);
+  CAMLreturn(Val_bool(mdom_node_is_element((mDOMNodeRef) node)));
+}
+
+value
+ml_node_is_blank(value node)
+{
+  CAMLparam1(node);
+  CAMLreturn(Val_bool(mdom_node_is_blank((mDOMNodeRef) node)));
+}
+
+value
+ml_node_is_entity_ref(value node)
+{
+  CAMLparam1(node);
+  CAMLreturn(Val_bool(mdom_node_is_entity_ref((mDOMNodeRef) node)));
+}
+
+value
+ml_node_get_type(value node)
+{
+  CAMLparam1(node);
+  CAMLreturn(Val_int(mdom_node_get_type((mDOMNodeRef) node)));
+}
+
+value
+ml_node_get_name(value node)
+{
+  CAMLparam1(node);
+  CAMLreturn(Val_option(mdom_node_get_name((mDOMNodeRef) node), Val_mDOMString));
+}
+
+value
+ml_node_get_content(value node)
+{
+  CAMLparam1(node);
+  CAMLreturn(Val_option(mdom_node_get_content((mDOMNodeRef) node), Val_mDOMString));
+}
+
+value
+ml_node_get_ns_uri(value node)
+{
+  CAMLparam1(node);
+  CAMLreturn(Val_option(mdom_node_get_ns_uri((mDOMNodeRef) node), Val_mDOMString));
+}
+
+value
+ml_node_get_attribute(value node, value name)
+{
+  CAMLparam2(node,name);
+  CAMLreturn(Val_option(mdom_node_get_attribute((mDOMNodeRef) node, String_val(name)), Val_mDOMString));
+}
+
+value
+ml_node_get_attribute_ns(value node, value name, value ns_uri)
+{
+  CAMLparam2(node,name);
+  CAMLreturn(Val_option(mdom_node_get_attribute_ns((mDOMNodeRef) node,
+                                                  String_val(name),
+                                                  String_val(ns_uri)), Val_mDOMString));
+}
+
+value
+ml_node_get_parent(value node)
+{
+  CAMLparam1(node);
+  CAMLreturn(Val_option(mdom_node_get_parent((mDOMNodeRef) node), Val_ptr));
+}
+
+value
+ml_node_get_prev_sibling(value node)
+{
+  CAMLparam1(node);
+  CAMLreturn(Val_option(mdom_node_get_prev_sibling((mDOMNodeRef) node), Val_ptr));
+}
+
+value
+ml_node_get_next_sibling(value node)
+{
+  CAMLparam1(node);
+  CAMLreturn(Val_option(mdom_node_get_next_sibling((mDOMNodeRef) node), Val_ptr));
+}
+
+value
+ml_node_get_first_child(value node)
+{
+  CAMLparam1(node);
+  CAMLreturn(Val_option(mdom_node_get_first_child((mDOMNodeRef) node), Val_ptr));
+}
+
+value
+ml_node_get_first_attribute(value node)
+{
+  CAMLparam1(node);
+  CAMLreturn(Val_option(mdom_node_get_first_attribute((mDOMNodeRef) node), Val_ptr));
+}
+
+value
+ml_node_is_first(value node)
+{
+  CAMLparam1(node);
+  CAMLreturn(Val_bool(mdom_node_is_first((mDOMNodeRef) node)));
+}
+
+value
+ml_node_is_last(value node)
+{
+  CAMLparam1(node);
+  CAMLreturn(Val_bool(mdom_node_is_last((mDOMNodeRef) node)));
+}
+
+value
+ml_attr_get_name(value attr)
+{
+  CAMLparam1(attr);
+  CAMLreturn(Val_option(mdom_attr_get_name((mDOMAttrRef) attr), Val_mDOMString));
+}
+
+value
+ml_attr_get_ns_uri(value attr)
+{
+  CAMLparam1(attr);
+  CAMLreturn(Val_option(mdom_attr_get_ns_uri((mDOMAttrRef) attr), Val_mDOMString));
+}
+
+value
+ml_attr_get_value(value attr)
+{
+  CAMLparam1(attr);
+  CAMLreturn(Val_option(mdom_attr_get_value((mDOMAttrRef) attr), Val_mDOMString));
+}
+
+value
+ml_attr_get_prev_sibling(value attr)
+{
+  CAMLparam1(attr);
+  CAMLreturn(Val_option(mdom_attr_get_prev_sibling((mDOMAttrRef) attr), Val_ptr));
+}
+
+value
+ml_attr_get_next_sibling(value attr)
+{
+  CAMLparam1(attr);
+  CAMLreturn(Val_option(mdom_attr_get_next_sibling((mDOMAttrRef) attr), Val_ptr));
+}
+
+value
+ml_attr_get_parent(value attr)
+{
+  CAMLparam1(attr);
+  CAMLreturn(Val_option(mdom_attr_get_parent((mDOMAttrRef) attr), Val_ptr));
+}
+
diff --git a/helm/DEVEL/mlminidom/ml_minidom.h b/helm/DEVEL/mlminidom/ml_minidom.h
new file mode 100644 (file)
index 0000000..4b92566
--- /dev/null
@@ -0,0 +1,38 @@
+/* Copyright (C) 2000, Luca Padovani <luca.padovani@cs.unibo.it>.
+ *
+ * This file is part of mlminidom, the Ocaml binding for minidom.
+ * 
+ * mlminidom is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * mlminidom is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with mlminidom; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
+ * 
+ * For details, send a mail to the author.
+ */
+
+#ifndef ml_minidom_h
+#define ml_minidom_h
+
+#define Val_ptr(p)        ((value) (p))
+#ifndef Val_option
+#define Val_option(p,f)   ((p != NULL) ? ml_some(f(p)) : Val_unit)
+#endif /* Val_option */
+#define Val_mDOMString(s) (copy_string((char*) (s)))
+#define mDOMString_val(v) ((mDOMStringRef) String_val(v))
+#define mDOMNode_val(v) ((mDOMNodeRef) v)
+
+#define mDOMNode_option_mDOMNodeRef(p) (((p) != NULL) ? ml_some((value) (p)) : Val_unit)
+#define mDOMNodeRef_mDOMNode_option(v) ((v == Val_unit) ? NULL : (mDOMNodeRef)Field((v),0))
+#define Val_mDOMNodeRef(p)             (mDOMNode_option_mDOMNodeRef(p))
+#define mDOMNodeRef_val(v)             (mDOMNodeRef_mDOMNode_option(v))
+
+#endif /* ml_minidom_h */
diff --git a/helm/DEVEL/mlminidom/mlminidom-0.0.1-1.spec b/helm/DEVEL/mlminidom/mlminidom-0.0.1-1.spec
new file mode 100644 (file)
index 0000000..3336a48
--- /dev/null
@@ -0,0 +1,27 @@
+Summary: The Ocaml binding for the minidom library
+Name: mlminidom
+Version: 0.0.1
+Release: 1
+Copyright: GPL
+URL: http://www.cs.unibo.it/helm
+Packager: Luca Padovani <luca.padovani@cs.unibo.it>
+Requires: ocaml >= 3.00, minidom >= 0.0.1, glib, glib-devel 
+Group: Applications/Publishing
+Source: www.cs.unibo.it:/~lpadovan/mml-widget/mlminidom-0.0.1.tar.gz
+%description
+The Ocaml binding for the minidom library
+
+%prep
+%setup
+
+%build
+./configure
+
+%install
+make
+make opt
+make install
+
+%files
+%doc AUTHORS COPYING ChangeLog NEWS README
+/usr/lib/ocaml/mlminidom
diff --git a/helm/DEVEL/mlminidom/ominidom.ml b/helm/DEVEL/mlminidom/ominidom.ml
new file mode 100644 (file)
index 0000000..343dfa3
--- /dev/null
@@ -0,0 +1,176 @@
+(* Copyright (C) 2000, Luca Padovani <luca.padovani@cs.unibo.it>.
+ *
+ * This file is part of mlminidom, the Ocaml binding for minidom.
+ * 
+ * mlminidom is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * mlminidom is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with mlminidom; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
+ * 
+ * For details, send a mail to the author.
+ *)
+
+exception Node_has_no_parent;;
+exception Node_has_no_sibling of string;;
+exception Node_has_no_children;;
+exception Node_has_no_attributes;;
+exception Attribute_has_no_sibling of string;;
+exception Attribute_has_no_parent;;
+exception Undefined_entity;;
+
+let option_to_exception v e =
+  match v with
+    Some x -> x
+  | None   -> raise e
+;;
+
+class o_mDOMString (str: Minidom.mDOMString) =
+  object
+    method get_dom_string = str
+    method get_string = Minidom.string_of_mDOMString str
+  end;;
+  
+let o_mDOMString_of_string str =
+  new o_mDOMString (Minidom.mDOMString_of_string str)
+
+class o_mDOMEntity (ent : Minidom.mDOMEntity) =
+  object
+    method get_dom_entity = ent
+    method get_content =
+      new o_mDOMString (Minidom.entity_get_content ent)
+  end
+;;
+
+class o_mDOMDoc (doc : Minidom.mDOMDoc) =
+  object
+    method get_dom_doc = doc
+
+    method get_root_node =
+      new o_mDOMNode (Minidom.doc_get_root_node doc)
+    method add_entity (name : o_mDOMString) (value : o_mDOMString) =
+      new o_mDOMEntity
+        (Minidom.doc_add_entity doc
+         (name#get_dom_string) (value#get_dom_string)
+       )
+    method get_entity (name : o_mDOMString) =
+      match Minidom.doc_get_entity doc (name#get_dom_string) with
+      | Some x -> new o_mDOMEntity x
+      | None -> raise Undefined_entity
+    method get_predefined_entity (name : o_mDOMString) =
+      match Minidom.doc_get_predefined_entity doc (name#get_dom_string) with
+      | Some x -> new o_mDOMEntity x
+      | None -> raise Undefined_entity
+  end
+and o_mDOMNode (node : Minidom.mDOMNode) =
+  object
+    method get_dom_node = node
+
+    method is_text = Minidom.node_is_text node
+    method is_element = Minidom.node_is_element node
+    method is_blank = Minidom.node_is_blank node
+    method is_entity_ref = Minidom.node_is_entity_ref node
+
+    method get_type = Minidom.node_get_type node
+    method get_name = 
+      match Minidom.node_get_name node with
+      | Some x -> Some (new o_mDOMString x)
+      | None   -> None
+    method get_ns_uri =
+      match Minidom.node_get_ns_uri node with
+      | Some x -> Some (new o_mDOMString x)
+      | None   -> None
+    method get_attribute (name : o_mDOMString) =
+      match Minidom.node_get_attribute node (name#get_dom_string) with
+      | Some x -> Some (new o_mDOMString x)
+      | None   -> None
+    method get_attribute_ns (name : o_mDOMString) (uri : o_mDOMString) =
+      match 
+        Minidom.node_get_attribute_ns node
+         (name#get_dom_string) (uri#get_dom_string)
+      with
+      | Some x -> Some (new o_mDOMString x)
+      | None   -> None
+    method get_content =
+      match Minidom.node_get_content node with
+      | Some x -> Some (new o_mDOMString x)
+      | None   -> None
+    method get_parent =
+      new o_mDOMNode
+       (option_to_exception (Minidom.node_get_parent node) Node_has_no_parent)
+    method get_prev_sibling =
+      new o_mDOMNode
+       (option_to_exception
+        (Minidom.node_get_prev_sibling node)
+        (Node_has_no_sibling "left")
+       )
+    method get_next_sibling =
+      new o_mDOMNode
+       (option_to_exception
+        (Minidom.node_get_next_sibling node)
+        (Node_has_no_sibling "right")
+       )
+    method get_first_child =
+      new o_mDOMNode
+       (option_to_exception
+        (Minidom.node_get_first_child node)
+        (Node_has_no_children)
+       )
+    method get_first_attribute =
+      new o_mDOMAttr
+       (option_to_exception
+         (Minidom.node_get_first_attribute node)
+         (Node_has_no_attributes)
+       )
+    method is_first = Minidom.node_is_first node
+    method is_last = Minidom.node_is_last node
+
+    method get_children =
+      List.map (function x -> new o_mDOMNode x) (Minidom.node_get_children node)
+    method get_attributes = List.map
+      (function x -> new o_mDOMAttr x) (Minidom.node_get_attributes node)
+  end
+and o_mDOMAttr (attr : Minidom.mDOMAttr) =
+  object
+    method get_dom_attr = attr
+
+    method get_name =
+      match Minidom.attr_get_name attr with
+      | Some x -> Some (new o_mDOMString x)
+      | None   -> None
+    method get_ns_uri =
+      match Minidom.attr_get_ns_uri attr with
+      | Some x -> Some (new o_mDOMString x)
+      | None   -> None
+    method get_value =
+      match Minidom.attr_get_value attr with
+      | Some x -> Some (new o_mDOMString x)
+      | None   -> None
+    method get_prev_sibling =
+      new o_mDOMAttr
+        (option_to_exception
+         (Minidom.attr_get_prev_sibling attr)
+         (Attribute_has_no_sibling "left")
+       )
+    method get_next_sibling =
+      new o_mDOMAttr
+        (option_to_exception
+         (Minidom.attr_get_next_sibling attr)
+         (Attribute_has_no_sibling "right")
+       )
+    method get_parent =
+      new o_mDOMNode
+        (option_to_exception
+         (Minidom.attr_get_parent attr) Attribute_has_no_parent
+       )
+  end
+;;
+    
diff --git a/helm/DEVEL/mlminidom/ominidom.mli b/helm/DEVEL/mlminidom/ominidom.mli
new file mode 100644 (file)
index 0000000..42b7d67
--- /dev/null
@@ -0,0 +1,85 @@
+(* Copyright (C) 2000, Luca Padovani <luca.padovani@cs.unibo.it>.
+ *
+ * This file is part of mlminidom, the Ocaml binding for minidom.
+ * 
+ * mlminidom is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * mlminidom is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with mlminidom; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
+ * 
+ * For details, send a mail to the author.
+ *)
+
+exception Node_has_no_parent
+exception Node_has_no_sibling of string
+exception Node_has_no_children
+exception Node_has_no_attributes
+exception Attribute_has_no_sibling of string
+exception Attribute_has_no_parent
+exception Undefined_entity
+
+class o_mDOMString : Minidom.mDOMString ->
+  object
+    method get_dom_string : Minidom.mDOMString
+    method get_string : string
+  end
+
+val o_mDOMString_of_string : string -> o_mDOMString
+
+class o_mDOMEntity : Minidom.mDOMEntity ->
+  object
+    method get_content : o_mDOMString
+    method get_dom_entity : Minidom.mDOMEntity
+  end
+
+class o_mDOMDoc : Minidom.mDOMDoc ->
+  object
+    method add_entity : o_mDOMString -> o_mDOMString -> o_mDOMEntity
+    method get_dom_doc : Minidom.mDOMDoc
+    method get_entity : o_mDOMString -> o_mDOMEntity
+    method get_predefined_entity : o_mDOMString -> o_mDOMEntity
+    method get_root_node : o_mDOMNode
+  end
+and o_mDOMNode : Minidom.mDOMNode ->
+  object
+    method get_attribute : o_mDOMString -> o_mDOMString option
+    method get_attribute_ns :
+      o_mDOMString -> o_mDOMString -> o_mDOMString option
+    method get_attributes : o_mDOMAttr list
+    method get_children : o_mDOMNode list
+    method get_content : o_mDOMString option
+    method get_dom_node : Minidom.mDOMNode
+    method get_first_attribute : o_mDOMAttr
+    method get_first_child : o_mDOMNode
+    method get_name : o_mDOMString option
+    method get_next_sibling : o_mDOMNode
+    method get_ns_uri : o_mDOMString option
+    method get_parent : o_mDOMNode
+    method get_prev_sibling : o_mDOMNode
+    method get_type : int
+    method is_blank : bool
+    method is_element : bool
+    method is_entity_ref : bool
+    method is_first : bool
+    method is_last : bool
+    method is_text : bool
+  end
+and o_mDOMAttr : Minidom.mDOMAttr ->
+  object
+    method get_dom_attr : Minidom.mDOMAttr
+    method get_name : o_mDOMString option
+    method get_next_sibling : o_mDOMAttr
+    method get_ns_uri : o_mDOMString option
+    method get_parent : o_mDOMNode
+    method get_prev_sibling : o_mDOMAttr
+    method get_value : o_mDOMString option
+  end
diff --git a/helm/DEVEL/mlminidom/test.ml b/helm/DEVEL/mlminidom/test.ml
new file mode 100644 (file)
index 0000000..1a239f8
--- /dev/null
@@ -0,0 +1,104 @@
+(* Copyright (C) 2000, Luca Padovani <luca.padovani@cs.unibo.it>.
+ *
+ * This file is part of mlminidom, the Ocaml binding for minidom.
+ * 
+ * mlminidom is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * mlminidom is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with mlminidom; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
+ * 
+ * For details, send a mail to the author.
+ *)
+
+let doc = Minidom.doc_load "test.xml"
+
+let root = Minidom.doc_get_root_node doc
+
+let check_attribute_ns attr =
+  Printf.printf "\n\n";
+  let ns_uri = Minidom.attr_get_ns_uri attr
+  and attr_name = Minidom.attr_get_name attr
+  and attr_value = Minidom.attr_get_value attr
+  and parent = Minidom.attr_get_parent attr
+  in
+  match parent,ns_uri,attr_name,attr_value with
+    Some parent_node,Some uri,Some attribute_name,Some attribute_value ->
+      let attr_value = Minidom.node_get_attribute_ns parent_node attribute_name uri
+      in begin
+        match attr_value with
+          Some attr1 ->
+           Printf.printf "found the attribute with ns %s (was %s)\n"
+              (Minidom.string_of_mDOMString attr1) (Minidom.string_of_mDOMString attribute_value)
+        | None ->
+           Printf.printf "attribute not found (uri was %s)!!!!\n" (Minidom.string_of_mDOMString uri)
+      end
+  | _ ->
+      Printf.printf "parent_node == NULL || uri == NULL || attribute_name == NULL || attribute_value == NULL\n"
+;;
+    
+let print_attribute attr =
+  check_attribute_ns attr;
+  let ns_uri = Minidom.attr_get_ns_uri attr
+  in
+  begin
+    match ns_uri with
+      Some uri -> Printf.printf " %s:" (Minidom.string_of_mDOMString uri);
+    | None -> ()
+  end;
+  match ((Minidom.attr_get_name attr), (Minidom.attr_get_value attr)) with
+    (Some attr_name, Some attr_value) ->
+      Printf.printf " %s=\"%s\"" (Minidom.string_of_mDOMString attr_name) (Minidom.string_of_mDOMString attr_value) 
+  | (Some attr_name, _) ->
+      Printf.printf " ??? attribute %s has no value !!!" (Minidom.string_of_mDOMString attr_name)
+  | (_,_) ->
+      Printf.printf " ??? very strange attribute !!!"
+;;
+
+let rec print_node n node =
+  if Minidom.node_is_blank node then ()
+  else if Minidom.node_is_element node then begin
+    match Minidom.node_get_name node with
+      Some node_name -> 
+        begin
+          let children = Minidom.node_get_children node
+          and attributes = Minidom.node_get_attributes node
+          and ns_uri = Minidom.node_get_ns_uri node
+          and is_first,is_last = (Minidom.node_is_first node), (Minidom.node_is_last node)
+          in
+          for i = 1 to n do print_char ' ' done;
+          Printf.printf "<";
+          begin
+            match ns_uri with
+              Some uri -> Printf.printf "%s:" (Minidom.string_of_mDOMString uri)
+            | None     -> ()
+          end;
+          Printf.printf "%s" (Minidom.string_of_mDOMString node_name);
+          List.iter print_attribute attributes;
+          Printf.printf ">\n";
+          List.iter (print_node (n + 2)) children;
+          for i = 1 to n do print_char ' ' done;
+          Printf.printf "</%s>\n" (Minidom.string_of_mDOMString node_name)
+        end
+    | None -> Printf.printf "??? this node has no name !!!\n"
+  end else if Minidom.node_is_text node then begin
+    match Minidom.node_get_content node with
+      Some node_content ->
+        for i = 1 to n do print_char ' ' done;
+        Printf.printf "%s\n" (Minidom.string_of_mDOMString node_content)
+    | None -> Printf.printf "??? this node has no content !!!\n"
+  end else begin
+    Printf.printf "don't know how to manage a node with type %d\n" (Minidom.node_get_type node)
+  end
+;;
+  
+print_node 0 root;;
+
diff --git a/helm/DEVEL/mlminidom/test.xml b/helm/DEVEL/mlminidom/test.xml
new file mode 100644 (file)
index 0000000..83d2eef
--- /dev/null
@@ -0,0 +1,505 @@
+<?xml version="1.0" encoding="iso-8859-1"?>
+<?cocoon-format type="text/xhtml"?>
+<m:math xmlns:helm="http://www.cs.unibo.it/helm" xmlns:m="http://www.w3.org/1998/Math/MathML">
+    <m:mtable helm:xref="i0" columnalign="left" equalrows="false" align="baseline 1">
+        <m:mtr>
+            <m:mtd>
+                <m:mrow>
+                    <m:mtext>DEFINITION and_ind() OF TYPE</m:mtext>
+                </m:mrow>
+            </m:mtd>
+        </m:mtr>
+        <m:mtr>
+            <m:mtd>
+                <m:mrow>
+                    <m:mphantom>
+                        <m:mtext>__</m:mtext>
+                    </m:mphantom>
+                    <m:semantics xmlns:xlink="http://www.w3.org/1999/xlink">
+                        <m:mrow helm:xref="i22">
+                            <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                <m:mtr>
+                                    <m:mtd>
+                                        <m:mrow>
+                                            <m:mo stretchy="false">(</m:mo>
+                                            <m:mrow helm:xref="i23">
+                                                <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                                    <m:mtr>
+                                                        <m:mtd>
+                                                            <m:mo color="Blue">&#928;</m:mo>
+                                                            <m:mi>A</m:mi>
+                                                            <m:mo>:</m:mo>
+                                                            <m:mrow helm:xref="i24">
+                                                                <m:mo>Prop</m:mo>
+                                                            </m:mrow>
+                                                        </m:mtd>
+                                                    </m:mtr>
+                                                    <m:mtr>
+                                                        <m:mtd>
+                                                            <m:mrow>
+                                                                <m:mo>.</m:mo>
+                                                                <m:mrow helm:xref="i25">
+                                                                    <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                                                        <m:mtr>
+                                                                            <m:mtd>
+                                                                                <m:mo color="Blue">&#928;</m:mo>
+                                                                                <m:mi>B</m:mi>
+                                                                                <m:mo>:</m:mo>
+                                                                                <m:mrow helm:xref="i26">
+                                                                                    <m:mo>Prop</m:mo>
+                                                                                </m:mrow>
+                                                                            </m:mtd>
+                                                                        </m:mtr>
+                                                                        <m:mtr>
+                                                                            <m:mtd>
+                                                                                <m:mrow>
+                                                                                    <m:mo>.</m:mo>
+                                                                                    <m:mrow helm:xref="i27">
+                                                                                        <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                                                                            <m:mtr>
+                                                                                                <m:mtd>
+                                                                                                    <m:mo color="Blue">&#928;</m:mo>
+                                                                                                    <m:mi>P</m:mi>
+                                                                                                    <m:mo>:</m:mo>
+                                                                                                    <m:mrow helm:xref="i28">
+                                                                                                        <m:mo>Prop</m:mo>
+                                                                                                    </m:mrow>
+                                                                                                </m:mtd>
+                                                                                            </m:mtr>
+                                                                                            <m:mtr>
+                                                                                                <m:mtd>
+                                                                                                    <m:mrow>
+                                                                                                        <m:mo>.</m:mo>
+                                                                                                        <m:mrow helm:xref="i29">
+                                                                                                            <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                                                                                                <m:mtr>
+                                                                                                                    <m:mtd>
+                                                                                                                        <m:mo color="Blue">&#928;</m:mo>
+                                                                                                                        <m:mi>f</m:mi>
+                                                                                                                        <m:mo>:</m:mo>
+                                                                                                                        <m:mrow helm:xref="i30">
+                                                                                                                            <m:mo stretchy="false">(</m:mo>
+                                                                                                                            <m:mi helm:xref="i31">A</m:mi>
+                                                                                                                            <m:mo color="Blue">&#8594;</m:mo>
+                                                                                                                            <m:mrow helm:xref="i32">
+                                                                                                                                <m:mo stretchy="false">(</m:mo>
+                                                                                                                                <m:mi helm:xref="i33">B</m:mi>
+                                                                                                                                <m:mo color="Blue">&#8594;</m:mo>
+                                                                                                                                <m:mi helm:xref="i34">P</m:mi>
+                                                                                                                                <m:mo stretchy="false">)</m:mo>
+                                                                                                                            </m:mrow>
+                                                                                                                            <m:mo stretchy="false">)</m:mo>
+                                                                                                                        </m:mrow>
+                                                                                                                    </m:mtd>
+                                                                                                                </m:mtr>
+                                                                                                                <m:mtr>
+                                                                                                                    <m:mtd>
+                                                                                                                        <m:mrow>
+                                                                                                                            <m:mo>.</m:mo>
+                                                                                                                            <m:mrow helm:xref="i35">
+                                                                                                                                <m:mo color="Blue">&#928;</m:mo>
+                                                                                                                                <m:mi>a</m:mi>
+                                                                                                                                <m:mo>:</m:mo>
+                                                                                                                                <m:mrow helm:xref="i36">
+                                                                                                                                    <m:mo stretchy="false">(</m:mo>
+                                                                                                                                    <m:mi xlink:href="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i37">and</m:mi>
+                                                                                                                                    <m:mphantom>
+                                                                                                                                        <m:mtext>_</m:mtext>
+                                                                                                                                    </m:mphantom>
+                                                                                                                                    <m:mi helm:xref="i38">A</m:mi>
+                                                                                                                                    <m:mphantom>
+                                                                                                                                        <m:mtext>_</m:mtext>
+                                                                                                                                    </m:mphantom>
+                                                                                                                                    <m:mi helm:xref="i39">B</m:mi>
+                                                                                                                                    <m:mo stretchy="false">)</m:mo>
+                                                                                                                                </m:mrow>
+                                                                                                                                <m:mo>.</m:mo>
+                                                                                                                                <m:mi helm:xref="i40">P</m:mi>
+                                                                                                                            </m:mrow>
+                                                                                                                        </m:mrow>
+                                                                                                                    </m:mtd>
+                                                                                                                </m:mtr>
+                                                                                                            </m:mtable>
+                                                                                                        </m:mrow>
+                                                                                                    </m:mrow>
+                                                                                                </m:mtd>
+                                                                                            </m:mtr>
+                                                                                        </m:mtable>
+                                                                                    </m:mrow>
+                                                                                </m:mrow>
+                                                                            </m:mtd>
+                                                                        </m:mtr>
+                                                                    </m:mtable>
+                                                                </m:mrow>
+                                                            </m:mrow>
+                                                        </m:mtd>
+                                                    </m:mtr>
+                                                </m:mtable>
+                                            </m:mrow>
+                                        </m:mrow>
+                                    </m:mtd>
+                                </m:mtr>
+                                <m:mtr>
+                                    <m:mtd>
+                                        <m:mrow>
+                                            <m:mo color="#b03060">:&gt;</m:mo>
+                                            <m:mrow helm:xref="i41">
+                                                <m:mo>Prop</m:mo>
+                                            </m:mrow>
+                                        </m:mrow>
+                                    </m:mtd>
+                                </m:mtr>
+                                <m:mtr>
+                                    <m:mtd>
+                                        <m:mrow>
+                                            <m:mo stretchy="false">)</m:mo>
+                                        </m:mrow>
+                                    </m:mtd>
+                                </m:mtr>
+                            </m:mtable>
+                        </m:mrow>
+                        <m:annotation-xml encoding="MathML">
+                            <m:apply helm:xref="i22">
+                                <m:csymbol>cast</m:csymbol>
+                                <m:apply helm:xref="i23">
+                                    <m:csymbol>prod</m:csymbol>
+                                    <m:bvar>
+                                        <m:ci>A</m:ci>
+                                        <m:type>
+                                            <m:apply helm:xref="i24">
+                                                <m:csymbol>Prop</m:csymbol>
+                                            </m:apply>
+                                        </m:type>
+                                    </m:bvar>
+                                    <m:apply helm:xref="i25">
+                                        <m:csymbol>prod</m:csymbol>
+                                        <m:bvar>
+                                            <m:ci>B</m:ci>
+                                            <m:type>
+                                                <m:apply helm:xref="i26">
+                                                    <m:csymbol>Prop</m:csymbol>
+                                                </m:apply>
+                                            </m:type>
+                                        </m:bvar>
+                                        <m:apply helm:xref="i27">
+                                            <m:csymbol>prod</m:csymbol>
+                                            <m:bvar>
+                                                <m:ci>P</m:ci>
+                                                <m:type>
+                                                    <m:apply helm:xref="i28">
+                                                        <m:csymbol>Prop</m:csymbol>
+                                                    </m:apply>
+                                                </m:type>
+                                            </m:bvar>
+                                            <m:apply helm:xref="i29">
+                                                <m:csymbol>prod</m:csymbol>
+                                                <m:bvar>
+                                                    <m:ci>f</m:ci>
+                                                    <m:type>
+                                                        <m:apply helm:xref="i30">
+                                                            <m:csymbol>arrow</m:csymbol>
+                                                            <m:ci helm:xref="i31">A</m:ci>
+                                                            <m:apply helm:xref="i32">
+                                                                <m:csymbol>arrow</m:csymbol>
+                                                                <m:ci helm:xref="i33">B</m:ci>
+                                                                <m:ci helm:xref="i34">P</m:ci>
+                                                            </m:apply>
+                                                        </m:apply>
+                                                    </m:type>
+                                                </m:bvar>
+                                                <m:apply helm:xref="i35">
+                                                    <m:csymbol>prod</m:csymbol>
+                                                    <m:bvar>
+                                                        <m:ci>a</m:ci>
+                                                        <m:type>
+                                                            <m:apply helm:xref="i36">
+                                                                <m:csymbol>app</m:csymbol>
+                                                                <m:ci definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i37">and</m:ci>
+                                                                <m:ci helm:xref="i38">A</m:ci>
+                                                                <m:ci helm:xref="i39">B</m:ci>
+                                                            </m:apply>
+                                                        </m:type>
+                                                    </m:bvar>
+                                                    <m:ci helm:xref="i40">P</m:ci>
+                                                </m:apply>
+                                            </m:apply>
+                                        </m:apply>
+                                    </m:apply>
+                                </m:apply>
+                                <m:apply helm:xref="i41">
+                                    <m:csymbol>Prop</m:csymbol>
+                                </m:apply>
+                            </m:apply>
+                        </m:annotation-xml>
+                    </m:semantics>
+                </m:mrow>
+            </m:mtd>
+        </m:mtr>
+        <m:mtr>
+            <m:mtd>
+                <m:mrow>
+                    <m:mtext>AS</m:mtext>
+                </m:mrow>
+            </m:mtd>
+        </m:mtr>
+        <m:mtr>
+            <m:mtd>
+                <m:mrow>
+                    <m:mphantom>
+                        <m:mtext>__</m:mtext>
+                    </m:mphantom>
+                    <m:semantics xmlns:xlink="http://www.w3.org/1999/xlink">
+                        <m:mrow helm:xref="i1">
+                            <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                <m:mtr>
+                                    <m:mtd>
+                                        <m:mo color="Red">&#955;</m:mo>
+                                        <m:mi>A</m:mi>
+                                        <m:mo>:</m:mo>
+                                        <m:mrow helm:xref="i2">
+                                            <m:mo>Prop</m:mo>
+                                        </m:mrow>
+                                    </m:mtd>
+                                </m:mtr>
+                                <m:mtr>
+                                    <m:mtd>
+                                        <m:mrow>
+                                            <m:mo>.</m:mo>
+                                            <m:mrow helm:xref="i3">
+                                                <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                                    <m:mtr>
+                                                        <m:mtd>
+                                                            <m:mo color="Red">&#955;</m:mo>
+                                                            <m:mi>B</m:mi>
+                                                            <m:mo>:</m:mo>
+                                                            <m:mrow helm:xref="i4">
+                                                                <m:mo>Prop</m:mo>
+                                                            </m:mrow>
+                                                        </m:mtd>
+                                                    </m:mtr>
+                                                    <m:mtr>
+                                                        <m:mtd>
+                                                            <m:mrow>
+                                                                <m:mo>.</m:mo>
+                                                                <m:mrow helm:xref="i5">
+                                                                    <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                                                        <m:mtr>
+                                                                            <m:mtd>
+                                                                                <m:mo color="Red">&#955;</m:mo>
+                                                                                <m:mi>P</m:mi>
+                                                                                <m:mo>:</m:mo>
+                                                                                <m:mrow helm:xref="i6">
+                                                                                    <m:mo>Prop</m:mo>
+                                                                                </m:mrow>
+                                                                            </m:mtd>
+                                                                        </m:mtr>
+                                                                        <m:mtr>
+                                                                            <m:mtd>
+                                                                                <m:mrow>
+                                                                                    <m:mo>.</m:mo>
+                                                                                    <m:mrow helm:xref="i7">
+                                                                                        <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                                                                            <m:mtr>
+                                                                                                <m:mtd>
+                                                                                                    <m:mo color="Red">&#955;</m:mo>
+                                                                                                    <m:mi>f</m:mi>
+                                                                                                    <m:mo>:</m:mo>
+                                                                                                    <m:mrow helm:xref="i8">
+                                                                                                        <m:mo stretchy="false">(</m:mo>
+                                                                                                        <m:mi helm:xref="i9">A</m:mi>
+                                                                                                        <m:mo color="Blue">&#8594;</m:mo>
+                                                                                                        <m:mrow helm:xref="i10">
+                                                                                                            <m:mo stretchy="false">(</m:mo>
+                                                                                                            <m:mi helm:xref="i11">B</m:mi>
+                                                                                                            <m:mo color="Blue">&#8594;</m:mo>
+                                                                                                            <m:mi helm:xref="i12">P</m:mi>
+                                                                                                            <m:mo stretchy="false">)</m:mo>
+                                                                                                        </m:mrow>
+                                                                                                        <m:mo stretchy="false">)</m:mo>
+                                                                                                    </m:mrow>
+                                                                                                </m:mtd>
+                                                                                            </m:mtr>
+                                                                                            <m:mtr>
+                                                                                                <m:mtd>
+                                                                                                    <m:mrow>
+                                                                                                        <m:mo>.</m:mo>
+                                                                                                        <m:mrow helm:xref="i13">
+                                                                                                            <m:mtable columnalign="left" equalrows="false" align="baseline 1">
+                                                                                                                <m:mtr>
+                                                                                                                    <m:mtd>
+                                                                                                                        <m:mo color="Red">&#955;</m:mo>
+                                                                                                                        <m:mi>a</m:mi>
+                                                                                                                        <m:mo>:</m:mo>
+                                                                                                                        <m:mrow helm:xref="i14">
+                                                                                                                            <m:mo stretchy="false">(</m:mo>
+                                                                                                                            <m:mi xlink:href="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i15">and</m:mi>
+                                                                                                                            <m:mphantom>
+                                                                                                                                <m:mtext>_</m:mtext>
+                                                                                                                            </m:mphantom>
+                                                                                                                            <m:mi helm:xref="i16">A</m:mi>
+                                                                                                                            <m:mphantom>
+                                                                                                                                <m:mtext>_</m:mtext>
+                                                                                                                            </m:mphantom>
+                                                                                                                            <m:mi helm:xref="i17">B</m:mi>
+                                                                                                                            <m:mo stretchy="false">)</m:mo>
+                                                                                                                        </m:mrow>
+                                                                                                                    </m:mtd>
+                                                                                                                </m:mtr>
+                                                                                                                <m:mtr>
+                                                                                                                    <m:mtd>
+                                                                                                                        <m:mrow>
+                                                                                                                            <m:mo>.</m:mo>
+                                                                                                                            <m:mrow helm:xref="i18">
+                                                                                                                                <m:mo>&lt;</m:mo>
+                                                                                                                                <m:mi helm:xref="i19">P</m:mi>
+                                                                                                                                <m:mo>&gt;</m:mo>
+                                                                                                                                <m:mo>CASES</m:mo>
+                                                                                                                                <m:mphantom>
+                                                                                                                                    <m:mtext>_</m:mtext>
+                                                                                                                                </m:mphantom>
+                                                                                                                                <m:mi helm:xref="i20">a</m:mi>
+                                                                                                                                <m:mphantom>
+                                                                                                                                    <m:mtext>_</m:mtext>
+                                                                                                                                </m:mphantom>
+                                                                                                                                <m:mo>OF</m:mo>
+                                                                                                                                <m:mrow>
+                                                                                                                                    <m:mo stretchy="false">(</m:mo>
+                                                                                                                                    <m:mi>conj</m:mi>
+                                                                                                                                    <m:mphantom>
+                                                                                                                                        <m:mtext>_</m:mtext>
+                                                                                                                                    </m:mphantom>
+                                                                                                                                    <m:mi>$1</m:mi>
+                                                                                                                                    <m:mphantom>
+                                                                                                                                        <m:mtext>_</m:mtext>
+                                                                                                                                    </m:mphantom>
+                                                                                                                                    <m:mi>$2</m:mi>
+                                                                                                                                    <m:mo stretchy="false">)</m:mo>
+                                                                                                                                </m:mrow>
+                                                                                                                                <m:mo color="Green">&#8658;</m:mo>
+                                                                                                                                <m:mrow>
+                                                                                                                                    <m:mo stretchy="false">(</m:mo>
+                                                                                                                                    <m:mi helm:xref="i21">f</m:mi>
+                                                                                                                                    <m:mphantom>
+                                                                                                                                        <m:mtext>_</m:mtext>
+                                                                                                                                    </m:mphantom>
+                                                                                                                                    <m:mi>$1</m:mi>
+                                                                                                                                    <m:mphantom>
+                                                                                                                                        <m:mtext>_</m:mtext>
+                                                                                                                                    </m:mphantom>
+                                                                                                                                    <m:mi>$2</m:mi>
+                                                                                                                                    <m:mo stretchy="false">)</m:mo>
+                                                                                                                                </m:mrow>
+                                                                                                                                <m:mphantom>
+                                                                                                                                    <m:mtext>_</m:mtext>
+                                                                                                                                </m:mphantom>
+                                                                                                                                <m:mo>END</m:mo>
+                                                                                                                            </m:mrow>
+                                                                                                                        </m:mrow>
+                                                                                                                    </m:mtd>
+                                                                                                                </m:mtr>
+                                                                                                            </m:mtable>
+                                                                                                        </m:mrow>
+                                                                                                    </m:mrow>
+                                                                                                </m:mtd>
+                                                                                            </m:mtr>
+                                                                                        </m:mtable>
+                                                                                    </m:mrow>
+                                                                                </m:mrow>
+                                                                            </m:mtd>
+                                                                        </m:mtr>
+                                                                    </m:mtable>
+                                                                </m:mrow>
+                                                            </m:mrow>
+                                                        </m:mtd>
+                                                    </m:mtr>
+                                                </m:mtable>
+                                            </m:mrow>
+                                        </m:mrow>
+                                    </m:mtd>
+                                </m:mtr>
+                            </m:mtable>
+                        </m:mrow>
+                        <m:annotation-xml encoding="MathML">
+                            <m:lambda helm:xref="i1">
+                                <m:bvar>
+                                    <m:ci>A</m:ci>
+                                    <m:type>
+                                        <m:apply helm:xref="i2">
+                                            <m:csymbol>Prop</m:csymbol>
+                                        </m:apply>
+                                    </m:type>
+                                </m:bvar>
+                                <m:lambda helm:xref="i3">
+                                    <m:bvar>
+                                        <m:ci>B</m:ci>
+                                        <m:type>
+                                            <m:apply helm:xref="i4">
+                                                <m:csymbol>Prop</m:csymbol>
+                                            </m:apply>
+                                        </m:type>
+                                    </m:bvar>
+                                    <m:lambda helm:xref="i5">
+                                        <m:bvar>
+                                            <m:ci>P</m:ci>
+                                            <m:type>
+                                                <m:apply helm:xref="i6">
+                                                    <m:csymbol>Prop</m:csymbol>
+                                                </m:apply>
+                                            </m:type>
+                                        </m:bvar>
+                                        <m:lambda helm:xref="i7">
+                                            <m:bvar>
+                                                <m:ci>f</m:ci>
+                                                <m:type>
+                                                    <m:apply helm:xref="i8">
+                                                        <m:csymbol>arrow</m:csymbol>
+                                                        <m:ci helm:xref="i9">A</m:ci>
+                                                        <m:apply helm:xref="i10">
+                                                            <m:csymbol>arrow</m:csymbol>
+                                                            <m:ci helm:xref="i11">B</m:ci>
+                                                            <m:ci helm:xref="i12">P</m:ci>
+                                                        </m:apply>
+                                                    </m:apply>
+                                                </m:type>
+                                            </m:bvar>
+                                            <m:lambda helm:xref="i13">
+                                                <m:bvar>
+                                                    <m:ci>a</m:ci>
+                                                    <m:type>
+                                                        <m:apply helm:xref="i14">
+                                                            <m:csymbol>app</m:csymbol>
+                                                            <m:ci definitionURL="cic:/coq/INIT/Logic/Conjunction/and.ind" helm:xref="i15">and</m:ci>
+                                                            <m:ci helm:xref="i16">A</m:ci>
+                                                            <m:ci helm:xref="i17">B</m:ci>
+                                                        </m:apply>
+                                                    </m:type>
+                                                </m:bvar>
+                                                <m:apply helm:xref="i18">
+                                                    <m:csymbol>mutcase</m:csymbol>
+                                                    <m:ci helm:xref="i19">P</m:ci>
+                                                    <m:ci helm:xref="i20">a</m:ci>
+                                                    <m:apply>
+                                                        <m:csymbol>app</m:csymbol>
+                                                        <m:ci>conj</m:ci>
+                                                        <m:ci>$1</m:ci>
+                                                        <m:ci>$2</m:ci>
+                                                    </m:apply>
+                                                    <m:apply>
+                                                        <m:csymbol>app</m:csymbol>
+                                                        <m:ci helm:xref="i21">f</m:ci>
+                                                        <m:ci>$1</m:ci>
+                                                        <m:ci>$2</m:ci>
+                                                    </m:apply>
+                                                </m:apply>
+                                            </m:lambda>
+                                        </m:lambda>
+                                    </m:lambda>
+                                </m:lambda>
+                            </m:lambda>
+                        </m:annotation-xml>
+                    </m:semantics>
+                </m:mrow>
+            </m:mtd>
+        </m:mtr>
+    </m:mtable>
+</m:math>