HTML pdf doc generation fixes

wkhtmltopdf isn't using a fixed-width font for CSS font-family:monospace.
Nor is it using one for <PRE> <CODE> or <TT> elements.
Add in some Courier fonts for it to use - note that Courier 10 Pitch is
installed on Ubuntu by default. Note these fonts need to be installed on
the system that generates the pdf documentation.

Previously the htmldoc stylesheet was kept in place and the SWIG
stylesheet was prepended to it inline in SWIGDocumentation.html.
Now the SWIG stylesheet has been amended with most of the htmldoc
stylesheet changes and completely replaced after htmldoc is run.

3 files changed, 20 insertions, 7 deletions

diff --git a/Doc/Manual/Makefile b/Doc/Manual/Makefile
index 2c90e91e5..c7769dc97 100644
--- a/Doc/Manual/Makefile
+++ b/Doc/Manual/Makefile
@@ -39,7 +39,7 @@ check:
 #  2) Tabs in <pre> elements should be expanded to 8 spaces by default, but
 #     are expanded to just one space and css tab-size is not working.
 #  3) <pre> <tt> <code> elements do not always select a fixed-width font - try installing the
-#     Courier font to fix.
+#     Courier font to fix - these have been added to style.css.
 generate: SWIGDocumentation.html
 	wkhtmltopdf --margin-top 20mm --margin-bottom 20mm --margin-left 10mm --margin-right 10mm --header-font-size 6 --footer-font-size 6 --header-spacing 6 --footer-spacing 6 --header-center '[doctitle]' --footer-left '[subsection]' --footer-right '[page]' SWIGDocumentation.html SWIGDocumentation.pdf
 
diff --git a/Doc/Manual/fixstyle.py b/Doc/Manual/fixstyle.py
index 1007d5949..a36096890 100644
--- a/Doc/Manual/fixstyle.py
+++ b/Doc/Manual/fixstyle.py
@@ -1,6 +1,6 @@
 #!/usr/bin/python
 
-# Adds the SWIG stylesheet to the generated documentation on a single page
+# Replace the inline htmldoc stylesheet with the SWIG stylesheet
 
 import sys
 import string
@@ -14,11 +14,16 @@ swigstyle = "\n" + open("style.css").read()
 
 lines = data.splitlines()
 result = [ ]
+skip = False
 for s in lines:
-	if s == "<STYLE TYPE=\"text/css\"><!--":
-		result.append(s + swigstyle)
-	else:
-		result.append(s)
+    if not skip:
+        result.append(s)
+    if s == "<STYLE TYPE=\"text/css\"><!--":
+        result.append(swigstyle)
+        skip = True
+    elif s == "--></STYLE>":
+        result.append(s)
+        skip = False
 
 data = "\n".join(result)
 
diff --git a/Doc/Manual/style.css b/Doc/Manual/style.css
index 02329e56f..45e51e35b 100644
--- a/Doc/Manual/style.css
+++ b/Doc/Manual/style.css
@@ -32,6 +32,7 @@ div.code {
   margin-left: 4em;
   margin-right: 4em;
   background-color: #F0FFFF;
+  font-family: "Courier New", Courier, "Courier 10 Pitch", monospace;
 }
 
 div.targetlang {
@@ -41,9 +42,9 @@ div.targetlang {
   margin-left: 4em;
   margin-right: 4em;
   background-color: #d7f6bb;
+  font-family: "Courier New", Courier, "Courier 10 Pitch", monospace;
 }
 
-
 div.shell {
   border-style: solid; 
   border-width: 1px; 
@@ -51,6 +52,7 @@ div.shell {
   margin-left: 4em;
   margin-right: 4em;
   background-color: #DCDCDC;
+  font-family: "Courier New", Courier, "Courier 10 Pitch", monospace;
 }
 
 div.diagram {
@@ -60,6 +62,7 @@ div.diagram {
   margin-left: 4em;
   margin-right: 4em;
   background-color: #FFEBCD;
+  font-family: "Courier New", Courier, "Courier 10 Pitch", monospace;
 }
 
 ul li p {
@@ -82,3 +85,8 @@ div.indent p {
   margin-right: 0;
 }
 
+pre, code, tt {
+  font-family: "Courier New", Courier, "Courier 10 Pitch", monospace;
+}
+
+body { font-family: serif; }