Génération d'une toc en html et avec l'option -ps

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

4 files changed, 66 insertions, 71 deletions

diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index a9968b03eb..b66d34e9dd 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -317,14 +317,15 @@ let all_target l =
 	print "spec: $(VIFILES)\n\n";
 	print "gallina: $(GFILES)\n\n";
 	print "html: $(GLOBFILES) $(VFILES)\n";
-	print "\t-mkdir html\n"; 
-	print "\t$(COQDOC) -html $(COQLIBS) -d html $(VFILES)\n\n";
+	print "\t- mkdir html\n"; 
+	print "\t$(COQDOC) -toc -html $(COQLIBS) -d html $(VFILES)\n\n";
 	print "gallinahtml: $(GLOBFILES) $(VFILES)\n";
-	print "\t$(COQDOC) -html -g $(COQLIBS) -d html $(VFILES)\n\n";
+	print "\t- mkdir html\n"; 
+	print "\t$(COQDOC) -toc -html -g $(COQLIBS) -d html $(VFILES)\n\n";
 	print "all.ps: $(VFILES)\n";
-	print "\t$(COQDOC) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
+	print "\t$(COQDOC) -toc -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
 	print "all-gal.ps: $(VFILES)\n";
-	print "\t$(COQDOC) -ps -g -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
+	print "\t$(COQDOC) -toc -ps -g -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
 	print "\n\n"
       end
       
@@ -395,12 +396,12 @@ let rec process_cmd_line = function
 	      
 let banner () =
   print
-"#########################################################################
- ##  v      #                  The Coq Proof Assistant                   ##
- ## <O___,, # CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud ##
- ##   \\VV/  #                                                            ##
- ##    //   #   Makefile automagically generated by coq_makefile V8.1    ##
- ##########################################################################
+"##########################################################################
+##  v      #                  The Coq Proof Assistant                   ##
+## <O___,, # CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud ##
+##   \\VV/  #                                                            ##
+##    //   #   Makefile automagically generated by coq_makefile V8.2    ##
+##########################################################################
 
 "
 
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index f87b86389f..9bb7bd4002 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -34,12 +34,6 @@ type index_entry =
   | Ref of coq_module * string
   | Mod of coq_module * string
 
-let string_of_index_entry ie = 
-  match ie with
-    | Def (s, t) -> "Def ("^s^", _)"
-    | Ref (m, s) -> "Ref (_, "^s^")"
-    | Mod (m, s) -> "Mod (_, "^s^")"
-
 let current_type = ref Library
 let current_library = ref ""
   (** referes to the file being parsed *)
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index f0f39edfdd..b00bcfcf96 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -19,9 +19,7 @@
  *)
 
 open Cdglobals
-open Filename
 open Printf
-open Pretty
 
 (*s \textbf{Usage.} Printed on error output. *)
 
@@ -76,7 +74,7 @@ let banner () =
   flush stderr
     
 let target_full_name f = 
-  match !target_language with
+  match !Cdglobals.target_language with
     | HTML -> f ^ ".html"
     | _ -> f ^ ".tex"
 	
@@ -123,7 +121,7 @@ let add_path dir name =
 let name_of_path = Str.global_replace (Str.regexp "/") ".";;
 
 let coq_module filename = 
-  let bfname = chop_extension filename in
+  let bfname = Filename.chop_extension filename in
   let nfname = normalize_filename bfname in
   let rec change_prefix map f = 
     match map with
@@ -148,9 +146,9 @@ let coq_module filename =
 
 let what_file f =
   check_if_file_exists f;
-  if check_suffix f ".v" || check_suffix f ".g" then
+  if Filename.check_suffix f ".v" || Filename.check_suffix f ".g" then
     Vernac_file (f, coq_module f)
-  else if check_suffix f ".tex" then
+  else if Filename.check_suffix f ".tex" then
     Latex_file f
   else 
      (eprintf "\ncoqdoc: don't know what to do with %s\n" f; exit 1)
@@ -324,6 +322,7 @@ let clean_temp_files basefile =
     remove (basefile ^ ".tex");
     remove (basefile ^ ".log");
     remove (basefile ^ ".aux");
+    remove (basefile ^ ".toc");
     remove (basefile ^ ".dvi");
     remove (basefile ^ ".ps");
     remove (basefile ^ ".haux");
@@ -352,7 +351,7 @@ let copy src dst =
 let gen_one_file l =
   let file = function
     | Vernac_file (f,m) -> 
-	Output.set_module m; coq_file f m
+	Output.set_module m; Pretty.coq_file f m
     | Latex_file _ -> ()
   in
     if (!header_trailer) then Output.header ();
@@ -368,8 +367,7 @@ let gen_mult_files l =
 	let hf = target_full_name m in
 	  open_out_file hf;
 	  if (!header_trailer) then Output.header (); 
-	  if !toc then Output.make_toc ();
-	  coq_file f m; 
+	  Pretty.coq_file f m; 
 	  if (!header_trailer) then Output.trailer ();
 	  close_out_file()
     | Latex_file _ -> ()
@@ -434,52 +432,54 @@ let produce_document l =
 	gen_mult_files l
 	  
 let produce_output fl =
-  if not (!dvi || !ps) then begin
+  if not (!dvi || !ps) then 
     produce_document fl
-  end else begin
-    let texfile = Filename.temp_file "coqdoc" ".tex" in
-    let basefile = chop_suffix texfile ".tex" in
-    let final_out_to = !out_to in
-      out_to := File texfile;
-      produce_document fl;
-      let command = 
-	let file = basename texfile in
-	let file = 
-	  if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file 
+  else 
+    begin
+      let texfile = Filename.temp_file "coqdoc" ".tex" in
+      let basefile = Filename.chop_suffix texfile ".tex" in
+      let final_out_to = !out_to in
+	out_to := File texfile;
+	output_dir := (Filename.dirname texfile);
+	produce_document fl;
+	let latexcmd = 
+	  let file = Filename.basename texfile in
+	  let file = 
+	    if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file 
+	  in
+	    sprintf "latex %s && latex %s 1>&2 %s" file file (if !quiet then "> /dev/null" else "")
 	in
-	  sprintf "(latex %s && latex %s) 1>&2 %s" file file
-	    (if !quiet then "> /dev/null" else "")
-      in
-      let res = locally (dirname texfile) Sys.command command in
-	if res <> 0 then begin
-	  eprintf "Couldn't run LaTeX successfully\n"; 
-	  clean_and_exit basefile res
-	end;
-	let dvifile = basefile ^ ".dvi" in
-	  if !dvi then 
-	    begin
-	      match final_out_to with
-		| MultFiles | StdOut -> cat dvifile
-		| File f -> copy dvifile f
+	let res = locally (Filename.dirname texfile) Sys.command latexcmd in
+	  if res <> 0 then begin
+	      eprintf "Couldn't run LaTeX successfully\n"; 
+	      clean_and_exit basefile res
 	    end;
-	  if !ps then begin
-	    let psfile = basefile ^ ".ps" 
-	    in
-	    let command = 
-	      sprintf "dvips %s -o %s %s" dvifile psfile 
-		(if !quiet then "> /dev/null 2>&1" else "")
-	    in
-	    let res = Sys.command command in
-	      if res <> 0 then begin
-		eprintf "Couldn't run dvips successfully\n"; 
-		clean_and_exit basefile res
+	  
+	  let dvifile = basefile ^ ".dvi" in
+	    if !dvi then 
+	      begin
+		match final_out_to with
+		  | MultFiles | StdOut -> cat dvifile
+		  | File f -> copy dvifile f
 	      end;
-	      match final_out_to with
-		| MultFiles | StdOut -> cat psfile
-		| File f -> copy psfile f
-	  end;
-	  clean_temp_files basefile
-  end
+	    if !ps then begin
+		let psfile = basefile ^ ".ps" 
+		in
+		let command = 
+		  sprintf "dvips %s -o %s %s" dvifile psfile 
+		    (if !quiet then "> /dev/null 2>&1" else "")
+		in
+		let res = Sys.command command in
+		  if res <> 0 then begin
+		      eprintf "Couldn't run dvips successfully\n"; 
+		      clean_and_exit basefile res
+		    end;
+		  match final_out_to with
+		    | MultFiles | StdOut -> cat psfile
+		    | File f -> copy psfile f
+	      end;
+	    clean_temp_files basefile
+    end
 
 
 (*s \textbf{Main program.} Print the banner, parse the command line,
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 77b4eda8d3..5e37213867 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -301,7 +301,7 @@ module Html = struct
 
   let start_module () = 
     if not !short then begin
-      (* add_toc_entry (Toc_library !current_module); *)
+      add_toc_entry (Toc_library !current_module);
       printf "<h1 class=\"libtitle\">Library %s</h1>\n\n" !current_module
     end
 
@@ -555,8 +555,8 @@ module Html = struct
 	  item n; 
 	  printf "<a href=\"%s\">" r; f (); printf "</a>\n"
     in
-    Queue.iter make_toc_entry toc_q;
-    stop_item ();
+      Queue.iter make_toc_entry toc_q;
+      stop_item ();
 
 end