Updates for new web pages, todo list.

6 files changed, 45 insertions, 41 deletions

diff --git a/AUTHORS b/AUTHORS
index 6a30ec35..3816baf0 100644
--- a/AUTHORS
+++ b/AUTHORS
@@ -1,21 +1,18 @@
--*- outline -*-
+Current Authors/Maintainers:
 
-*  Current Authors/Maintainers
-** David Aspinall    <da@dcs.ed.ac.uk>	               
+ David Aspinall <da@dcs.ed.ac.uk>	
    doc, etc, generic, html, images, isa
-** Patrick Loiseleur <Patrick.Loiseleur@lri.fr>    
+ Patrick Loiseleur <Patrick.Loiseleur@lri.fr>    
    coq
-** Markus Wenzel <wenzelm@informatik.tu-muenchen.de>
+ Markus Wenzel <wenzelm@informatik.tu-muenchen.de>
    isar
-** Paul Callaghan <P.C.Callaghan@durham.ac.uk>
-   plastic
+ Paul Callaghan <P.C.Callaghan@durham.ac.uk>
+   plastic, lego
 
-*  Previous Authors:
-** Thomas Kleymann   
-   lego, doc, generic
-** Healfdene Goguen  
-   coq, generic, doc
-** Dilip Sequeira    
-   lego
+Previous Authors:
+
+  Thomas Kleymann   (lego, doc, generic)
+  Healfdene Goguen  (coq, generic, doc)
+  Dilip Sequeira    (lego)
 
 
diff --git a/CHANGES b/CHANGES
index 242f7a3f..4fb76c9c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -23,6 +23,8 @@ Summary of Changes for Proof General 2.1
 * Improvements to Coq mode: better recognition of
   Coq syntax, support for proof-shell-restart-cmd.
 
+* Toolbar can now be switched on and off via menu.
+
 * Bug fix for templates in Isabelle theory file mode.
 
 * Bug fix for long-lines with funny characters causing
diff --git a/COPYING b/COPYING
index cd626661..313f9451 100644
--- a/COPYING
+++ b/COPYING
@@ -1,4 +1,4 @@
-Proof General is Copyright (C) 1998 LFCS.
+Proof General is Copyright (C) 1998,1999 LFCS.
 
 You are allowed to freely copy and modify this software
 for non-commercial use, providing you observe these 
diff --git a/Makefile.devel b/Makefile.devel
index 1f283a54..62bab01f 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -50,10 +50,12 @@
 
 
 # Release tag.  For pre-releases.  Watch out with
-# substitution in tag target below, which edits
-# html/download.html
+# substitution in tag target below, which edits $(DOWNLOADHTML)
 PRERELEASE_TAG=2.1pre$(shell date "+%y%m%d")
 
+# html/download.phtml
+DOWNLOADHTML=download.phtml
+
 
 # This is used for full releases to control the tag name
 # and distribution name.  No editing of html is done
@@ -95,7 +97,7 @@ TAR=tar
 DEVELMAKE=make -f Makefile.devel
 
 # Files not to include the distribution area or tarball 
-NONDISTFILES=.cvsignore */.cvsignore html etc Makefile.devel doc/notes.txt images/*.xcf images/notes.txt images/gimp images/Makefile isa/wip.ML plastic/ isar/
+NONDISTFILES=.cvsignore */.cvsignore html etc Makefile.devel doc/notes.txt images/*.xcf images/notes.txt images/gimp images/Makefile isa/wip.ML html/notes.txt plastic/ isar/ 
 
 # Files not to include in the distribution tarball
 IGNOREDFILES=doc/ProofGeneral.dvi Makefile.devel todo isa/wip.ML
@@ -218,7 +220,7 @@ images:	FORCE
 ##
 ## tag:    tag the CVS sources of working directory with CVS_RELEASENAME,
 ##	   set version stamp in proof-site.el and ProofGeneral.spec 
-##         to VERSION, and edit download.html if VERSION matches 
+##         to VERSION, and edit $(DOWNLOADHTML) if VERSION matches 
 ##	   PRERELEASE_TAG.
 ##
 tag:		
@@ -227,18 +229,18 @@ tag:
 	@echo "*************************************************"
 	if [ -n "`cvs -n -q update`" ]; then exit 1; fi
 # Tag proof-site.el and ProofGeneral.spec
-	(cd generic; mv proof-site.el proof-site.el.old; sed -e 's/defconst proof-version \".*\"/defconst proof-version \"Proof General, Version $(VERSION) released by da,tms. Email proofgen@dcs.ed.ac.uk.\"/g' proof-site.el.old > proof-site.el; rm proof-site.el.old)
+	(cd generic; mv proof-site.el proof-site.el.old; sed -e 's/defconst proof-version \".*\"/defconst proof-version \"Proof General, Version $(VERSION) released by da. Email proofgen@dcs.ed.ac.uk.\"/g' proof-site.el.old > proof-site.el; rm proof-site.el.old)
 	(cd etc; mv ProofGeneral.spec ProofGeneral.spec.old; sed -e 's/Version:.*$$/Version:	$(VERSION)/g' ProofGeneral.spec.old > ProofGeneral.spec; rm ProofGeneral.spec.old)
-# Edit download.html only for prereleases.
+# Edit $(DOWNLOADHTML) only for prereleases.
 # Careful: the sed command below relies on previous value of PRERELEASE_TAG.
 	if [ $(PRERELEASE_TAG) = $(VERSION) ]; then \
-	  (cd html; mv download.html download.html.old; sed -e 's|ProofGeneral-2\.1pre......|ProofGeneral-$(PRERELEASE_TAG)|g' download.html.old > download.html; rm download.html.old) \
+	  (cd html; mv $(DOWNLOADHTML) $(DOWNLOADHTML).old; sed -e 's|ProofGeneral-2\.1pre......|ProofGeneral-$(PRERELEASE_TAG)|g' $(DOWNLOADHTML).old > $(DOWNLOADHTML); rm $(DOWNLOADHTML).old) \
 	fi
 # This hack to SOURCE: name is only needed because we have an obsolete version
 # of rpm installed on standard machines at dcs.ed, and we have to build with
 # that version.  Otherwise we could use the %{version} macro in the spec file.
 	(cd etc; mv ProofGeneral.spec ProofGeneral.spec.old; sed -e 's/ProofGeneral-.*.tar.gz/$(RELEASENAMETARGZ)/g' ProofGeneral.spec.old > ProofGeneral.spec; rm ProofGeneral.spec.old)
-	cvs commit -m"Set version tag for new release." generic/proof-site.el html/download.html etc/ProofGeneral.spec
+	cvs commit -m"Set version tag for new release." generic/proof-site.el html/$(DOWNLOADHTML) etc/ProofGeneral.spec
 	cvs tag "$(CVS_RELEASENAME)"
 
 ############################################################
diff --git a/README b/README
index 9c528edc..67f64b39 100644
--- a/README
+++ b/README
@@ -10,15 +10,17 @@ Please help us with this aim!  Configure Proof General for your proof
 assistant, by adding features at the generic level wherever possible.
 Send ideas, comments, patches, code to proofgen@dcs.ed.ac.uk.
 
-
 See INSTALL for installation details.
 
 See COPYING for license details.
 
 See doc/ for documentation of Proof General.
 
+For the latest news and downloads, check the Proof General web page
+at: http://www.dcs.ed.ac.uk/home/proofgen
+
 
-David Aspinall & Thomas Kleymann
-November 1998.
+David Aspinall.
+July 1999.
 		
 
diff --git a/todo b/todo
index 91755348..55cfecd9 100644
--- a/todo
+++ b/todo
@@ -25,18 +25,6 @@ A Clarify licence situation for Proof General after question from
   currently [22 Jan 1999] being drafted by UNIVED.
   Will wait for this (at least) before releasing 2.1.
 
-B Add a "register" page for registering downloads.  Perhaps filling
-  will be mandatory for users in a non-academic environment.
-  Suggestion: send an email to proofgen@dcs.ed.ac.uk with POST
-  results. Template:
-    http://www.dcs.ed.ac.uk/home/da/Isamode/IsamodeSurvey.html
-  [2 hours]
-
-B Make a mailing list for Proof General users.
-  [2 hours for introductory messages, mentioning on web
-   pages, understanding Majordomo.  Maybe support will
-   make the list itself.]
-
 B Polish ProofGeneral.texi and publish LaTeX version as an LFCS
   Technical Report.  
 
@@ -63,6 +51,10 @@ A BUGS to investigate:
 A Fix INFO-DIR-ENTRY in doc/ProofGeneral.texi to put Proof General 
   info file into a good place.
 
+B CVS repository issues.
+  Where are obsolete 'fileattr' files generated from/maintained?
+  Should junk these (which appear to say that tms is watching everything).
+
 B QUESTION: why do we have proof-shell-proof-completed-regexp's
   perhaps objectionable behaviour of forcing the response buffer?
   Would it be safe just to set the proof-shell-proof-completed flag
@@ -332,6 +324,10 @@ D Display management is much better than it was, but perhaps
 D Fixup display of urgent messages in minibuffer: split at
   newlines so we don't get ^J's in FSF Emacs.
 
+D Make wellclean target remove images in html/images which are
+  generated from the image directory.  Consider putting all the
+  image sources in images/
+
 X Is it possible to let C-c C-c (SIGINT) issue additional process input?
   Poly/ML requires an 'f' at the interrupt handler's prompt to proceed, or
   rather, to fail gracefully.
@@ -548,12 +544,12 @@ X Sections and files are handled incorrectly.
 * Here are things to be done to Isabelle Mode
 =============================================
 
-A auto-adjust Pretty.setmargin when window is resized
-
 A Multiple files needs careful testing.  There are cases when
   retracting asks for files to be removed which were never loaded.
   This might be harmless, but might be better cleaned up.
 
+B auto-adjust Pretty.setmargin when window is resized
+
 C derive an isa-response-mode from proof-response-mode;
   see lego.el (10min) 
 
@@ -572,7 +568,8 @@ X Add ability to choose logic.  Maybe not necessary: can use default
   (ponder this)
 
 X Write perl scripts to generate TAGS file for ML and thy files.
-  (6h, I've completely forgotten perl), or better:
+  (6h, I've completely forgotten perl).  Does anyone
+  actually want this?
 
 X Manage multiple proofs (markers in possibly different buffers)
 	 
@@ -587,6 +584,7 @@ C `proof-zap-commas-region' does not work for Emacs 20.2 on
 
 C proof-shell-dont-show-annotations doesn't seem to work.
 
+
 * Bugs in other packages beyond our control
 ===========================================
 
@@ -597,6 +595,8 @@ contain lines with stuff that looks lisp-ish.  e.g. "(asd . ads)"
 * Stable version release checklist
 ==================================
 
+0. Make all files have same CVS branch with cvs commit -f 
+   (only seems to work locally, not via cvs server).
 1. Test multiple file test suite for LEGO, Isabelle.  Coq example.
 2. Check case with FSF Emacs
 3. Check case with compiled code, for XEmacs only.
@@ -607,6 +607,7 @@ contain lines with stuff that looks lisp-ish.  e.g. "(asd . ads)"
      cd doc; make magic
 6. Update Emacs versions in texi, html/ 
 7. Check web page references from other places.
+8. Validate web pages if they're changed much.