From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 tools/coqdoc/cpretty.mll | 29 +++++++++++++++++++----------
 1 file changed, 19 insertions(+), 10 deletions(-)

(limited to 'tools/coqdoc/cpretty.mll')

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