-
Easy installation!
+ +Easy installation
To use Proof General, simply unpack the sources with
@@ -201,16 +199,8 @@ Emacs. See the file in the distribution for more details. --Please send us -any problems, suggestions, or patches. -
- - --
-
Easy installation of X-Symbol!
+Easy installation of X-Symbol
Contrary to what you may expect from the documentation of
diff --git a/html/features.phtml b/html/features.phtml
index 89ad9fd1..c3bcfd89 100644
--- a/html/features.phtml
+++ b/html/features.phtml
@@ -6,43 +6,10 @@ It doesn't matter if you're an Emacs militant or a pacifist!
Proof General is designed to be useful for novices and expert users alike.
It will be useful to you if you use a proof assistant, and
-you'd like an interface with the following features:
-simplified interaction,
-script management,
-multiple file scripting,
-proof by pointing,
-toolbar and menus,
-syntax highlighting,
-real symbols,
-functions menu,
-tags,
-and finally,
-adaptability.
-
-Are you convinced yet?
-If not, read on…
+you'd like an interface with the following features...
-
-
-
-
- Proof General is designed for proof assistants which have a
- command-line shell interpreter. When using Proof General, the proof
- assistant's shell is hidden from the user. Communication takes
- place via three buffers (Emacs text widgets). The script
- buffer holds input, the commands to construct a proof. The
- goals buffer displays the current list of subgoals to be
- solved. The response buffer displays other output from the
- proof assistant. By default, only two of these three buffers are
- displayed at once. This means that the user only sees the output
- from the most recent interaction, rather than a screen full of
- output from the proof assistant.
-
- Despite this more friendly communication model, Proof General does not - commandeer the proof assistant shell: the user still has complete - access to it if necessary. -
-
-
+
- A proof script is a sequence of commands sent to a proof assistant to construct a proof, usually stored in @@ -64,7 +31,26 @@ If not, read on… of Proof General to see script managament in action. - + +
-
+ Proof General is designed for proof assistants which have a
+ command-line shell interpreter. When using Proof General, the proof
+ assistant's shell is hidden from the user. Communication takes
+ place via three buffers (Emacs text widgets). The script
+ buffer holds input, the commands to construct a proof. The
+ goals buffer displays the current list of subgoals to be
+ solved. The response buffer displays other output from the
+ proof assistant. By default, only two of these three buffers are
+ displayed at once. This means that the user only sees the output
+ from the most recent interaction, rather than a screen full of
+ output from the proof assistant.
+
+ Despite this more friendly communication model, Proof General does not + commandeer the proof assistant shell: the user still has complete + access to it if necessary. +
+
+
- Script management in Proof General can work across many script files, integrating with the file handling of @@ -78,7 +64,7 @@ If not, read on… Proof General (based on the order in which files were processed). - +
- Proof by pointing allows you to click on a subterm of a goal to be proved, and apply an appropriate rule or @@ -89,9 +75,10 @@ If not, read on… Proof General also uses the subterm structure to make it easy to cut and paste from complicated terms. - + - +
- Proof General has a toolbar with buttons for examining the proof state, starting a proof, manoeuvring in the proof script, @@ -107,7 +94,7 @@ If not, read on… - +
- Syntax highlighting is an editing feature which decorates a file with different colours or fonts according to the syntax of some @@ -118,7 +105,7 @@ If not, read on… assumptions, for example. - +
-
Proof General has a close integration with the
powerful
@@ -135,7 +122,7 @@ If not, read on…
- A pull-down menu gives easy navigations to theorems, definitions, and declarations @@ -151,7 +138,7 @@ If not, read on… remotely, while your files and editor reside on your local machine. - +
- Tags are an editing feature which allow you to quickly locate the definition or declaration of a particular identifier. Proof General @@ -162,7 +149,7 @@ If not, read on… - +
-
Proof General is designed to be adaptable. Many aspects
of its behaviour can be easily customized (using dialogue boxes and
diff --git a/html/functions.php3 b/html/functions.php3
index 715fbafc..0422dc37 100644
--- a/html/functions.php3
+++ b/html/functions.php3
@@ -113,7 +113,6 @@ function date_modified($filename) {
}
/* Nav bar separator */
-
$separator = '
';
/* A link to one of the main pages (must appear in navbar menu) */
diff --git a/html/gallery.phtml b/html/gallery.phtml
index 45bbb11e..e433da8a 100644
--- a/html/gallery.phtml
+++ b/html/gallery.phtml
@@ -9,7 +9,7 @@ Here are some publicity pictures for Proof General. They were created
by David Aspinall in his spare time, using the excellent freeware
programs GIMP and Blender. The General himself is
-based on a commercial mesh by
+based on a commercial mesh given away by
Viewpoint.
diff --git a/html/header.phtml b/html/header.phtml index 3cdc722c..207c366d 100644 --- a/html/header.phtml +++ b/html/header.phtml @@ -1,10 +1,10 @@ -
+
-- cgit v1.2.3- + 
+ width=158 height=183 border=0 >
@@ -17,7 +17,9 @@ * Look for $WANTED in array. If not found, use default of "Home" * and fix $WANTED. Hrefs are given by page parameter to current doc. */ + $separator=' ';
$WANTED=$HTTP_GET_VARS["page"];
+ print "
\n"; ?>\n"; $links_arr = array( "Home" => "main", "News" => "news", @@ -28,6 +30,7 @@ "About" => "about", "Links" => "links" ); + $midpoint = "Download"; $DEFAULT = $links_arr["Home"]; $wanted_okay = 0; for (reset($links_arr); $name = key($links_arr); next($links_arr)) { @@ -41,13 +44,15 @@ for (reset($links_arr); $name = key($links_arr); next($links_arr)) { print $separator; if ($WANTED == $links_arr[$name]) { - print "" . $name . ""; + print "" . $name . ""; } else { link_root($links_arr[$name],$name); } - print "
\n"; + print "\n"; + if ($name==$midpoint) print ""; } + print "