diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-06 17:34:24 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-06 17:34:24 +0000 |
| commit | d7e8aa7b7acbc13793837aa8d582124f72afbf25 (patch) | |
| tree | c7df8bd0dc927a585803b0b2990c0b996196cdf5 /tools/coqdoc/cpretty.mll | |
| parent | 94fc8064371e5a786de28188cac0b0b2bc80ebba (diff) | |
Fix behavior on newlines with parse-comments and also do [] escaping as
usual in this mode (report and request by B. Pierce).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12054 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/cpretty.mll')
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 234df6530..cf4d89a34 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -679,12 +679,16 @@ and comment = parse if !Cdglobals.parse_comments then Output.start_comment (); comment lexbuf } | "*)" space* nl { - if !Cdglobals.parse_comments then - (Output.end_comment (); Output.line_break ()); + if !Cdglobals.parse_comments then (Output.end_comment (); Output.line_break ()); decr comment_level; if !comment_level > 0 then comment lexbuf else true } | "*)" { if !Cdglobals.parse_comments then (Output.end_comment ()); decr comment_level; if !comment_level > 0 then comment lexbuf else false } + | "[" { + if !Cdglobals.parse_comments then ( + brackets := 1; + Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ()); + comment lexbuf } | eof { false } | space+ { if !Cdglobals.parse_comments then Output.indentation (fst (count_spaces (lexeme lexbuf))); comment lexbuf } @@ -715,7 +719,7 @@ and body = parse if !Cdglobals.parse_comments then Output.start_comment (); let eol = comment lexbuf in if eol - then begin Output.line_break(); body_bol lexbuf end + then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end else body lexbuf } | identifier { let s = lexeme lexbuf in |