From 0343b2b7187a599d2373e92e00d5e8ad7da91c3f Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 29 Sep 2000 17:47:34 +0000 Subject: Remove messy link_root links. --- html/about.html | 4 ++-- html/develdownload.html | 6 +++--- html/doc.html | 3 +-- html/download.html | 6 +++--- html/features.html | 2 +- html/header.html | 6 ++++-- html/main.html | 37 ++++++++++++++++++++++++++----------- html/mission.html | 6 +++--- html/oldnews.html | 4 ++-- html/projects.html | 2 +- html/register.html | 4 ++-- 11 files changed, 48 insertions(+), 32 deletions(-) (limited to 'html') diff --git a/html/about.html b/html/about.html index ab04202e..7cc7e8af 100644 --- a/html/about.html +++ b/html/about.html @@ -9,8 +9,8 @@ proof-by-pointing and script management were added to LEGO mode, and the code was made generic. The generic basis was developed by Thomas Kleymann, Dilip Sequeira, Healfdene Goguen and David Aspinall. The current authors and maintainers of the various instantiations of -Proof General are mentioned on the +Proof General are mentioned on the +front page..

The Proof General project was coordinated until October 1998 by diff --git a/html/develdownload.html b/html/develdownload.html index c8a3050e..64952d62 100644 --- a/html/develdownload.html +++ b/html/develdownload.html @@ -26,7 +26,7 @@ Please register if you haven't done so already.

The manual included with the pre-release may be updated from that of the -. +last stable release.

You can see the current documentation: the user manual in @@ -81,7 +81,7 @@ notes about work-in-progress.

For install instructions, see -the . +the stable version download.

@@ -110,7 +110,7 @@ The complete archive also includes:

- diff --git a/html/download.html b/html/download.html index 03948ac0..48934d13 100644 --- a/html/download.html +++ b/html/download.html @@ -61,7 +61,7 @@ One or more of the supported proof assistants. Or write your own support for a new assistant.
See the - for links to supported +front page for links to supported assistants. @@ -80,7 +80,7 @@ for installation notes. - + @@ -129,7 +129,7 @@ and documentation (in Info and HTML formats).

Documentation is available in other formats -here . +here here. If you want to format the documentation yourself, you may like to download the

For (even) more details of the above features, see the - +documentation page.

diff --git a/html/header.html b/html/header.html index 9b7d70d3..cb5b3aba 100644 --- a/html/header.html +++ b/html/header.html @@ -18,7 +18,9 @@ * and fix $WANTED. Hrefs are given by page parameter to current doc. */ $separator='.'; - $WANTED=$HTTP_GET_VARS["page"]; + $urlbits = parse_url($REQUEST_URI); + $file = ereg_replace("^(.*/)+","",$urlbits["path"]); + $WANTED = ereg_replace(".html","",$file); print "\n"; $links_arr = array( "Home" => "main", @@ -47,7 +49,7 @@ print "" . $name . ""; } else { - link_root($links_arr[$name],$name); + print "$name"; } print " \n"; if ($name=="Download" || $name=="Documentation") print "\n"; diff --git a/html/main.html b/html/main.html index 614c194a..df52edb2 100644 --- a/html/main.html +++ b/html/main.html @@ -17,16 +17,19 @@ You need a recent version in either case. The aim of the Proof General project is to provide a powerful and configurable interfaces which help user-interaction with interactive proof assistants. The strategy of Proof General is to target power -users rather than novices, but we include general user interface -niceties, such as toolbar and menus, which make use easier for all. +users rather than novices, building an environment for proof +engineering. But we include general user interface niceties, such +as toolbar and menus, which make use easier for all. Proof General is +now used for organizing large proof developments, and for teaching +interactive proof.

To read more about what Proof General provides, -. +check the features list. To see what Proof General looks like in use, have a look at these screenshots. To download Proof General, visit the -. +download page. To contact the developers, click .

@@ -35,8 +38,7 @@ To contact the developers, click

What systems does Proof General work with?

-Proof General comes ready-customized for several proof assistants, -including: +Proof General comes ready-customized for these proof assistants:

@@ -122,11 +124,24 @@ including:

-There is also a preliminary version of -, for -HOL98. -We are seeking a volunteer from the HOL community to support -and improve this (perhaps also supporting other HOL variants). +There are also preliminary instances of Proof General: +

+

+These instances of Proof General are functional, but only show a bare +fraction of the functionality possible. We are +seeking volunteers to support and improve each of these +(please send a note to + feedback@proofgen.org if you're interested).

Proof General is ready to be customized to new proof assistants. diff --git a/html/mission.html b/html/mission.html index deec79dc..a0203092 100644 --- a/html/mission.html +++ b/html/mission.html @@ -113,9 +113,9 @@ for each proof assistant by an experienced user/developer.

Amongst other features, Proof General currently includes - +script management and -, +proof-by-pointing both championed in Projet CROAP.
@@ -125,7 +125,7 @@ Proof General also advances the state-of-the-art. For example, we introduced proof-by-pointing in an free-form environment, and extended script management to handle -. +multiple files. diff --git a/html/oldnews.html b/html/oldnews.html index ab36d1a0..1ef78c93 100644 --- a/html/oldnews.html +++ b/html/oldnews.html @@ -52,7 +52,7 @@ see the
  • 23rd March 2000

    Proof General 3.1 is now available from the -. Enjoy! +download page. Enjoy!

  • 14th March 2000 @@ -94,7 +94,7 @@ current development release.
  • 15th February 2000

    There is now a new -. +page for developers. I plan to apply for funding to continue managing the evolution and development of Proof General, once my own job position is more secure. diff --git a/html/projects.html b/html/projects.html index a2f8cbd2..ef13c874 100644 --- a/html/projects.html +++ b/html/projects.html @@ -66,7 +66,7 @@ has a powerful source-level debugger, edebug.

    If you are interested in working on any of these projects, feel free to discuss with the project proposer or on the -. +developer's mailing list.

    diff --git a/html/register.html b/html/register.html index 888de909..5a0ccadb 100644 --- a/html/register.html +++ b/html/register.html @@ -33,7 +33,7 @@ provide a case for support for Proof General in the future.

    If you have already registered you do not need to fill in the form -again, so return to +again, so return to the download page.

    Registration Form

    @@ -100,7 +100,7 @@ again, so return to print "

    \n

    "; print "

    \nClick "; - link_root("download#prereq","here"); + print "here"; print " to return to the download page.

    \n"; click_to_go_back(); -- cgit v1.2.3