From ecc1e64d50b82950881de1d32879bca0091e6e64 Mon Sep 17 00:00:00 2001
From: Claude Marche <cmarche@dispater.(none)>
Date: Sat, 20 Oct 2012 10:44:58 +0200
Subject: [PATCH] fix small problems with HTML version of the manual

---
 Makefile.in      |  2 +-
 doc/macros.tex   |  2 +-
 doc/manpages.tex | 30 ++++++++++++++----------------
 doc/manual.tex   | 13 ++++++-------
 4 files changed, 22 insertions(+), 25 deletions(-)

diff --git a/Makefile.in b/Makefile.in
index 65bea5f1ef..c38921db9c 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -1229,7 +1229,7 @@ doc/manual.pdf: $(BNFTEX) $(DOCTEX) doc/manual.bib
 # the dependency on the pdf ensures the bbl was built
 doc/html/manual.html: doc/manual.pdf doc/fix.hva
 	cd doc; rm -rf html; mkdir -p html
-	cp doc/manual.bbl doc/html/
+	cp doc/*.png doc/manual.bbl doc/html/
 	cd doc; $(HEVEA) -o html/manual.html -fix -O fix.hva makeidx.hva manual.tex
 
 doc/html/index.html: doc/html/manual.html
diff --git a/doc/macros.tex b/doc/macros.tex
index 961b76f391..cb9423c202 100644
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -9,7 +9,7 @@
 \newcommand{\emptyitem}{%
 %BEGIN LATEX
 ~
-%ENDLATEX
+%END LATEX
 }
 
 % BNF grammar
diff --git a/doc/manpages.tex b/doc/manpages.tex
index 5d9aacf8a9..7f03173adf 100644
--- a/doc/manpages.tex
+++ b/doc/manpages.tex
@@ -410,9 +410,8 @@ are groups together under several tabs
   the editor to use will be set to ``CoqIDE'' by default, and this
   \urldef{\urlprfgen}{\url}{http://proofgeneral.inf.ed.ac.uk/}
   dialog allows you to select the Emacs editor and its
-\todo{uncomment the following}
-%  \ahref{\urlprfgen}{Proof General} mode instead%
-%  \begin{latexonly} (\urlprfgen)\end{latexonly}.
+ \ahref{\urlprfgen}{Proof General} mode instead%
+ \begin{latexonly} (\urlprfgen)\end{latexonly}.
 \end{itemize}
 \item[\textsf{Provers} tab]
   allows to select which of the installed provers one wants to see
@@ -842,19 +841,18 @@ There are three styles of output: `table', `simpletree', and
 %BEGIN LATEX
 \fbox{\includegraphics[width=0.9\textwidth]{hello_proof.png}}
 %END LATEX
-\todo{uncomment the following}
-% \begin{htmlonly}
-% \begin{rawhtml}
-% <table border="1"><tr><td colspan="2">Obligations</td><td text-rotation="90">Alt-Ergo (0.94)</td><td text-rotation="90">Coq (8.3pl4)</td><td text-rotation="90">Simplify (1.5.4)</td></td></tr>
-% <td bgcolor="#C0FFC0" colspan="2">G1</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#C0FFC0">0.00</td></tr>
-% <td bgcolor="#FF0000" colspan="2">G2</td><td bgcolor="#FF8000">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#FF8000">0.00</td></tr>
-% <tr><td bgcolor="#FF0000" colspan="2">split_goal</td><td bgcolor="#E0E0E0"></td><td bgcolor="#E0E0E0"></td><td bgcolor="#E0E0E0"></td></tr>
-% <td rowspan="2">&nbsp;&nbsp;</td><td bgcolor="#FF0000" colspan="1">G2.1</td><td bgcolor="#FF8000">0.00</td><td bgcolor="#FF8000">0.49</td><td bgcolor="#FF8000">0.00</td></tr>
-% <tr><td bgcolor="#C0FFC0" colspan="1">G2.2</td><td bgcolor="#C0FFC0">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#C0FFC0">0.00</td></tr>
-% <td bgcolor="#C0FFC0" colspan="2">G3</td><td bgcolor="#C0FFC0">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#FF8000">0.00</td></tr>
-% </table>
-% \end{rawhtml}
-% \end{htmlonly}
+\begin{htmlonly}
+\begin{rawhtml}
+<table border="1"><tr><td colspan="2">Obligations</td><td text-rotation="90">Alt-Ergo (0.94)</td><td text-rotation="90">Coq (8.3pl4)</td><td text-rotation="90">Simplify (1.5.4)</td></td></tr>
+<td bgcolor="#C0FFC0" colspan="2">G1</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#C0FFC0">0.00</td></tr>
+<td bgcolor="#FF0000" colspan="2">G2</td><td bgcolor="#FF8000">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#FF8000">0.00</td></tr>
+<tr><td bgcolor="#FF0000" colspan="2">split_goal</td><td bgcolor="#E0E0E0"></td><td bgcolor="#E0E0E0"></td><td bgcolor="#E0E0E0"></td></tr>
+<td rowspan="2">&nbsp;&nbsp;</td><td bgcolor="#FF0000" colspan="1">G2.1</td><td bgcolor="#FF8000">0.00</td><td bgcolor="#FF8000">0.49</td><td bgcolor="#FF8000">0.00</td></tr>
+<tr><td bgcolor="#C0FFC0" colspan="1">G2.2</td><td bgcolor="#C0FFC0">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#C0FFC0">0.00</td></tr>
+<td bgcolor="#C0FFC0" colspan="2">G3</td><td bgcolor="#C0FFC0">0.00</td><td bgcolor="#E0E0E0">---</td><td bgcolor="#FF8000">0.00</td></tr>
+</table>
+\end{rawhtml}
+\end{htmlonly}
 \end{center}
 \caption{HTML table produced for the HelloProof example}
 \label{fig:html}
diff --git a/doc/manual.tex b/doc/manual.tex
index f7780cf545..9f57c67afa 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -21,7 +21,7 @@
 
 \usepackage{listings}
 \usepackage{xspace}
-%\usepackage{hevea}
+\usepackage{hevea}
 
 %BEGIN LATEX
 \setulmarginsandblock{30mm}{30mm}{*}
@@ -134,12 +134,11 @@ $^2$ Inria Saclay -- \^Ile-de-France, Toccata, Palaiseau, F-91120
 \urldef{\urlutcat}{\url}{http://frama-c.cea.fr/u3cat}
 \urldef{\urlhilite}{\url}{http://www.open-do.org/projects/hi-lite/}
 
-\todo{uncomment the following}
-  % This work has been partly supported by the `\ahref{\urlutcat}{U3CAT}'
-  % national ANR project (ANR-08-SEGI-021-08\begin{latexonly},
-  % \urlutcat\end{latexonly}) and by the `\ahref{\urlhilite}{Hi-Lite}'
-  % \begin{latexonly}(\urlhilite)\end{latexonly} FUI project of the
-  % System@tic competitivity cluster.
+  This work has been partly supported by the `\ahref{\urlutcat}{U3CAT}'
+  national ANR project (ANR-08-SEGI-021-08\begin{latexonly},
+  \urlutcat\end{latexonly}) and by the `\ahref{\urlhilite}{Hi-Lite}'
+  \begin{latexonly}(\urlhilite)\end{latexonly} FUI project of the
+  System@tic competitivity cluster.
 
 \end{flushleft}
 \end{center}
-- 
GitLab