Correction d'un bug dans Coqdoc (indentation & mots clés)

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

1 files changed, 13 insertions, 8 deletions

diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 096e64a81..e9fd9c65e 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -325,17 +325,22 @@ rule coq_bol = parse
 	    skip_to_dot lexbuf; 
 	    coq_bol lexbuf 
 	  end else begin
-	    indentation (count_spaces s); 
-	    ident s (lexeme_start lexbuf); 
-	    let eol= body lexbuf in 
-	      if eol then coq_bol lexbuf else coq lexbuf
+	    let s = lexeme lexbuf in 
+	    let nbsp = count_spaces s in
+	      indentation nbsp; 
+	      let s = String.sub s nbsp (String.length s - nbsp) in
+		ident s (lexeme_start lexbuf + nbsp); 
+		let eol= body lexbuf in 
+		  if eol then coq_bol lexbuf else coq lexbuf
 	  end }
   | space* gallina_kw
       { let s = lexeme lexbuf in 
-	  indentation (count_spaces s);
-	  ident s (lexeme_start lexbuf); 
-	  let eol= body lexbuf in
-	    if eol then coq_bol lexbuf else coq lexbuf }
+	let nbsp = count_spaces s in
+	  indentation nbsp;
+	  let s = String.sub s nbsp (String.length s - nbsp)  in
+	    ident s (lexeme_start lexbuf + nbsp); 
+	    let eol= body lexbuf in
+	      if eol then coq_bol lexbuf else coq lexbuf }
   | space* "(**" space+ "printing" space+ (identifier | token) space+
       { let tok = lexeme lexbuf in
 	let s = printing_token lexbuf in