diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-01-06 16:03:44 +0100 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-01-06 16:03:44 +0100 |
commit | 91c9e77b8d75a3c04b64337805d2ce335b27c875 (patch) | |
tree | d98973ff87335bd11994df8ed365b4ddf08f4b2a /tools/coqdoc | |
parent | fb6bee00a1b52aecbdccc76bf3aa6edf6ed3df08 (diff) |
Improve error recovery in case of ill-formed coqdoc comment. (Fix for bug #3802.)
Diffstat (limited to 'tools/coqdoc')
-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 ea274a8c4..58d2d1676 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 |