diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index ea274a8c48..58d2d16760 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -893,11 +893,15 @@ and doc indents = parse and escaped_math_latex = parse | "$" { Output.stop_latex_math () } | eof { Output.stop_latex_math () } + | "*)" + { Output.stop_latex_math (); backtrack lexbuf } | _ { Output.latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf } and escaped_latex = parse | "%" { () } | eof { () } + | "*)" + { backtrack lexbuf } | _ { Output.latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf } and escaped_html = parse @@ -907,6 +911,8 @@ and escaped_html = parse | "##" { Output.html_char '#'; escaped_html lexbuf } | eof { () } + | "*)" + { backtrack lexbuf } | _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf } and verbatim inline = parse |