From 54f652a05b0c7995d4385f4139009f299b36bc45 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sat, 13 Jul 2002 16:29:53 +0000
Subject: Fix layout a bit

---
 html/screenshot.html | 47 +++++++++++++++++++++++++++--------------------
 1 file changed, 27 insertions(+), 20 deletions(-)

(limited to 'html')

diff --git a/html/screenshot.html b/html/screenshot.html
index 3cf0ccae..6cce9e3a 100644
--- a/html/screenshot.html
+++ b/html/screenshot.html
@@ -3,12 +3,9 @@ Here are some screenshots of Proof General 3.0 running with
 different theorem provers.  To see the full-size version
 of a picture, click on its thumbnail.
 </p>
-<p>
-<i>NB: Your browser needs PNG support to view these pictures.
-</i>
-</p>
 
-<!-- todo: php3 this, add space between rows! -->
+<!-- FIXME: update pictures.  Fix vertical centering of screenshots. -->
+
 <table width="80%">
 <tr>
 <td width="200">
@@ -17,7 +14,7 @@ of a picture, click on its thumbnail.
 </a>
 </td>
 <td>
-<p>
+<p><font size="-1">
 Building a simple proof in LEGO with proof-by-pointing.
 <br>
 The top half of the window displays the proof script. 
@@ -29,8 +26,10 @@ has a blue background.
 <br>
 Clicking on terms in the subgoals list generates
 commands which are added to the proof script.
-</p>
-</tr>
+</font></p>
+<br>
+</td></tr>
+
 <tr>
 <td width="200">
 <a href="images/pg-coq-screenshot.png">
@@ -38,7 +37,7 @@ commands which are added to the proof script.
 </a>
 </td>
 <td>
-<p>
+<p><font size="-1">
 Coq Proof General running in multiple frame mode,
 full screen shot (1024x768).
 <br>
@@ -49,8 +48,10 @@ indication that Coq is processing the
 induction step, because the background of
 the proof step is pink.  It will become
 blue when Coq finishes that step.
-</p>
-</tr>
+</font></p>
+</br>
+</td></tr>
+
 <tr>
 <td width="200">
 <a href="images/pg-isa-screenshot.png">
@@ -58,7 +59,7 @@ blue when Coq finishes that step.
 </a>
 </td>
 <td>
-<p>
+<p><font size="-1">
 Replaying a domain theory proof in Isabelle's HOLCF logic.
 <br>
 In Isabelle, theory files as well as ML files are coloured.
@@ -71,8 +72,10 @@ display as symbols using the
 <a href="http://x-symbol.sourceforge.net/">X-Symbol</a>
 package in conjunction with Proof General.  
 Here you can see some symbols in Isabelle's output.
-</p>
-</tr>
+</font></p>
+</br>
+</td></tr>
+
 <tr>
 <td width="200">
 <a href="images/pg-isar-screenshot.png">
@@ -80,11 +83,13 @@ Here you can see some symbols in Isabelle's output.
 </a>
 </td>
 <td>
-<p>
-Replaying a proof in Isar, Isabelle's new proof language
+<p><font size="-1">
+Replaying a proof in Isar, Isabelle's declarative proof language
 developed by Markus Wenzel.
-</p>
-</tr>
+</font></p>
+<br>
+</td></tr>
+
 <tr>
 <td width="200">
 <a href="images/pg-lego-console.png">
@@ -92,13 +97,15 @@ developed by Markus Wenzel.
 </a>
 </td>
 <td>
-<p>
+<p><font size="-1">
 LEGO Proof General running in plain console mode.
 <br>
 This shows that you can run Proof General even if sometimes
 you need to use a plain tty or xterminal.   Of course, the
 graphical features are reduced!
-</p>
+</font></p>
+<br>
+</td>
 </tr>
 </table>
 
-- 
cgit v1.2.3