diff options
Diffstat (limited to 'tools/coqdoc/cpretty.mll')
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 29 |
1 files changed, 19 insertions, 10 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 919f37b9..1be440a7 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*s Utility functions for the scanners *) @@ -682,7 +684,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 +709,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 +854,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 +894,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 } |