diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-06-03 08:28:57 +0200 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-06-03 08:28:57 +0200 |
commit | c75805f735d6a7f9972fe9ae8214eebc97c20852 (patch) | |
tree | 43b790f539cfd275502823709aa0de0f7b49e061 /tools/coqdoc | |
parent | 99881431d7f3050b5062300c28a514ccd04f878b (diff) |
Make "coqdoc -g --parse-comments" behave properly (bug #4773).
As a side effect, there should be a small speedup when ignoring comments.
This commit also fixes two bugs related to handling "$$" and "#" in
comments.
Diffstat (limited to 'tools/coqdoc')
-rw-r--r-- | tools/coqdoc/cpretty.mll | 173 |
1 files changed, 96 insertions, 77 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 431080c6b..7bc342555 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -245,6 +245,12 @@ let s = String.sub s isp (String.length s - isp) in Output.keyword s (lexeme_start lexbuf + isp) + let only_gallina () = + !Cdglobals.gallina && !in_proof <> None + + let parse_comments () = + !Cdglobals.parse_comments && not (only_gallina ()) + } (*s Regular expressions *) @@ -486,7 +492,7 @@ rule coq_bol = parse in if eol then coq_bol lexbuf else coq lexbuf } | space* end_kw { let eol = - if not (!in_proof <> None && !Cdglobals.gallina) then + if not (only_gallina ()) then begin backtrack lexbuf; body_bol lexbuf end else skip_to_dot lexbuf in @@ -535,14 +541,15 @@ rule coq_bol = parse coq_bol lexbuf } | space* "(*" { comment_level := 1; - if !Cdglobals.parse_comments then begin - let s = lexeme lexbuf in - let nbsp,isp = count_spaces s in - Output.indentation nbsp; - Output.start_comment (); - end; - let eol = comment lexbuf in - if eol then coq_bol lexbuf else coq lexbuf } + let eol = + if parse_comments () then begin + let s = lexeme lexbuf in + let nbsp, isp = count_spaces s in + Output.indentation nbsp; + Output.start_comment (); + comment lexbuf + end else skipped_comment lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } | eof { () } | _ @@ -558,7 +565,7 @@ rule coq_bol = parse and coq = parse | nl - { if not (!in_proof <> None && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf } + { if not (only_gallina ()) then Output.line_break(); coq_bol lexbuf } | "(**" space_nl { Output.end_coq (); Output.start_doc (); let eol = doc_bol lexbuf in @@ -566,16 +573,12 @@ and coq = parse if eol then coq_bol lexbuf else coq lexbuf } | "(*" { comment_level := 1; - if !Cdglobals.parse_comments then begin - let s = lexeme lexbuf in - let nbsp,isp = count_spaces s in - Output.indentation nbsp; - Output.start_comment (); - end; - let eol = comment lexbuf in - if eol then coq_bol lexbuf - else coq lexbuf - } + let eol = + if parse_comments () then begin + Output.start_comment (); + comment lexbuf + end else skipped_comment lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } | nl+ space* "]]" { if not !formatted then begin @@ -820,9 +823,10 @@ and doc indents = parse | Some is -> doc_list_bol is | None -> doc_bol in - let eol = comment lexbuf in - if eol then bol_parse lexbuf else doc indents lexbuf - } + let eol = + if !Cdglobals.parse_comments then comment lexbuf + else skipped_comment lexbuf in + if eol then bol_parse lexbuf else doc indents lexbuf } | '*'* "*)" space_nl* "(**" {(match indents with | Some _ -> Output.stop_item () @@ -941,7 +945,9 @@ and escaped_coq = parse Output.sublexer_in_doc '['; escaped_coq lexbuf } | "(*" { Tokens.flush_sublexer (); comment_level := 1; - ignore (comment lexbuf); escaped_coq lexbuf } + ignore (if !Cdglobals.parse_comments then comment lexbuf + else skipped_comment lexbuf); + escaped_coq lexbuf } | "*)" { (* likely to be a syntax error: we escape *) backtrack lexbuf } | eof @@ -981,71 +987,78 @@ and comments = parse | _ { Output.char (lexeme_char lexbuf 0); comments lexbuf } -(*s Skip comments *) +and skipped_comment = parse + | "(*" + { incr comment_level; + skipped_comment lexbuf } + | "*)" space* nl + { decr comment_level; + if !comment_level > 0 then skipped_comment lexbuf else true } + | "*)" + { decr comment_level; + if !comment_level > 0 then skipped_comment lexbuf else false } + | eof { false } + | _ { skipped_comment lexbuf } and comment = parse - | "(*" { 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 } - | "*)" { - 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 - if !Cdglobals.plain_comments then Output.char '[' + | "(*" + { incr comment_level; + Output.start_comment (); + comment lexbuf } + | "*)" space* nl + { Output.end_comment (); + Output.line_break (); + decr comment_level; + if !comment_level > 0 then comment lexbuf else true } + | "*)" + { Output.end_comment (); + decr comment_level; + if !comment_level > 0 then comment lexbuf else false } + | "[" + { if !Cdglobals.plain_comments then Output.char '[' else (brackets := 1; Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ()); - comment lexbuf } - | "[[" nl { - if !Cdglobals.parse_comments then - if !Cdglobals.plain_comments then (Output.char '['; Output.char '[') + comment lexbuf } + | "[[" nl + { if !Cdglobals.plain_comments then (Output.char '['; Output.char '[') else (formatted := true; Output.start_inline_coq_block (); let _ = body_bol lexbuf in Output.end_inline_coq_block (); formatted := false); - comment lexbuf} + comment lexbuf } | "$" - { if !Cdglobals.parse_comments then - if !Cdglobals.plain_comments then Output.char '$' - else (Output.start_latex_math (); escaped_math_latex lexbuf); + { if !Cdglobals.plain_comments then Output.char '$' + else (Output.start_latex_math (); escaped_math_latex lexbuf); comment lexbuf } | "$$" - { if !Cdglobals.parse_comments - then - (if !Cdglobals.plain_comments then Output.char '$'; Output.char '$'); - doc None lexbuf } + { if !Cdglobals.plain_comments then Output.char '$'; + Output.char '$'; + comment lexbuf } | "%" - { if !Cdglobals.parse_comments - then - if !Cdglobals.plain_comments then Output.char '%' - else escaped_latex lexbuf; comment lexbuf } + { if !Cdglobals.plain_comments then Output.char '%' + else escaped_latex lexbuf; + comment lexbuf } | "%%" - { if !Cdglobals.parse_comments - then - (if !Cdglobals.plain_comments then Output.char '%'; Output.char '%'); + { if !Cdglobals.plain_comments then Output.char '%'; + Output.char '%'; comment lexbuf } | "#" - { if !Cdglobals.parse_comments - then - if !Cdglobals.plain_comments then Output.char '$' - else escaped_html lexbuf; comment lexbuf } + { if !Cdglobals.plain_comments then Output.char '#' + else escaped_html lexbuf; + comment lexbuf } | "##" - { if !Cdglobals.parse_comments - then - (if !Cdglobals.plain_comments then Output.char '#'; Output.char '#'); + { if !Cdglobals.plain_comments then Output.char '#'; + Output.char '#'; comment lexbuf } | eof { false } - | space+ { if !Cdglobals.parse_comments - then Output.indentation (fst (count_spaces (lexeme lexbuf))); - comment lexbuf } - | nl { if !Cdglobals.parse_comments - then Output.line_break (); comment lexbuf } - | _ { if !Cdglobals.parse_comments then Output.char (lexeme_char lexbuf 0); - comment lexbuf } + | space+ + { Output.indentation (fst (count_spaces (lexeme lexbuf))); + comment lexbuf } + | nl + { Output.line_break (); + comment lexbuf } + | _ { Output.char (lexeme_char lexbuf 0); + comment lexbuf } and skip_to_dot = parse | '.' space* nl { true } @@ -1120,12 +1133,18 @@ and body = parse let eol = doc_bol lexbuf in Output.end_doc (); Output.start_coq (); if eol then body_bol lexbuf else body lexbuf } - | "(*" { Tokens.flush_sublexer(); comment_level := 1; - if !Cdglobals.parse_comments then Output.start_comment (); - let eol = comment lexbuf in - if eol - then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end - else body lexbuf } + | "(*" + { Tokens.flush_sublexer(); comment_level := 1; + let eol = + if parse_comments () then begin + Output.start_comment (); + comment lexbuf + end else begin + let eol = skipped_comment lexbuf in + if eol then Output.line_break(); + eol + end in + if eol then body_bol lexbuf else body lexbuf } | "where" { Tokens.flush_sublexer(); Output.ident (lexeme lexbuf) None; |