From 8e66761c81648add03ed21b157a3bace716b8e08 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Thu, 29 Apr 2010 16:33:36 +0000
Subject: "make source-doc" builds documentation of mli in html and pdf at
 dev/ocamldoc/

old "make source-doc" that documents ml files and didn't work is now
"make ml-doc" but still don't work :-)

"make clean" cleans dev/ocamldoc/ properly

wierd? calls of dependency graph generation leave unchanged

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12978 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/Makefile                |  53 -----------
 dev/docintro                |  50 ----------
 dev/html/style.css          | 220 --------------------------------------------
 dev/ocamldoc/docintro       |  49 ++++++++++
 dev/ocamldoc/html/style.css | 220 ++++++++++++++++++++++++++++++++++++++++++++
 5 files changed, 269 insertions(+), 323 deletions(-)
 delete mode 100644 dev/Makefile
 delete mode 100644 dev/docintro
 delete mode 100644 dev/html/style.css
 create mode 100644 dev/ocamldoc/docintro
 create mode 100644 dev/ocamldoc/html/style.css

(limited to 'dev')

diff --git a/dev/Makefile b/dev/Makefile
deleted file mode 100644
index 4693bd136c..0000000000
--- a/dev/Makefile
+++ /dev/null
@@ -1,53 +0,0 @@
-include ../config/Makefile
-
-LOCALINCLUDES=-I ../config -I ../tools -I ../tools/coqdoc \
-	      -I ../scripts -I ../lib -I ../kernel -I ../kernel/byterun -I ../library \
-              -I ../proofs -I ../tactics -I ../pretyping \
-              -I ../interp -I ../toplevel -I ../parsing -I ../ide/utils -I ../ide \
-              -I ../plugins/omega -I ../plugins/romega \
-	      -I ../plugins/ring -I ../plugins/dp -I ../plugins/setoid_ring \
-              -I ../plugins/xml -I ../plugins/extraction \
-              -I ../plugins/fourier -I ../plugins/cc \
-	      -I ../plugins/funind -I ../plugins/firstorder \
-              -I ../plugins/field -I ../plugins/subtac -I ../plugins/rtauto \
-              -I ../plugins/recdef
-
-MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
-
-MLIS=$(wildcard ../lib/*.mli ../kernel/*.mli ../library/*.mli \
-	../pretyping/*.mli ../interp/*.mli \
-	../parsing/*.mli ../proofs/*.mli \
-	../tactics/*.mli ../toplevel/*.mli)
-
-all:: html coq.pdf
-
-newsyntax.dvi: newsyntax.tex
-	latex $<
-	latex $<
-
-coq.dvi: coq.tex
-	latex coq
-	latex coq
-
-coq.tex::
-	ocamldoc -latex -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\
-	$(MLIS) -t "Coq mlis documentation" -intro docintro -o coq.tex
-
-html::
-	ocamldoc -html -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\
-	$(MLIS) -d html -colorize-code \
-	-t "Coq mlis documentation" -intro docintro -css-style style.css
-
-%.dot: ../%
-	ocamldoc -rectypes $(MLINCLUDES) -t $* -dot -dot-reduce ../$*/*.ml ../$*/*.mli -o $@
-
-%.png: %.dot
-	dot -Tpng $< -o $@
-
-clean::
-	rm -f *~ *.log *.aux
-
-.SUFFIXES: .tex .png
-
-%.pdf: %.tex
-	pdflatex $< && pdflatex $<
\ No newline at end of file
diff --git a/dev/docintro b/dev/docintro
deleted file mode 100644
index 3d37d5374d..0000000000
--- a/dev/docintro
+++ /dev/null
@@ -1,50 +0,0 @@
-{!indexlist}
-
-This is Coq, a proof assistant for the Calculus of Inductive Construction.
-This document describes the implementation of Coq.
-It has been automatically generated from the source of
-Coq using ocamldoc, a literate programming tool for
-Objective Caml  freely available at http://caml.inria.fr/.
-The source files are organized in several directories ordered like that:
-
-{ol {- Utility libraries : lib
-
-describes the various utility libraries used in the code
-of Coq.}
-{- Kernel : kernel
-
-describes the \Coq\ kernel, which is a type checker for the Calculus
-of Inductive Construction.}
-{- Library : library
-
-describes the Coq library, which is made of two parts:
-- a general mechanism to keep a trace of all operations and of
-    the state of the system, with backtrack capabilities;
-- a global environment for the CCI, with functions to export and 
-    import compiled modules.
-
-}
-{- Pretyping : pretyping
-
-}
-{- Front abstract syntax of terms : interp
-
-describes the translation from Coq context-dependent
-front abstract syntax of terms {v front v} to and from the
-context-free, untyped, raw form of constructions {v rawconstr v}.}
-{- Parsers and printers : parsing
-
-describes the implementation of the \Coq\ parsers and printers.}
-{- Proof engine : proofs
-
-describes the Coq proof engine, which is also called
-the ``refiner'', since it provides a way to build terms by successive
-refining steps. Those steps are either primitive rules or higher-level
-tactics.}
-{- Tacticts : tactics
-
-describes the Coq main tactics.}
-{- Toplevel : toplevel
-
-describes the highest modules of the Coq system.}
-}
diff --git a/dev/html/style.css b/dev/html/style.css
deleted file mode 100644
index b8f02a15fb..0000000000
--- a/dev/html/style.css
+++ /dev/null
@@ -1,220 +0,0 @@
-a:visited {
-  color: #416DFF; text-decoration: none; 
-}
-
-a:link {
-  color: #416DFF; text-decoration: none;
-}
-
-a:hover {
-  color: Red; text-decoration: none; background-color: #5FFF88
-}
-
-a:active {
-  color: Red; text-decoration: underline; 
-}
-
-.keyword {
-  font-weight: bold; color: Red 
-}
-
-.keywordsign {
-  color: #C04600 
-}
-
-.superscript {
-  font-size: 4 
-}
-
-.subscript {
-  font-size: 4 
-}
-
-.comment {
-  color: Green 
-}
-
-.constructor {
-  color: Blue 
-}
-
-.type {
-  color: #5C6585 
-}
-
-.string {
-  color: Maroon 
-}
-
-.warning {
-  color: Red; font-weight: bold 
-}
-
-.info {
-  margin-left: 3em; margin-right: 3em 
-}
-
-.param_info {
-  margin-top: 4px; margin-left: 3em; margin-right: 3em 
-}
-
-.code {
-  color: #465F91; 
-}
-
-h1 {
-  font-size: 20pt; text-align: center; 
-}
-
-h5, h6, div.h7, div.h8, div.h9 {
-  font-size: 20pt;
-  border: 1px solid #000000;
-  margin-top: 5px;
-  margin-bottom: 2px;
-  text-align: center;
-  padding: 2px;
-}
-
-h5 {
-  background-color: #90FDFF;
-}
-
-h6 {
-  background-color: #016699;
-  color: white;
-}
-
-div.h7 {
-  background-color: #E0FFFF;
-}
-
-div.h8 {
-  background-color: #F0FFFF;
-}
-
-div.h9 {
-  background-color: #FFFFFF;
-}
-
-.typetable, .indextable, .paramstable {
-  border-style: hidden;
-}
-
-.paramstable {
-  padding: 5pt 5pt;
-}
-
-body {
-  background-color: white;
-}
-
-tr {
-  background-color: white;
-}
-
-td.typefieldcomment {
-  background-color: #FFFFFF;
-  font-size: smaller;
-}
-
-pre {
-  margin-bottom: 4px;
-}
-
-div.sig_block {
-  margin-left: 2em;
-}
-
-
-h2 {
-  font-family: Arial, Helvetica, sans-serif;
-  font-size: 16pt;
-  font-weight: normal;
-  border-bottom: 1px solid #dadada;
-  border-top: 1px solid #dadada;
-  color: #101010;
-  background: #eeeeff;
-  margin: 25px 0px 10px 0px;
-  padding: 1px 1px 1px 1px;
-}
-
-h3 {
-  font-family: Arial, Helvetica, sans-serif;
-  font-size: 12pt;
-  color: #016699;
-  font-weight: bold;
-  padding: 15px 0 0 0ex;
-  margin: 5px 0 0 0;
-}
-
-h4 {
-  font-family: Arial, Helvetica, sans-serif;
-  font-size: 10pt;
-  color: #016699;
-  padding: 15px 0 0 0ex;
-  margin: 5px 0 0 0;
-}
-
-/* Here starts the overwrite of default rules to give a better look */
-
-body {
-  font-family: Calibri, Georgia, Garamond, Baskerville, serif;
-  font-size: 12pt;
-  background-color: white;
-}
-
-a:link, a {
-  color: #6895c3 !important;
-}
-
-a:hover {
-  color: #2F4459 !important;
-  background-color: white;
-}
-
-hr {
-  height: 1px;
-  color: #016699;
-  background-color: #016699;
-  border-width: 0;
-}
-
-h1, h1 a:link, h1 a:visited, h1 a {
-  font-family: Cambria, Georgia, Garamond, Baskerville, serif;
-  color: #016699;
-}
-
-.navbar {
-  float: left;
-}
-
-.navbar a, .navbar a:link, .navbar a:visited {
-  color: #016699;
-  font-family: Arial, Helvetica, sans-serif;
-  font-weight: bold;
-  font-size: 80%;
-}
-
-.keyword {
-  color: #c13939;
-}
-
-.constructor {
-  color: #3c8f7e;
-}
-
-pre, code {
-  font-family: "DejaVu Sans Mono", "Bitstream Vera Mono", "Courrier New", monospace;
-  white-space: normal;
-  font-size: 9pt;
-  font-weight: bold;
-}
-
-.type br {
-  display: none;
-}
-
-.info {
-  margin-left: 1em;
-  font-size: 12pt;
-}
diff --git a/dev/ocamldoc/docintro b/dev/ocamldoc/docintro
new file mode 100644
index 0000000000..3c0e262d47
--- /dev/null
+++ b/dev/ocamldoc/docintro
@@ -0,0 +1,49 @@
+{!indexlist}
+
+This is Coq, a proof assistant for the Calculus of Inductive Constructions.
+This document describes the implementation of Coq.
+It has been automatically generated from the source of
+Coq using {{:http://caml.inria.fr/}ocamldoc}.
+The source files are organized in several directories ordered like that:
+
+{ol {- Utility libraries : lib
+
+describes the various utility libraries used in the code
+of Coq.}
+{- Kernel : kernel
+
+describes the Coq kernel, which is a type checker for the Calculus
+of Inductive Constructions.}
+{- Library : library
+
+describes the Coq library, which is made of two parts:
+- a general mechanism to keep a trace of all operations and of
+    the state of the system, with backtrack capabilities;
+- a global environment for the CCI, with functions to export and 
+    import compiled modules.
+
+}
+{- Pretyping : pretyping
+
+}
+{- Front abstract syntax of terms : interp
+
+describes the translation from Coq context-dependent
+front abstract syntax of terms {v constr_expr v} to and from the
+context-free, untyped, raw form of constructions {v rawconstr v}.}
+{- Parsers and printers : parsing
+
+describes the implementation of the Coq parsers and printers.}
+{- Proof engine : proofs
+
+describes the Coq proof engine, which is also called
+the ``refiner'', since it provides a way to build terms by successive
+refining steps. Those steps are either primitive rules or higher-level
+tactics.}
+{- Tacticts : tactics
+
+describes the Coq main tactics.}
+{- Toplevel : toplevel
+
+describes the highest modules of the Coq system.}
+}
diff --git a/dev/ocamldoc/html/style.css b/dev/ocamldoc/html/style.css
new file mode 100644
index 0000000000..c2c45b6297
--- /dev/null
+++ b/dev/ocamldoc/html/style.css
@@ -0,0 +1,220 @@
+a:visited {
+  color: #416DFF; text-decoration: none; 
+}
+
+a:link {
+  color: #416DFF; text-decoration: none;
+}
+
+a:hover {
+  color: Red; text-decoration: none; background-color: #5FFF88
+}
+
+a:active {
+  color: Red; text-decoration: underline; 
+}
+
+.keyword {
+  font-weight: bold; color: Red 
+}
+
+.keywordsign {
+  color: #C04600 
+}
+
+.superscript {
+  font-size: 8 
+}
+
+.subscript {
+  font-size: 8 
+}
+
+.comment {
+  color: Green 
+}
+
+.constructor {
+  color: Blue 
+}
+
+.type {
+  color: #5C6585 
+}
+
+.string {
+  color: Maroon 
+}
+
+.warning {
+  color: Red; font-weight: bold 
+}
+
+.info {
+  margin-left: 3em; margin-right: 3em 
+}
+
+.param_info {
+  margin-top: 4px; margin-left: 3em; margin-right: 3em 
+}
+
+.code {
+  color: #465F91; 
+}
+
+h1 {
+  font-size: 20pt; text-align: center; 
+}
+
+h5, h6, div.h7, div.h8, div.h9 {
+  font-size: 20pt;
+  border: 1px solid #000000;
+  margin-top: 5px;
+  margin-bottom: 2px;
+  text-align: center;
+  padding: 2px;
+}
+
+h5 {
+  background-color: #90FDFF;
+}
+
+h6 {
+  background-color: #016699;
+  color: white;
+}
+
+div.h7 {
+  background-color: #E0FFFF;
+}
+
+div.h8 {
+  background-color: #F0FFFF;
+}
+
+div.h9 {
+  background-color: #FFFFFF;
+}
+
+.typetable, .indextable, .paramstable {
+  border-style: hidden;
+}
+
+.paramstable {
+  padding: 5pt 5pt;
+}
+
+body {
+  background-color: white;
+}
+
+tr {
+  background-color: white;
+}
+
+td.typefieldcomment {
+  background-color: #FFFFFF;
+  font-size: smaller;
+}
+
+pre {
+  margin-bottom: 4px;
+}
+
+div.sig_block {
+  margin-left: 2em;
+}
+
+
+h2 {
+  font-family: Arial, Helvetica, sans-serif;
+  font-size: 16pt;
+  font-weight: normal;
+  border-bottom: 1px solid #dadada;
+  border-top: 1px solid #dadada;
+  color: #101010;
+  background: #eeeeff;
+  margin: 25px 0px 10px 0px;
+  padding: 1px 1px 1px 1px;
+}
+
+h3 {
+  font-family: Arial, Helvetica, sans-serif;
+  font-size: 12pt;
+  color: #016699;
+  font-weight: bold;
+  padding: 15px 0 0 0ex;
+  margin: 5px 0 0 0;
+}
+
+h4 {
+  font-family: Arial, Helvetica, sans-serif;
+  font-size: 10pt;
+  color: #016699;
+  padding: 15px 0 0 0ex;
+  margin: 5px 0 0 0;
+}
+
+/* Here starts the overwrite of default rules to give a better look */
+
+body {
+  font-family: Calibri, Georgia, Garamond, Baskerville, serif;
+  font-size: 12pt;
+  background-color: white;
+}
+
+a:link, a {
+  color: #6895c3 !important;
+}
+
+a:hover {
+  color: #2F4459 !important;
+  background-color: white;
+}
+
+hr {
+  height: 1px;
+  color: #016699;
+  background-color: #016699;
+  border-width: 0;
+}
+
+h1, h1 a:link, h1 a:visited, h1 a {
+  font-family: Cambria, Georgia, Garamond, Baskerville, serif;
+  color: #016699;
+}
+
+.navbar {
+  float: left;
+}
+
+.navbar a, .navbar a:link, .navbar a:visited {
+  color: #016699;
+  font-family: Arial, Helvetica, sans-serif;
+  font-weight: bold;
+  font-size: 80%;
+}
+
+.keyword {
+  color: #c13939;
+}
+
+.constructor {
+  color: #3c8f7e;
+}
+
+pre, code {
+  font-family: "DejaVu Sans Mono", "Bitstream Vera Mono", "Courrier New", monospace;
+  white-space: normal;
+  font-size: 9pt;
+  font-weight: bold;
+}
+
+.type br {
+  display: none;
+}
+
+.info {
+  margin-left: 1em;
+  font-size: 12pt;
+}
-- 
cgit v1.2.3