aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/cpretty.mll
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-03-24 20:02:25 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-03-24 20:02:25 +0000
commit3432aa39554502152abd397959f021e168720dca (patch)
treef327c76c1f0137d60d1dce51df18b77418efd9c0 /tools/coqdoc/cpretty.mll
parent6a14070e4666cc8c0457b03c81ea99a9a6c4b833 (diff)
Fix coqdoc bugs reported by Ian Lynagh.
- Add coqdoccomment LaTeX environment to sty file - Fix buggy parsing in comments git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12013 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/cpretty.mll')
-rw-r--r--tools/coqdoc/cpretty.mll9
1 files changed, 5 insertions, 4 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 1420c9a92..234df6530 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -675,8 +675,10 @@ and comments = parse
(*s Skip comments *)
and comment = parse
- | "(*" { incr comment_level; comment lexbuf }
- | "*)" space* nl {
+ | "(*" { incr comment_level;
+ if !Cdglobals.parse_comments then Output.start_comment ();
+ comment lexbuf }
+ | "*)" space* nl {
if !Cdglobals.parse_comments then
(Output.end_comment (); Output.line_break ());
decr comment_level; if !comment_level > 0 then comment lexbuf else true }
@@ -692,7 +694,7 @@ and comment = parse
and skip_to_dot = parse
| '.' space* nl { true }
- | eof | '.' space+ { false}
+ | eof | '.' space+ { false }
| "(*" { comment_level := 1; ignore (comment lexbuf); skip_to_dot lexbuf }
| _ { skip_to_dot lexbuf }
@@ -712,7 +714,6 @@ and body = parse
| "(*" { comment_level := 1;
if !Cdglobals.parse_comments then Output.start_comment ();
let eol = comment lexbuf in
- if !Cdglobals.parse_comments then Output.end_comment ();
if eol
then begin Output.line_break(); body_bol lexbuf end
else body lexbuf }