Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit ecc1e64d authored by Claude Marche's avatar Claude Marche

fix small problems with HTML version of the manual

parent a431393b
......@@ -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
......
......@@ -9,7 +9,7 @@
\newcommand{\emptyitem}{%
%BEGIN LATEX
~
%ENDLATEX
%END LATEX
}
% BNF grammar
......
......@@ -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}
......
......@@ -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}
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment