Correction du bug #1509

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

1 files changed, 10 insertions, 6 deletions

diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index c34a779e3..57bdaf635 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -478,11 +478,11 @@ and doc = parse
 	start_inline_coq (); escaped_coq lexbuf; end_inline_coq ();
 	doc lexbuf }
   | "[[" '\n' space*
-      { formatted := true; start_code ();
+      { formatted := true; line_break (); start_inline_coq ();
 	indentation (count_spaces (lexeme lexbuf)); 
-	without_gallina coq lexbuf; 
-	end_code (); formatted := false;
-	doc lexbuf }
+	let eol = body_bol lexbuf in 
+	  end_inline_coq (); formatted := false;
+	  if eol then doc_bol lexbuf else doc lexbuf}
   | '*'* "*)" space* '\n'
       { true }
   | '*'* "*)"
@@ -593,6 +593,8 @@ and body_bol = parse
 
 and body = parse
   | '\n' {line_break(); body_bol lexbuf}
+  | '\n'+ space* "]]"
+      { if not !formatted then begin symbol (lexeme lexbuf); body lexbuf end else true }
   | eof { false }
   | '.' space* '\n' | '.' space* eof { char '.'; line_break(); true }      
   | '.' space+ { char '.'; char ' '; false }
@@ -600,12 +602,14 @@ and body = parse
 	     if eol then body_bol lexbuf else body lexbuf }
   | identifier 
       { let s = lexeme lexbuf in 
-	  ident s (lexeme_start lexbuf); body lexbuf }
+	  ident s (lexeme_start lexbuf); 
+	  body lexbuf }
   | token
       { let s = lexeme lexbuf in
 	  symbol s; body lexbuf }
   | _ { let c = lexeme_char lexbuf 0 in 
-	  char c; body lexbuf }
+	  char c; 
+          body lexbuf }
 
 and skip_hide = parse
   | eof | end_hide { () }