From 7923bb570cd493aff31ac1c94f9e03ff4efd465f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 5 Nov 2020 13:08:14 +0100 Subject: Addressing #13304: how to verbatim an expression mentioning >>. We clarify that there are two kinds of verbatim: inline and block. We add a test testing verbatim and others. Co-authored-by: Xia Li-yao --- test-suite/coqdoc/bug5700.html.out | 6 +- test-suite/coqdoc/bug5700.tex.out | 6 +- test-suite/coqdoc/bug5700.v | 2 +- test-suite/coqdoc/verbatim.html.out | 114 ++++++++++++++++++++++++++++++++++++ test-suite/coqdoc/verbatim.tex.out | 84 ++++++++++++++++++++++++++ test-suite/coqdoc/verbatim.v | 40 +++++++++++++ tools/coqdoc/cpretty.mll | 51 +++++++++------- tools/coqdoc/output.ml | 8 +-- 8 files changed, 278 insertions(+), 33 deletions(-) create mode 100644 test-suite/coqdoc/verbatim.html.out create mode 100644 test-suite/coqdoc/verbatim.tex.out create mode 100644 test-suite/coqdoc/verbatim.v diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out index 286e8bba4d..84214a73d3 100644 --- a/test-suite/coqdoc/bug5700.html.out +++ b/test-suite/coqdoc/bug5700.html.out @@ -22,8 +22,7 @@
-
foo (* bar *)
- + foo (* {bar_bar} *)
Definition const1 := 1.
@@ -32,8 +31,7 @@
-
more (* nested (* comments *) within verbatim *)
- + more (* nested (* comments *) within verbatim *)
Definition const2 := 2.
diff --git a/test-suite/coqdoc/bug5700.tex.out b/test-suite/coqdoc/bug5700.tex.out index 1a1af5dfdd..9dddb00450 100644 --- a/test-suite/coqdoc/bug5700.tex.out +++ b/test-suite/coqdoc/bug5700.tex.out @@ -20,14 +20,12 @@ \begin{coqdoccode} \end{coqdoccode} -\begin{verbatim}foo (* bar *) \end{verbatim} - \begin{coqdoccode} +\texttt{ foo (* \{bar\_bar\} *) } \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} +\texttt{ more (* nested (* comments *) within verbatim *) } \begin{coqdoccode} \coqdocnoindent \coqdockw{Definition} \coqdef{Coqdoc.bug5700.const2}{const2}{\coqdocdefinition{const2}} := 2.\coqdoceol \end{coqdoccode} diff --git a/test-suite/coqdoc/bug5700.v b/test-suite/coqdoc/bug5700.v index 839034a48f..fc985276af 100644 --- a/test-suite/coqdoc/bug5700.v +++ b/test-suite/coqdoc/bug5700.v @@ -1,4 +1,4 @@ -(** << foo (* bar *) >> *) +(** << foo (* {bar_bar} *) >> *) Definition const1 := 1. (** << more (* nested (* comments *) within verbatim *) >> *) diff --git a/test-suite/coqdoc/verbatim.html.out b/test-suite/coqdoc/verbatim.html.out new file mode 100644 index 0000000000..bf9f975ee8 --- /dev/null +++ b/test-suite/coqdoc/verbatim.html.out @@ -0,0 +1,114 @@ + + + + + +Coqdoc.verbatim + + + + +
+ + + +
+ +

Library Coqdoc.verbatim

+ +
+
+ +
+ +
+ +
+uint32_t shift_right( uint32_t a, uint32_t shift )
+{
+    return a >> shift;
+}
+
+ +
+ +This line and the following shows verbatim text: + +
+ + A stand-alone inline verbatim + +
+ + A non-ended inline verbatim to test line location + + +
+ +
    +
  • item 1 + +
    • +
  • item 2 is verbatim + +
    • +
  • item 3 is verbatim too +
    +A coq block : ∀ n, n = 0 +
    + +     +
    • +
  • verbatim again, and a formula True → False + +
    • +
  • +
    +multiline
+verbatim
+
    + +
    • +
  • last item + +
    • +
+ +
+ +
+ + + + + + + + + + +
Γ ⊢ A +   +
Γ ⊢ A ∨ B
+
+ +
+A non-ended block verbatim to test line location
+
+*)
+
+
+
+
+
+ + + +
+ + + \ No newline at end of file diff --git a/test-suite/coqdoc/verbatim.tex.out b/test-suite/coqdoc/verbatim.tex.out new file mode 100644 index 0000000000..b692f6ad6a --- /dev/null +++ b/test-suite/coqdoc/verbatim.tex.out @@ -0,0 +1,84 @@ +\documentclass[12pt]{report} +\usepackage[utf8x]{inputenc} + +%Warning: tipa declares many non-standard macros used by utf8x to +%interpret utf8 characters but extra packages might have to be added +%such as "textgreek" for Greek letters not already in tipa +%or "stmaryrd" for mathematical symbols. +%Utf8 codes missing a LaTeX interpretation can be defined by using +%\DeclareUnicodeCharacter{code}{interpretation}. +%Use coqdoc's option -p to add new packages or declarations. +\usepackage{tipa} + +\usepackage[T1]{fontenc} +\usepackage{fullpage} +\usepackage{coqdoc} +\usepackage{amsmath,amssymb} +\usepackage{url} +\begin{document} +\coqlibrary{Coqdoc.verbatim}{Library }{Coqdoc.verbatim} + +\begin{coqdoccode} +\end{coqdoccode} + + +\begin{verbatim} +uint32_t shift_right( uint32_t a, uint32_t shift ) +{ + return a >> shift; +} +\end{verbatim} + + +This line and the following shows \texttt{verbatim } text: + + +\texttt{ A stand-alone inline verbatim } + + +\texttt{ A non-ended inline verbatim to test line location +} + + + +\begin{itemize} +\item item 1 + +\item item 2 is \texttt{verbatim} + +\item item 3 is \texttt{verbatim} too +\coqdoceol +\coqdocemptyline +\coqdocnoindent +\coqdocvar{A} \coqdocvar{coq} \coqdocvar{block} : \coqdockw{\ensuremath{\forall}} \coqdocvar{n}, \coqdocvar{n} = 0 + +\coqdocemptyline + +\item \texttt{verbatim} again, and a formula \coqdocvar{True} \ensuremath{\rightarrow} \coqdocvar{False} + +\item +\begin{verbatim} +multiline +verbatim +\end{verbatim} + +\item last item + +\end{itemize} + + +\begin{verbatim} +Γ ⊢ A +---- +Γ ⊢ A ∨ B +\end{verbatim} + + +\begin{verbatim} +A non-ended block verbatim to test line location + +*) +\end{verbatim} +\begin{coqdoccode} +\end{coqdoccode} +\end{document} diff --git a/test-suite/coqdoc/verbatim.v b/test-suite/coqdoc/verbatim.v new file mode 100644 index 0000000000..129a5117c9 --- /dev/null +++ b/test-suite/coqdoc/verbatim.v @@ -0,0 +1,40 @@ +(** + +<< +uint32_t shift_right( uint32_t a, uint32_t shift ) +{ + return a >> shift; +} +>> + +This line and the following shows << verbatim >> text: + +<< A stand-alone inline verbatim >> + +<< A non-ended inline verbatim to test line location + + +- item 1 +- item 2 is <> +- item 3 is <> too +[[ +A coq block : forall n, n = 0 +]] +- <> again, and a formula [ True -> False ] +- +<< +multiline +verbatim +>> +- last item + +[[[ +Γ ⊢ A +---- +Γ ⊢ A ∨ B +]]] + +<< +A non-ended block verbatim to test line location + +*) diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index d056887591..f2b6a3f38f 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -748,8 +748,10 @@ and doc_bol = parse } | (space_nl* nl) as s { new_lines (count_newlines s) lexbuf; Output.paragraph (); doc_bol lexbuf } - | "<<" space* - { Output.start_verbatim false; verbatim 0 false lexbuf; doc_bol lexbuf } + | "<<" space* nl + { new_lines 1 lexbuf; Output.start_verbatim false; verbatim_block lexbuf; doc_bol lexbuf } + | "<<" + { Output.start_verbatim true; verbatim_inline lexbuf; doc None lexbuf } | eof { true } | '_' @@ -771,10 +773,14 @@ and doc_list_bol indents = parse | InLevel (_,false) -> backtrack lexbuf; doc_bol lexbuf } - | "<<" space* - { Output.start_verbatim false; - verbatim 0 false lexbuf; + | "<<" space* nl + { new_lines 1 lexbuf; Output.start_verbatim false; + verbatim_block lexbuf; doc_list_bol indents lexbuf } + | "<<" space* + { Output.start_verbatim true; + verbatim_inline lexbuf; + doc (Some indents) lexbuf } | "[[" nl { new_lines 1 lexbuf; formatted := Some lexbuf.lex_start_p; Output.start_inline_coq_block (); @@ -921,7 +927,7 @@ and doc indents = parse Output.char (lexeme_char lexbuf 1); doc indents lexbuf } | "<<" space* - { Output.start_verbatim true; verbatim 0 true lexbuf; doc_bol lexbuf } + { Output.start_verbatim true; verbatim_inline lexbuf; doc indents lexbuf } | '"' { if !Cdglobals.plain_comments then Output.char '"' @@ -961,20 +967,25 @@ and escaped_html = parse { backtrack lexbuf } | _ { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf } -and verbatim depth inline = parse - | nl ">>" space* nl { new_lines 2 lexbuf; Output.verbatim_char inline '\n'; Output.stop_verbatim inline } - | nl ">>" { new_lines 1 lexbuf; Output.verbatim_char inline '\n'; Output.stop_verbatim inline } - | ">>" { Output.stop_verbatim inline } - | "(*" { 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 depth inline lexbuf } +and verbatim_block = parse + | nl ">>" space* nl { new_lines 2 lexbuf; Output.verbatim_char false '\n'; Output.stop_verbatim false } + | nl ">>" + { new_lines 1 lexbuf; + warn "missing newline after \">>\" block" lexbuf; + Output.verbatim_char false '\n'; + Output.stop_verbatim false } + | eof { warn "unterminated \">>\" block" lexbuf; Output.stop_verbatim false } + | nl { new_lines 1 lexbuf; Output.verbatim_char false (lexeme_char lexbuf 0); verbatim_block lexbuf } + | _ { Output.verbatim_char false (lexeme_char lexbuf 0); verbatim_block lexbuf } + +and verbatim_inline = parse + | nl { new_lines 1 lexbuf; + warn "unterminated inline \">>\"" lexbuf; + Output.char '\n'; + Output.stop_verbatim true } + | ">>" { Output.stop_verbatim true } + | eof { warn "unterminated inline \">>\"" lexbuf; Output.stop_verbatim true } + | _ { Output.verbatim_char true (lexeme_char lexbuf 0); verbatim_inline lexbuf } and url = parse | "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer } diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index a6165918f9..57b2b6e620 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -313,7 +313,7 @@ module Latex = struct let start_verbatim inline = if inline then printf "\\texttt{" - else printf "\\begin{verbatim}" + else printf "\\begin{verbatim}\n" let stop_verbatim inline = if inline then printf "}" @@ -628,11 +628,11 @@ module Html = struct let stop_quote () = start_quote () let start_verbatim inline = - if inline then printf "" - else printf "
"
+    if inline then printf ""
+    else printf "
\n"
 
   let stop_verbatim inline =
-    if inline then printf ""
+    if inline then printf ""
     else printf "
\n"
 
   let url addr name =
-- 
cgit v1.2.3