diff options
| author |  Tej Chajed <tchajed@mit.edu> | 2017-08-28 14:57:43 +0100 |
|---|---|---|
| committer | Tej Chajed <tchajed@mit.edu> | 2017-08-29 09:49:56 +0100 |
| commit | 13e33e52869d6c863eaa307f9eb5661b6eeeef93 (patch) | |
| tree | 1b74bca23d057e8513ba2d8a3088088ee2977155 /tools/coqdoc | |
| parent | 7b1ff0c70a3ba9cd3cfa5aa6723f8f8a2b6e5396 (diff) | |
coqdoc: Support comments in verbatim output
Fixes BZ#5700
Diffstat (limited to 'tools/coqdoc')
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 60a245dc4..186f6cf6c 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -682,7 +682,7 @@ and doc_bol = parse | space* nl+ { Output.paragraph (); doc_bol lexbuf } | "<<" space* - { Output.start_verbatim false; verbatim false lexbuf; doc_bol lexbuf } + { Output.start_verbatim false; verbatim 0 false lexbuf; doc_bol lexbuf } | eof { true } | '_' @@ -707,7 +707,7 @@ and doc_list_bol indents = parse } | "<<" space* { Output.start_verbatim false; - verbatim false lexbuf; + verbatim 0 false lexbuf; doc_list_bol indents lexbuf } | "[[" nl { formatted := true; @@ -852,7 +852,7 @@ and doc indents = parse Output.char (lexeme_char lexbuf 1); doc indents lexbuf } | "<<" space* - { Output.start_verbatim true; verbatim true lexbuf; doc_bol lexbuf } + { Output.start_verbatim true; verbatim 0 true lexbuf; doc_bol lexbuf } | '"' { if !Cdglobals.plain_comments then Output.char '"' @@ -892,13 +892,20 @@ and escaped_html = parse { backtrack lexbuf } | _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf } -and verbatim inline = parse +and verbatim depth inline = parse | nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline } | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline } | ">>" { Output.stop_verbatim inline } - | "*)" { Output.stop_verbatim inline; backtrack lexbuf } + | "(*" { Output.verbatim_char inline '('; + Output.verbatim_char inline '*'; + verbatim (depth+1) inline lexbuf } + | "*)" { if (depth == 0) + then (Output.stop_verbatim inline; backtrack lexbuf) + else (Output.verbatim_char inline '*'; + Output.verbatim_char inline ')'; + verbatim (depth-1) inline lexbuf) } | eof { Output.stop_verbatim inline } - | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim inline lexbuf } + | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim depth inline lexbuf } and url = parse | "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer } |