From 91c9e77b8d75a3c04b64337805d2ce335b27c875 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 6 Jan 2015 16:03:44 +0100
Subject: Improve error recovery in case of ill-formed coqdoc comment. (Fix for
 bug #3802.)

---
 tools/coqdoc/cpretty.mll | 6 ++++++
 1 file changed, 6 insertions(+)

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
-- 
cgit v1.2.3