From 3101ff981d36359f74d5996447ba70f41398e72b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 16 May 2007 18:30:02 +0000
Subject: - MAJ entêtes des fichiers produits par coq_makefile - Correction de
 bugs dans la reconnaissance d'un "*)" potentiel dans   les lignes
 correspondant au mécanisme "section" de coqdoc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9826 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/coqdoc.tex   |  4 ++--
 tools/coq_makefile.ml4  | 20 +++++++-------------
 tools/coqdoc/pretty.mll | 29 ++++++++++++++++++-----------
 3 files changed, 27 insertions(+), 26 deletions(-)

diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
index 63594a18f9..0e3cab3e61 100644
--- a/doc/refman/coqdoc.tex
+++ b/doc/refman/coqdoc.tex
@@ -104,7 +104,7 @@ combinations, e.g.
 
 \paragraph{Sections.}
 Sections are introduced by 1 to 4 leading stars (i.e. at the beginning of the
-line). One star is a section, two stars a sub-section, etc.
+line) followed by a space. One star is a section, two stars a sub-section, etc.
 The section title is given on the remaining of the line.
 Example:
 \begin{verbatim}
@@ -152,7 +152,7 @@ escape sequences:
 
 \paragraph{Verbatim.} 
 Verbatim material is introduced by a leading \verb+<<+ and closed by
-\verb+>>+. Example:
+\verb+>>+ at the beginning of a line. Example:
 \begin{verbatim}
 Here is the corresponding caml code:
 <<
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 256515c515..cc3b60923f 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -397,24 +397,18 @@ let rec process_cmd_line = function
 
 let banner () =
   print
-"##############################################################################
-##                 The Calculus of Inductive Constructions                  ##
-##                                                                          ##
-##                                Projet Coq                                ##
-##                                                                          ##
-##                     INRIA                        ENS-CNRS                ##
-##              Rocquencourt                        Lyon                    ##
-##                                                                          ##
-##                                  Coq V7                                  ##
-##                                                                          ##
-##                                                                          ##
-##############################################################################
+"#########################################################################
+##  v      #                  The Coq Proof Assistant                   ##
+## <O___,, # CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud ##
+##   \\VV/  #                                                            ##
+##    //   #   Makefile automagically generated by coq_makefile V8.1    ##
+##########################################################################
 
 "
 
 let warning () =
   print "# WARNING\n#\n";
-  print "# This Makefile has been automagically generated by coq_makefile\n";
+  print "# This Makefile has been automagically generated\n";
   print "# Edit at your own risks !\n";
   print "#\n# END OF WARNING\n\n"
 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 57bdaf635a..a095e9d137 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -52,6 +52,11 @@
     in
     count 0 (String.index s '*')
 
+  let strip_eol s =
+    let eol = s.[String.length s - 1] = '\n' in
+    (eol, if eol then String.sub s 1 (String.length s - 1) else s)
+
+
   let formatted = ref false
   let brackets = ref 0
 
@@ -449,22 +454,24 @@ and coq = parse
 	  if eol then coq_bol lexbuf else coq lexbuf}
       
 (*s Scanning documentation, at beginning of line *)
-      
+
 and doc_bol = parse
   | space* "\n" '\n'*
       { paragraph (); doc_bol lexbuf }
-  | space* section [^')'] ([^'\n' '*'] | '*' [^'\n'')'])*
-{ let lev, s = sec_title (lexeme lexbuf) in 
-    section lev (fun () -> ignore (doc (from_string s))); 
-    doc lexbuf }
-| space* '-'+
-     { let n = count_dashes (lexeme lexbuf) in
-	 if n >= 4 then rule () else item n;
-	 doc lexbuf }
-| "<<" space*
+  | space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')?
+      { let eol, lex = strip_eol (lexeme lexbuf) in
+        let lev, s = sec_title lex in
+Printf.eprintf "%s %d" s (if eol then 1 else 2);
+        section lev (fun () -> ignore (doc (from_string s)));
+	if eol then doc_bol lexbuf else doc lexbuf }
+  | space* '-'+
+      { let n = count_dashes (lexeme lexbuf) in
+	if n >= 4 then rule () else item n;
+        doc lexbuf }
+  | "<<" space*
       { start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
   | eof 
-      { false }
+      { true }
   | _ 
       { backtrack lexbuf; doc lexbuf }
 
-- 
cgit v1.2.3