Produce better html code with coqdoc and improve doc:

- correct nesting of a and div (fixes bug #2022)
- use span instead of div for inline parts
- fix standard lib template missing/new links
- use -g to produce the stdlib doc (no proofs)


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

4 files changed, 26 insertions, 23 deletions

diff --git a/Makefile.doc b/Makefile.doc
index 9f98cc2b5..e850f1c28 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -153,7 +153,7 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html
 doc/stdlib/index-body.html: | $(COQDOC) $(THEORIESVO)
 	- rm -rf doc/stdlib/html
 	$(MKDIR) doc/stdlib/html
-	$(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html \
+	$(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g \
 	  -R theories Coq $(THEORIESVO:.vo=.v)
 	mv doc/stdlib/html/index.html doc/stdlib/index-body.html
 
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 86dd5df22..84e4e4fa0 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -69,6 +69,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Logic/Description.v
     theories/Logic/Epsilon.v
     theories/Logic/IndefiniteDescription.v
+    theories/Logic/FunctionalExtensionality.v
   </dd>
     
   <dt> <b>Bool</b>:
@@ -268,8 +269,6 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
     theories/Relations/Relation_Operators.v
     theories/Relations/Relations.v
     theories/Relations/Operators_Properties.v
-    theories/Relations/Rstar.v
-    theories/Relations/Newman.v
   </dd>
     
   <dt> <b>Sets</b>:
@@ -313,7 +312,6 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
     theories/Classes/SetoidClass.v
     theories/Classes/SetoidDec.v
     theories/Classes/SetoidAxioms.v
-    theories/Classes/Functions.v
   </dd>
 
   <dt> <b>Setoids</b>:
@@ -475,7 +473,6 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
     theories/Program/Utils.v
     theories/Program/Syntax.v
     theories/Program/Program.v
-    theories/Program/FunctionalExtensionality.v
     theories/Program/Combinators.v
   </dd>
 
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index bb9d2886c..c4e0663cd 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -43,8 +43,6 @@ body { padding: 0px 0px;
 #main .section { background-color:#90bdff;
                  font-size : 175% }
 
-#main code { font-family: monospace }
-
 #main .doc { margin: 0px;
              padding: 10px;
              font-family: sans-serif;
@@ -55,7 +53,13 @@ body { padding: 0px 0px;
              background-color: #90bdff;
              border-style: plain}
 
-#main .doc code { font-family: monospace} 
+.inlinecode { 
+    display: inline;
+    font-family: monospace } 
+
+.code { 
+    display: block;
+    font-family: monospace } 
 
 /* Pied de page */
 
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 57ccce764..b38cf7b9a 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -446,38 +446,40 @@ module Html = struct
   let ident_ref m fid typ s =
     match find_module m with
     | Local ->
-	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; 
-	printf "<div class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</div></a>"
+	printf "<span class=\"id\" type=\"%s\">" typ; 
+	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid; raw_ident s;
+	printf "</a></span>"
     | Coqlib when !externals ->
 	let m = Filename.concat !coqlib m in
+	  printf "<span class=\"id\" type=\"%s\">" typ; 
 	  printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
-	  printf "<div class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</div></a>"
+	  raw_ident s; printf "</a></span>"
     | Coqlib | Unknown ->
-	printf "<div class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</div>"
+	printf "<span class=\"id\" type=\"%s\">" typ; raw_ident s; printf "</span>"
 	  
   let ident s loc = 
     if is_keyword s then begin
-      printf "<div class=\"id\" type=\"keyword\">"; 
+      printf "<span class=\"id\" type=\"keyword\">"; 
       raw_ident s; 
-      printf "</div>"
+      printf "</span>"
     end else 
       begin
 	try
 	  (match Index.find !current_module loc with
 	     | Def (fullid,ty) -> 
-		 printf "<a name=\"%s\">" fullid; 
-		 printf "<div class=\"id\" type=\"%s\">" (type_name ty); raw_ident s; printf "</div></a>"
+		 printf "<span class=\"id\" type=\"%s\">" (type_name ty); 
+		 printf "<a name=\"%s\">" fullid; raw_ident s; printf "</a></span>"
              | Mod (m,s') when s = s' ->
 		 module_ref m s
 	     | Ref (m,fullid,ty) -> 
 		 ident_ref m fullid (type_name ty) s
 	     | Mod _ ->
-		 printf "<div class=\"id\" type=\"mod\">"; raw_ident s ; printf "</div>")
+		 printf "<span class=\"id\" type=\"mod\">"; raw_ident s ; printf "</span>")
 	with Not_found ->
 	  if is_tactic s then
-	    (printf "<div class=\"id\" type=\"tactic\">"; raw_ident s; printf "</div>")
+	    (printf "<span class=\"id\" type=\"tactic\">"; raw_ident s; printf "</span>")
 	  else
-	    (printf "<div class=\"id\" type=\"var\">"; raw_ident s ; printf "</div>")
+	    (printf "<span class=\"id\" type=\"var\">"; raw_ident s ; printf "</span>")
       end
 
   let with_html_printing f tok =
@@ -508,9 +510,9 @@ module Html = struct
 
   let stop_item () = reach_item_level 0
 
-  let start_coq () = if not !raw_comments then printf "<code>\n"
+  let start_coq () = if not !raw_comments then printf "<div class=\"code\">\n"
 
-  let end_coq () = if not !raw_comments then printf "</code>\n"
+  let end_coq () = if not !raw_comments then printf "</div>\n"
 
   let start_doc () = 
     if not !raw_comments then
@@ -524,9 +526,9 @@ module Html = struct
 
   let end_code () = end_coq (); start_doc ()
 
-  let start_inline_coq () = printf "<code>"
+  let start_inline_coq () = printf "<span class=\"inlinecode\">"
 
-  let end_inline_coq () = printf "</code>"
+  let end_inline_coq () = printf "</span>"
 
   let paragraph () = stop_item (); printf "\n<br/><br/>\n"