From 13e33e52869d6c863eaa307f9eb5661b6eeeef93 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Mon, 28 Aug 2017 14:57:43 +0100 Subject: coqdoc: Support comments in verbatim output Fixes BZ#5700 --- test-suite/coqdoc/bug5700.html.out | 50 ++++++++++++++++++++++++++++++++++++++ test-suite/coqdoc/bug5700.tex.out | 24 ++++++++++++++++++ test-suite/coqdoc/bug5700.v | 5 ++++ tools/coqdoc/cpretty.mll | 19 ++++++++++----- 4 files changed, 92 insertions(+), 6 deletions(-) create mode 100644 test-suite/coqdoc/bug5700.html.out create mode 100644 test-suite/coqdoc/bug5700.tex.out create mode 100644 test-suite/coqdoc/bug5700.v diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out new file mode 100644 index 0000000000..0e05660d6c --- /dev/null +++ b/test-suite/coqdoc/bug5700.html.out @@ -0,0 +1,50 @@ + + + + + +Coqdoc.bug5700 + + + + +
+ + + +
+ +

Library Coqdoc.bug5700

+ +
+
+ +
+
foo (* bar *)
+ +
+
+Definition const1 := 1.
+ +
+
+ +
+
more (* nested (* comments *) within verbatim *)
+ +
+
+Definition const2 := 2.
+
+
+ + + +
+ + + \ No newline at end of file diff --git a/test-suite/coqdoc/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out new file mode 100644 index 0000000000..33990cb89f --- /dev/null +++ b/test-suite/coqdoc/bug5700.tex.out @@ -0,0 +1,24 @@ +\documentclass[12pt]{report} +\usepackage[]{inputenc} +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.bug5700}{Library }{Coqdoc.bug5700} + +\begin{coqdoccode} +\end{coqdoccode} +\begin{verbatim}foo (* bar *) \end{verbatim} + \begin{coqdoccode} +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.bug5700.const1}{const1}{\coqdocdefinition{const1}} := 1.\coqdoceol +\coqdocemptyline +\end{coqdoccode} +\begin{verbatim}more (* nested (* comments *) within verbatim *) \end{verbatim} + \begin{coqdoccode} +\coqdocnoindent +\coqdockw{Definition} \coqdef{Coqdoc.bug5700.const2}{const2}{\coqdocdefinition{const2}} := 2.\coqdoceol +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/bug5700.v b/test-suite/coqdoc/bug5700.v new file mode 100644 index 0000000000..839034a48f --- /dev/null +++ b/test-suite/coqdoc/bug5700.v @@ -0,0 +1,5 @@ +(** << foo (* bar *) >> *) +Definition const1 := 1. + +(** << more (* nested (* comments *) within verbatim *) >> *) +Definition const2 := 2. diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 60a245dc4d..186f6cf6cf 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -682,7 +682,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 +707,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 +852,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 +892,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