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 +++++++++++++ 6 files changed, 243 insertions(+), 9 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 (limited to 'test-suite') 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 + +*) -- cgit v1.2.3