diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/default-layout.html b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/default-layout.html
index c6484163e63721ed083d5184d8974e3644aece43..560388ca788069894560d35e8837c7a1edd3da9a 100644
--- a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/default-layout.html
+++ b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/default-layout.html
@@ -49,5 +49,19 @@
<script language="javascript" src="icons/imgadjust.js" type="text/javascript"></script>
+<div class="footer">
+<hr />
+<img src="icons/deploy-logo-small.png" /> Work sponsored by the <a class="footer" href="http://www.deploy-project.eu/">Deploy Project</a>
+
+| <img src="icons/pdf_icon.gif" /> <a class="footer" href="">Handbook as PDF</a>
+
+| <img src="icons/wikipedia.png" /> <a class="footer" href="http://wiki.event-b.org/">Rodin Wiki</a>
+
+| <a class="footer" rel="license" href="http://creativecommons.org/licenses/by/3.0/">
+<img alt="Creative Commons License" style="border-width:0" src="icons/cc-by.png" /></a>
+Creative Commons License
+
+</div>
+
</body>
</html>
diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/cc-by.png b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/cc-by.png
new file mode 100644
index 0000000000000000000000000000000000000000..ecd2abc73bd3d0bd46b806eb93351c017f15ab22
Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/cc-by.png differ
diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/deploy-logo-small.png b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/deploy-logo-small.png
new file mode 100644
index 0000000000000000000000000000000000000000..8846ba227f0cef79bdd89da0856cceb70dbfcfd4
Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/deploy-logo-small.png differ
diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/pdf_icon.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/pdf_icon.gif
new file mode 100644
index 0000000000000000000000000000000000000000..80f1c395eb2e0e85e1e21218677fa35ab48b74ac
Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/pdf_icon.gif differ
diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/wikipedia.png b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/wikipedia.png
new file mode 100644
index 0000000000000000000000000000000000000000..5428c9b1600b9eb99896d06660bebfd923f5e4ff
Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/wikipedia.png differ
diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/styles/styles.css b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/styles/styles.css
index 03d9c9ed47b4176671729587dd5bc0cb46f85c88..6590d338a5607b507890422d6a4dda38616e7d97 100644
--- a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/styles/styles.css
+++ b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/styles/styles.css
@@ -41,8 +41,6 @@ h1, h2, h3, h4, h5, h6 {
font-weight: normal;
}
-hr {color: black}
-
.minitoc {
border-top: 1px solid black;
border-bottom: 1px solid block;
@@ -218,9 +216,6 @@ table.list td {
margin-bottom: 0px;
}
-/* Rules */
-hr {color: black}
-
/* Image offset classes */
.raise15 {margin-bottom: 10px}
.raise14 {margin-bottom: 10px}
@@ -332,3 +327,16 @@ blockquote p span.rmfamily img {
position: absolute;
left: 0.5em;
}
+
+.footer {
+ font-family: "Lucida Grande", Arial, Helvetica, sans-serif;
+ color: #888;
+ text-align: center;
+}
+
+hr {
+color: #888;
+background-color: #888;
+height: 1px;
+}
+
diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/default-layout.html b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/default-layout.html
index 2264cb0b1ab69d73b21304c9b0ad27ea2c04e21c..146196d352fcfbf265250eb4e6e43cf3df787081 100644
--- a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/default-layout.html
+++ b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/default-layout.html
@@ -26,7 +26,8 @@ Manual
<div id="navcontainer">
<ul id="navlist">
-<li><a href="index.html">Documentation Home</a>
+<li><a href="index.html">Handbook Home</a>
+<li><a href="">Handbook as PDF</a>
<li><a href="http://wiki.event-b.org/">Rodin Wiki</a>
<li><a href="http://sourceforge.net/projects/rodin-b-sharp/">Rodin Download</a>
<li><a href="mailto:michael.jastram@formalmind.com">Contact</a>
@@ -35,8 +36,20 @@ Manual
<br/>
<br/>
-<center>
-<a href="http://www.deploy-project.eu/"><img src="icons/deploy.png" border="0"></a>
+<br/>
+<br/>
+<center id="navlist">
+
+<img src="icons/deploy.png" border="0"><br>
+This work is sponsored by the
+<a href="http://www.deploy-project.eu/">Deploy Project</a><br>
+
+<br/>
+<br/>
+
+<img alt="Creative Commons License" style="border-width:0" src="icons/cc-by.png" /><br />
+This work is licensed under a <a rel="license" href="http://creativecommons.org/licenses/by/3.0/">Creative Commons Attribution 3.0 Unported License</a>
+
</center>
</td><td valign="top" width="40"> </td><td valign="top" >
diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/cc-by.png b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/cc-by.png
new file mode 100644
index 0000000000000000000000000000000000000000..822491edb993b072fc183a2ce23adfa8c94cee7c
Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/cc-by.png differ
diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/pdf_icon.png b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/pdf_icon.png
new file mode 100644
index 0000000000000000000000000000000000000000..b6d2742401281b89915d84a8bc750a757b947ffb
Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/pdf_icon.png differ
diff --git a/org.rodinp.handbook.feature/latex/rodin-doc.tex b/org.rodinp.handbook.feature/latex/rodin-doc.tex
index 6a0b3b9f61c70489b0d95c3be4dd2d4b4f06222a..da53b7119b150d831b0c8e6603a427d3fe1691a4 100644
--- a/org.rodinp.handbook.feature/latex/rodin-doc.tex
+++ b/org.rodinp.handbook.feature/latex/rodin-doc.tex
@@ -51,6 +51,7 @@ This document demonstrates this approach with a very small portion of the existi
By Cliff and/or Jean-Raymond.
\section{Conventions}
+\label{conventions}
We use the following conventions in this manual:
diff --git a/org.rodinp.handbook.feature/latex/style-guide.tex b/org.rodinp.handbook.feature/latex/style-guide.tex
index 37ca09196df5bd3a5f44ae7367ad4e211fdd121e..3e8076c85f1d0b0aaed98d15127c4da0577dbf9f 100644
--- a/org.rodinp.handbook.feature/latex/style-guide.tex
+++ b/org.rodinp.handbook.feature/latex/style-guide.tex
@@ -1,14 +1,26 @@
-\subsection{Style Guide}
+\section{Style Guide}
-\info{For now, we will manage the style guide as \LaTeX together with the rest of the documentation. We may take it out upon publication.}
+\info{For now, we will manage the style guide as \LaTeX~together with the rest of the documentation. We may take it out upon publication.}
\subsubsection{General Stylistic Guidelines}
\begin{itemize}
+ \item The Conventions (\ref{conventions}) are part of the style guide.
\item Use the ``we'' form.
- \item Images must be no more than 600 pixels in width (for HTML version) This is fairly easy for bitmaps (screenshot), pay attention for vector images.
+ \item Images must be no more than 700 pixels in width (for HTML version) This is fairly easy for bitmaps (screenshot), pay attention to this regarding how plastex converts vector images.
\end{itemize}
+\subsubsection{Sections}
+
+\begin{itemize}
+ \item We have a small number of well-defined chapters, the top level structuring element.
+ \item sections and subsections are numbered. In the HTML-Versions, they are broken into subpages.
+ \item subsubsections do not receive numbers and are not broken into subpages in the HTML. Keep this in mind regarding both the reading flow and page sizes.
+ \item Avoid linking (ref) to subsubsections, as they don't have a number. Latex will instead provide a link to the next higher element. It works, but could create confusion.
+ \item Generally, we should avoid gaps in the hierarchy (i.e. having a subsubsection in a section without a subsection inbetween). \footnote{Coincidentally, this style guide violates this rule. Reason: We want the style guide not broken into subpages, but the proper hierarchy is a section.}
+\end{itemize}
+
+
\subsubsection{\LaTeX Styling}
\begin{itemize}