coqdoc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5379 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 83 insertions, 4 deletions

diff --git a/.depend b/.depend
index b94d84539..2895a351d 100644
--- a/.depend
+++ b/.depend
@@ -1,3 +1,4 @@
+doc/syntax.cmi: parsing/ast.cmi 
 ide/config_parser.cmi: lib/util.cmi 
 ide/coq.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \
     kernel/term.cmi lib/util.cmi toplevel/vernacexpr.cmo 
@@ -435,6 +436,8 @@ contrib/xml/doubleTypeInference.cmi: contrib/xml/acic.cmo kernel/environ.cmi \
     pretyping/evd.cmi kernel/term.cmi 
 contrib/xml/xmlcommand.cmi: library/libnames.cmi 
 ide/utils/configwin.cmi: ide/utils/uoptions.cmi 
+tools/coqdoc/output.cmi: tools/coqdoc/index.cmi 
+tools/coqdoc/pretty.cmi: tools/coqdoc/index.cmi 
 config/coq_config.cmo: config/coq_config.cmi 
 config/coq_config.cmx: config/coq_config.cmi 
 dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi 
@@ -455,6 +458,8 @@ dev/top_printers.cmx: parsing/ast.cmx toplevel/cerrors.cmx proofs/clenv.cmx \
     kernel/term.cmx pretyping/termops.cmx kernel/univ.cmx 
 doc/parse.cmo: parsing/ast.cmi 
 doc/parse.cmx: parsing/ast.cmx 
+doc/syntax.cmo: parsing/ast.cmi contrib/interface/parse.cmo doc/syntax.cmi 
+doc/syntax.cmx: parsing/ast.cmx contrib/interface/parse.cmx doc/syntax.cmi 
 ide/blaster_window.cmo: ide/coq.cmi ide/ideutils.cmi 
 ide/blaster_window.cmx: ide/coq.cmx ide/ideutils.cmx 
 ide/command_windows.cmo: ide/coq.cmi ide/coq_commands.cmo ide/ideutils.cmi \
@@ -3239,6 +3244,20 @@ ide/utils/okey.cmo: ide/utils/okey.cmi
 ide/utils/okey.cmx: ide/utils/okey.cmi 
 ide/utils/uoptions.cmo: ide/utils/uoptions.cmi 
 ide/utils/uoptions.cmx: ide/utils/uoptions.cmi 
+tools/coqdoc/alpha.cmo: tools/coqdoc/alpha.cmi 
+tools/coqdoc/alpha.cmx: tools/coqdoc/alpha.cmi 
+tools/coqdoc/index.cmo: tools/coqdoc/alpha.cmi tools/coqdoc/index.cmi 
+tools/coqdoc/index.cmx: tools/coqdoc/alpha.cmx tools/coqdoc/index.cmi 
+tools/coqdoc/main.cmo: config/coq_config.cmi tools/coqdoc/index.cmi \
+    tools/coqdoc/output.cmi tools/coqdoc/pretty.cmi 
+tools/coqdoc/main.cmx: config/coq_config.cmx tools/coqdoc/index.cmx \
+    tools/coqdoc/output.cmx tools/coqdoc/pretty.cmx 
+tools/coqdoc/output.cmo: tools/coqdoc/index.cmi tools/coqdoc/output.cmi 
+tools/coqdoc/output.cmx: tools/coqdoc/index.cmx tools/coqdoc/output.cmi 
+tools/coqdoc/pretty.cmo: tools/coqdoc/index.cmi tools/coqdoc/output.cmi \
+    tools/coqdoc/pretty.cmi 
+tools/coqdoc/pretty.cmx: tools/coqdoc/index.cmx tools/coqdoc/output.cmx \
+    tools/coqdoc/pretty.cmi 
 tactics/tauto.cmo: parsing/grammar.cma
 tactics/tauto.cmx: parsing/grammar.cma
 tactics/eqdecide.cmo: parsing/grammar.cma
diff --git a/Makefile b/Makefile
index dbb6540f9..276d779a5 100644
--- a/Makefile
+++ b/Makefile
@@ -62,7 +62,8 @@ else
  HIDE = @
 endif
 
-LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \
+LOCALINCLUDES=-I config -I tools -I tools/coqdoc \
+	      -I scripts -I lib -I kernel -I library \
               -I proofs -I tactics -I pretyping \
               -I interp -I toplevel -I parsing -I ide/utils \
 	      -I ide -I translate \
@@ -1045,10 +1046,12 @@ COQMAKEFILE=bin/coq_makefile$(EXE)
 GALLINA=bin/gallina$(EXE)
 COQTEX=bin/coq-tex$(EXE)
 COQWC=bin/coqwc$(EXE)
+COQDOC=bin/coqdoc$(EXE)
 COQVO2XML=bin/coq_vo2xml$(EXE)
 RUNCOQVO2XML=coq_vo2xml$(EXE)   # Uses the one in PATH and not the one in bin
 
-TOOLS=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQVO2XML) $(COQWC)
+TOOLS=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQVO2XML) \
+      $(COQWC) $(COQDOC)
 
 tools:: $(TOOLS) dev/top_printers.cmo
 
@@ -1082,6 +1085,16 @@ $(COQWC): tools/coqwc.cmo
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ tools/coqwc.cmo
 
+beforedepend:: tools/coqdoc/pretty.ml tools/coqdoc/index.ml
+
+COQDOCCMO=$(CONFIG) tools/coqdoc/alpha.cmo tools/coqdoc/index.cmo \
+          tools/coqdoc/output.cmo tools/coqdoc/pretty.cmo \
+	  tools/coqdoc/main.cmo
+
+$(COQDOC): $(COQDOCCMO)
+	$(SHOW)'OCAMLC -o $@'
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma unix.cma $(COQDOCCMO)
+
 COQVO2XMLCMO=$(CONFIG) toplevel/usage.cmo tools/coq_vo2xml.cmo
 
 $(COQVO2XML): $(COQVO2XMLCMO)
@@ -1091,6 +1104,7 @@ $(COQVO2XML): $(COQVO2XMLCMO)
 clean::
 	rm -f tools/coqdep_lexer.ml tools/gallina_lexer.ml
 	rm -f tools/coqwc.ml
+	rm -f tools/coqdoc/pretty.ml tools/coqdoc/index.ml
 
 archclean::
 	rm -f $(TOOLS)
@@ -1201,7 +1215,7 @@ install-allreals::
 	  cp $$f $(FULLCOQLIB)/`dirname $$f`; \
         done
 
-install-coq-info: install-coq-manpages install-emacs
+install-coq-info: install-coq-manpages install-emacs install-latex
 
 MANPAGES=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
 	man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \
@@ -1215,6 +1229,17 @@ install-emacs:
 	$(MKDIR) $(FULLEMACSLIB)
 	cp tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB)
 
+# where to put the coqdoc style file
+TEXDIR = $(BASETEXDIR)/tex/latex/misc 
+
+# command to update TeX' kpathsea database
+UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null
+
+install-latex:
+	$(MKDIR) $(TEXDIR)
+	cp tools/coqdoc/coqdoc.sty $(TEXDIR)	
+	-$(UPDATETEX)
+
 ###########################################################################
 # Documentation
 # Literate programming (with ocamlweb)
diff --git a/bin/.cvsignore b/bin/.cvsignore
index 32c168302..e5e3c2104 100644
--- a/bin/.cvsignore
+++ b/bin/.cvsignore
@@ -17,3 +17,4 @@ coqide.opt
 coqtopnew.opt
 coqtopnew.byte
 coqwc
+coqdoc
diff --git a/config/Makefile.template b/config/Makefile.template
index 0749c3540..d3f853f17 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -85,6 +85,12 @@ INSTALL=COQTOPDIRECTORY/bin/ARCHITECTURE/coqinstallEXECUTEEXTENSION
 # the command MKDIR (try to replace it with mkdirhier if you have problems)
 MKDIR=mkdir -p
 
+# where to put the coqdoc.sty style file
+BASETEXDIR=TEXDIRECTORY
+
+# command to update TeX' kpathsea database
+MKTEXLSR=MKTEXLSRCOMMAND
+
 #the command STRIP 
 # Unix systems and profiling: true
 # Unix systems and no profiling: strip
diff --git a/configure b/configure
index 162f0cb78..35d48ed7c 100755
--- a/configure
+++ b/configure
@@ -36,6 +36,7 @@ libdir_spec=no
 mandir_spec=no
 emacslib_spec=no
 emacs_spec=no
+texdir_spec=no
 reals_opt=no
 reals=all
 arch_spec=no
@@ -55,6 +56,8 @@ while : ; do
 		      libdir=$2/lib/coq
                       mandir_spec=yes
 		      mandir=$2/man
+		      texdir_spec=yes
+		      texdir=$2/share/texmf
 		      shift;;
     -local|--local) local=true
                     bindir_spec=yes
@@ -65,6 +68,8 @@ while : ; do
 		    mandir=$COQTOP/man
                     emacslib_spec=yes
 		    emacslib=$COQTOP/tools/emacs
+		    texdir_spec=yes
+		    texdir=$COQTOP/share/texmf
 		    reals_opt=yes
 		    reals=all;;
     -src|--src) COQTOP=$2
@@ -84,6 +89,9 @@ while : ; do
     -emacs |--emacs) emacs_spec=yes
 		     emacs=$2
 		     shift;;
+    -texdir|--texdir) texdir_spec=yes
+	              texdir=$2
+		      shift;;
     -arch|--arch) arch_spec=yes
                   arch=$2
 		  shift;;
@@ -151,7 +159,8 @@ case $ARCH in
 	 bindir_def=/usr/local/bin
 	 libdir_def=/usr/local/lib/coq
 	 mandir_def=/usr/local/man
-	 emacslib_def=/usr/share/emacs/site-lisp;;
+	 emacslib_def=/usr/share/emacs/site-lisp
+         texdir_def=/usr/share/texmf;;
 esac
 
 emacs_def=emacs
@@ -200,6 +209,17 @@ case $emacslib_spec in
     yes) EMACSLIB=$emacslib;;
 esac
 
+case $texdir_spec in
+    no) echo "Where should I install TeX/LaTeX files [$texdir_def] ?"
+        read TEXDIR
+	
+	case $TEXDIR in
+	    "") TEXDIR=$texdir_def;;
+	    *) true;;
+	esac;;
+    yes) TEXDIR=$texdir;;
+esac
+
 case $reals_opt in
     no) echo "Should I compile the complete theory of real analysis [Y/N, default is Y] ?"
 	read reals_ans
@@ -357,6 +377,12 @@ case $ARCH in
     fi
 esac
 
+# mktexlsr
+MKTEXLSR=`which mktexlsr`
+case $MKTEXLSR in
+    "") MKTEXLSR=true;;
+esac
+
 # Summary of the configuration
 
 echo ""
@@ -465,6 +491,8 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|MANDIRDIRECTORY|$MANDIR|" \
     -e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \
     -e "s|EMACSCOMMAND|$EMACS|" \
+    -e "s|TEXDIRECTORY|$TEXDIR|" \
+    -e "s|MKTEXLSRCOMMAND|$MKTEXLSR|" \
     -e "s|ARCHITECTURE|$ARCH|" \
     -e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \
     -e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \