Updates and new images

14 files changed, 72 insertions, 17 deletions

diff --git a/images/Makefile b/images/Makefile
index 62e5943a..a5f35f56 100644
--- a/images/Makefile
+++ b/images/Makefile
@@ -20,11 +20,14 @@
 
 # Sources
 BUTTONS=goal.xcf next.xcf qed.xcf restart.xcf retract.xcf undo.xcf use.xcf
-WEBPIX=isabelle_transparent.xcf ProofGeneral.xcf text_general.xcf text_proof.xcf
+WEBPIX=isabelle_transparent.xcf ProofGeneral.xcf pg-text.xcf
 
 # Targets for html directory
 WEBPIX_ONLY=
-WEBPIX_TARGETS=$(WEBPIX_ONLY) ProofGeneral.jpg text_general.gif text_proof.gif
+WEBPIX_TARGETS=$(WEBPIX_ONLY) ProofGeneral.jpg pg-text.gif
+# Targets for doc directory
+DOCPIX_TARGETS=ProofGeneral.jpg
+
 # Junk not wanted
 UNWANTED=text_general.jpg text_proof.jpg
 
@@ -66,7 +69,9 @@ clean:
 	rm -f $(WEBPIX_ONLY) $(UNWANTED)
 
 install: webpix
-	cp -pf $(WEBPIX_TARGETS) ../html
+	cp -pf $(WEBPIX_TARGETS) ../html/images
+	cp -pf $(DOCPIX_TARGETS) ../doc
+
 ##
 ## Batch mode is a bit broken on The Gimp at the moment (v 1.0)
 ## For script fu, at least, it seems tricky to pass arguments to
diff --git a/images/ProofGeneral.8bit.gif b/images/ProofGeneral.8bit.gif
index 7aab1cae..dfb182be 100644
--- a/images/ProofGeneral.8bit.gif
+++ b/images/ProofGeneral.8bit.gif
diff --git a/images/ProofGeneral.gif b/images/ProofGeneral.gif
index a67429f7..ed91610c 100644
--- a/images/ProofGeneral.gif
+++ b/images/ProofGeneral.gif
diff --git a/images/ProofGeneral.jpg b/images/ProofGeneral.jpg
index 2b23f03b..6d5bfbfe 100644
--- a/images/ProofGeneral.jpg
+++ b/images/ProofGeneral.jpg
diff --git a/images/ProofGeneral.xcf b/images/ProofGeneral.xcf
index 27c1b4ef..d651749d 100644
--- a/images/ProofGeneral.xcf
+++ b/images/ProofGeneral.xcf
diff --git a/images/coq-badge.xcf b/images/coq-badge.xcf
new file mode 100644
index 00000000..98ba6ded
--- /dev/null
+++ b/images/coq-badge.xcf
diff --git a/images/gimp/scripts/proofgeneral.scm b/images/gimp/scripts/proofgeneral.scm
index 9491655e..7c67d5b5 100644
--- a/images/gimp/scripts/proofgeneral.scm
+++ b/images/gimp/scripts/proofgeneral.scm
@@ -66,7 +66,8 @@
     ;; Flatten and save as jpg
     ;;(gimp-image-flatten image)
     ;; Flattening forces a white background.  Let's use merge.
-    (gimp-image-merge-visible-layers image 0)
+    (if (> (car (gimp-image-get-layers image)) 1)
+	(gimp-image-merge-visible-layers image 0))
     (file-jpeg-save 1 image (car (gimp-image-active-drawable image))
 		    jpgname jpgname
 		    0.75 0 1)
@@ -96,7 +97,7 @@
 
 (define (script-fu-proofgeneral-save-all-pix)
   (mapcar script-fu-proofgeneral-save-pic
-	  '("ProofGeneral" "text_proof" "text_general")))
+	  '("ProofGeneral" "pg-text")))
 
 (script-fu-register "script-fu-proofgeneral-save-all-jpegs" 
 		    "<Toolbox>/Xtns/Script-Fu/Proof General/Save all Jpegs"
diff --git a/images/isabelle-badge.xcf b/images/isabelle-badge.xcf
new file mode 100644
index 00000000..ad5de7bd
--- /dev/null
+++ b/images/isabelle-badge.xcf
diff --git a/images/lego-badge.xcf b/images/lego-badge.xcf
new file mode 100644
index 00000000..c0a2985d
--- /dev/null
+++ b/images/lego-badge.xcf
diff --git a/images/notes.txt b/images/notes.txt
index c58eafc3..2d4e0a9a 100644
--- a/images/notes.txt
+++ b/images/notes.txt
@@ -1,11 +1,16 @@
 $Id$
 
-Notes about icons here (not for distribution).
-==============================================
+Notes about how I made the icons and logos here  (not for distribution).
+========================================================================
+					David Aspinall <da@dcs.ed.ac.uk>
 
-Icons to fit on the (default size) Emacs toolbars are 32x32.
-The ones with pictures were made at 256x256, then shrunk
-to have text added.
+ICONS
+=====
+
+Made with the Gimp.
+
+Icons to fit on the (default size) Emacs toolbars are 32x32.  The ones
+with pictures were made at 256x256, then shrunk to have text added.
 
 Background grey is V74.
 Red for buttons is 135,13,13.
@@ -20,9 +25,10 @@ Text is lucidafax at point size 8.
 blank.xcf -- blank with correct background colour.
 
 
----
+LOGOS
+=====
 
-Proof general Text logo:
+Original text logo:
 
 script fu -> logos -> comic book
 
@@ -33,15 +39,58 @@ script fu -> logos -> comic book
 
 Then I filled background with web page colour, and shaded portion
 with green colour.
+
+New text logo: same font, but made in blender file.
  
-----
 
-Proof general logo:
+Proof general logos
+===================
+
+Web page: scene with canvas backdrop.  Render in blender at full size,
+then use gimp to scale to web size (250pix wide).  This gives much
+nicer result than low-resolution render: textures are smoothed out
+more prettily.
 
-Saved as eps for texi documentation.  
+EPS (doc/ProofGeneral.eps): For texi documentation.  Used another,
+wider image with alpha channel to (attempt to) leave background white
+on printed page.  Post processing with gimp to add fuzzy border and
+white background since eps (gimp?) can't handle alpha channel.
+
+  Width 5.00 "
+  Height 7.87  (wrong, obviously: 3.48 is right by scaling)
+
+      But: this is *page* size!  The image size itself
+      was square, I think.   
+      Size of tiff image is 904x903.
 
-  Width 3.00 "
-  Height 7.87   (keep aspect ration checked, height not edited though)
   X-offset 2.8 "
   Y-offset 1.0 "
   Rotation: 0
+
+Actually, Y-offset seems to have no effect on page position: what
+happens is that tex compensates for the offset when it inserts the
+image!  Changing the offset and retexing puts the image back where TeX
+wants it.  Probably same true for X offset.
+
+Solving the size problem: original .eps is 8.4M.  (Original xcf file
+is missing/not saved).
+
+Test procedure: 
+
+ 1. render at 239dpi (original file seems to have 1200x1200 image in
+ it, this is closest I can get, makes 1199x1199 image).
+ 2. save as pnm (gives 4.1M file)
+ 3. Run pnmtoeps with -rle argument to get run length encoding. (4.1M)
+ 4. gzip -9  -> gives 1.6M file.
+
+Just using gzip directly gives 1.6M file anyway.
+tiff is 1.5M.  png is 1.2M.  bz2 is 1.3M.
+
+Okay, so we'll distribute the original .eps file, gzipped.  
+(It gets zipped inside the tar file anyway, of course, but
+leaving it zipped is less polluting).
+
+Badges
+======
+
+These were cut out from a close-up view of Proof General's chest.
diff --git a/images/pg-text.8bit.gif b/images/pg-text.8bit.gif
new file mode 100644
index 00000000..faf44286
--- /dev/null
+++ b/images/pg-text.8bit.gif
diff --git a/images/pg-text.gif b/images/pg-text.gif
new file mode 100644
index 00000000..046fe760
--- /dev/null
+++ b/images/pg-text.gif
diff --git a/images/pg-text.jpg b/images/pg-text.jpg
new file mode 100644
index 00000000..e2f1d5e3
--- /dev/null
+++ b/images/pg-text.jpg
diff --git a/images/pg-text.xcf b/images/pg-text.xcf
new file mode 100644
index 00000000..5f823f65
--- /dev/null
+++ b/images/pg-text.xcf