Improve error recovery in case of ill-formed coqdoc comment. (Fix for bug #3802.)

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