diff options
Diffstat (limited to 'tools/coqdoc/cpretty.mll')
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 235 |
1 files changed, 125 insertions, 110 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 431080c6..919f37b9 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -75,7 +75,7 @@ let stop_env () = if !r then stop (); r := false in (fun x -> !r), start_env, stop_env - let in_emph, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph + let _, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph let in_quote, start_quote, stop_quote = in_env Output.start_quote Output.stop_quote let url_buffer = Buffer.create 40 @@ -111,12 +111,6 @@ Cdglobals.gallina := s.st_gallina; Cdglobals.light := s.st_light - let without_ref r f x = save_state (); r := false; f x; restore_state () - - let without_gallina = without_ref Cdglobals.gallina - - let without_light = without_ref Cdglobals.light - let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false let end_show () = restore_state () @@ -245,6 +239,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 +486,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 +535,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 { () } | _ @@ -550,7 +551,7 @@ rule coq_bol = parse if not !Cdglobals.gallina then begin backtrack lexbuf; body_bol lexbuf end else - skip_to_dot lexbuf + skip_to_dot_or_brace lexbuf in if eol then coq_bol lexbuf else coq lexbuf } @@ -558,7 +559,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 +567,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 @@ -650,7 +647,7 @@ and coq = parse if not !Cdglobals.gallina then begin backtrack lexbuf; body lexbuf end else - skip_to_dot lexbuf + skip_to_dot_or_brace lexbuf in if eol then coq_bol lexbuf else coq lexbuf} @@ -678,7 +675,7 @@ and doc_bol = parse in match check_start_list line with | Neither -> backtrack_past_newline lexbuf; doc None lexbuf - | List n -> Output.paragraph (); + | List n -> if lines > 0 then Output.paragraph (); Output.item 1; doc (Some [n]) lexbuf | Rule -> Output.rule (); doc None lexbuf } @@ -739,24 +736,7 @@ and doc_list_bol indents = parse in let (n_spaces,_) = count_spaces buf in match find_level indents n_spaces with - | InLevel _ -> - Output.paragraph (); - backtrack_past_newline lexbuf; - doc_list_bol indents lexbuf - | StartLevel n -> - if n = 1 then - begin - Output.stop_item (); - backtrack_past_newline lexbuf; - doc_bol lexbuf - end - else - begin - Output.paragraph (); - backtrack_past_newline lexbuf; - doc_list_bol indents lexbuf - end - | Before -> + | StartLevel 1 | Before -> (* Here we were at the beginning of a line, and it was blank. The next line started before any list items. So: insert a paragraph for the empty line, rewind to whatever's just @@ -766,6 +746,10 @@ and doc_list_bol indents = parse Output.paragraph (); backtrack_past_newline lexbuf; doc_bol lexbuf + | StartLevel _ | InLevel _ -> + Output.paragraph (); + backtrack_past_newline lexbuf; + doc_list_bol indents lexbuf } | space* _ @@ -774,10 +758,7 @@ and doc_list_bol indents = parse | Before -> Output.stop_item (); backtrack lexbuf; doc_bol lexbuf | StartLevel n -> - (if n = 1 then - Output.stop_item () - else - Output.reach_item_level (n-1)); + Output.reach_item_level (n-1); backtrack lexbuf; doc (Some (take (n-1) indents)) lexbuf | InLevel (n,_) -> @@ -820,9 +801,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 +923,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,76 +965,101 @@ 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 } | eof | '.' space+ { false } - | "(*" { comment_level := 1; ignore (comment lexbuf); skip_to_dot lexbuf } + | "(*" + { comment_level := 1; + ignore (skipped_comment lexbuf); + skip_to_dot lexbuf } + | _ { skip_to_dot lexbuf } + +and skip_to_dot_or_brace = parse + | '.' space* nl { true } + | eof | '.' space+ { false } + | "(*" + { comment_level := 1; + ignore (skipped_comment lexbuf); + skip_to_dot_or_brace lexbuf } + | "}" space* nl + { true } + | "}" + { false } + | space* + { skip_to_dot_or_brace lexbuf } | _ { skip_to_dot lexbuf } and body_bol = parse @@ -1120,12 +1129,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; |