- coqdoc: correction d'un bug sur les commentaires imbriqués

- coq_makefile: amélioration des chemins de camlp4/5



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

2 files changed, 21 insertions, 14 deletions

diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 2dfac4e18..7b4b7c6e4 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -156,7 +156,6 @@ let variables l =
     | _ :: r -> var_aux r
   in
     section "Variables definitions.";
-    print "CAMLP4LIB:=$(shell $(CAMLBIN)camlp5 -where 2> /dev/null || $(CAMLBIN)camlp4 -where)\n";
     print "CAMLP4:=$(notdir $(CAMLP4LIB))\n"; 
     if Coq_config.local then
       (print "COQSRC:=$(COQTOP)\n";
@@ -175,7 +174,7 @@ let variables l =
   -I $(COQTOP)/contrib/subtac -I $(COQTOP)/contrib/xml \\
   -I $(CAMLP4LIB)\n")
     else
-      (print "COQSRC:=$(shell $(COQTOP)coqc -where)\n"; 
+      (print "COQSRC:=$(shell $(COQBIN)coqc -where)\n"; 
        print "COQSRCLIBS:=-I $(COQSRC)\n");
     print "ZFLAGS:=$(OCAMLLIBS) $(COQSRCLIBS)\n";
     if !opt = "-byte" then 
@@ -255,7 +254,8 @@ let include_dirs l =
   let str_i' = parse_includes inc_i' in
   let str_r = parse_includes inc_r in
     section "Libraries definition.";
-    print "OCAMLLIBS:="; print_list "\\\n  " str_i; print "\n";
+    print "CAMLP4LIB:=$(shell $(CAMLBIN)camlp5 -where 2> /dev/null || $(CAMLBIN)camlp4 -where)\n";
+    print "OCAMLLIBS:=-I $(CAMLP4LIB) "; print_list "\\\n  " str_i; print "\n";
     print "COQLIBS:="; print_list "\\\n  " str_i'; print " "; print_list "\\\n  " str_r; print "\n";
     print "COQDOCLIBS:=";   print_list "\\\n  " str_r; print "\n\n"
 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index b2fa915b6..b02133285 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -56,6 +56,7 @@
 
   let formatted = ref false
   let brackets = ref 0
+  let comment_level = ref 0
 
   let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
 
@@ -93,7 +94,8 @@
 
   let reset () =
     formatted := false;
-    brackets := 0
+    brackets := 0;
+    comment_level := 0
 
   (* erasing of Section/End *)
 
@@ -386,6 +388,7 @@ rule coq_bol = parse
   | space* "(**" space+ "printing" space+
       { eprintf "warning: bad 'printing' command at character %d\n" 
 	  (lexeme_start lexbuf); flush stderr;
+	comment_level := 1;
 	ignore (comment lexbuf);
 	coq_bol lexbuf }
   | space* "(**" space+ "remove" space+ "printing" space+ 
@@ -395,10 +398,12 @@ rule coq_bol = parse
   | space* "(**" space+ "remove" space+ "printing" space+
       { eprintf "warning: bad 'remove printing' command at character %d\n" 
 	  (lexeme_start lexbuf); flush stderr;
+	comment_level := 1;
 	ignore (comment lexbuf);
 	coq_bol lexbuf }
   | space* "(*"
-      { let eol = comment lexbuf in
+      { comment_level := 1; 
+	let eol = comment lexbuf in
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | eof 
       { () }
@@ -422,7 +427,8 @@ and coq = parse
 	  Output.end_doc (); Output.start_coq (); 
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | "(*"
-      { let eol = comment lexbuf in
+      { comment_level := 1;
+	let eol = comment lexbuf in
 	  if eol then begin Output.line_break(); coq_bol lexbuf end 
           else coq lexbuf
       }
@@ -557,7 +563,7 @@ and escaped_coq = parse
   | "["
       { incr brackets; Output.char '['; escaped_coq lexbuf }
   | "(*"
-      { ignore (comment lexbuf); escaped_coq lexbuf }
+      { comment_level := 1; ignore (comment lexbuf); escaped_coq lexbuf }
   | "*)"
       { (* likely to be a syntax error: we escape *) backtrack lexbuf }
   | eof
@@ -592,16 +598,16 @@ and comments = parse
 (*s Skip comments *)
 
 and comment = parse
-  | "(*" { comment lexbuf }
-  | "*)" space* nl { true }
-  | "*)" { false }
-  | eof  { false }
-  | _    { comment lexbuf }
+  | "(*" { incr comment_level; comment lexbuf }
+  | "*)" space* nl { decr comment_level; if !comment_level > 0 then comment lexbuf else true }
+  | "*)" { decr comment_level; if !comment_level > 0 then comment lexbuf else false }
+  | eof  {  false }
+  | _    {  comment lexbuf }
 
 and skip_to_dot = parse
   | '.' space* nl { true }
   | eof | '.' space+ { false}
-  | "(*" { ignore (comment lexbuf); skip_to_dot lexbuf }
+  | "(*" { comment_level := 1; ignore (comment lexbuf); skip_to_dot lexbuf }
   | _ { skip_to_dot lexbuf }
 
 and body_bol = parse
@@ -617,7 +623,8 @@ and body = parse
   | '.' space* nl | '.' space* eof { Output.char '.'; Output.line_break(); true }      
   | '.' space+ { Output.char '.'; Output.char ' '; false }
   | '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
-  | "(*" { let eol = comment lexbuf in 
+  | "(*" { comment_level := 1; 
+	   let eol = comment lexbuf in 
 	     if eol 
 	     then begin Output.line_break(); body_bol lexbuf end
 	     else body lexbuf }