From 0164d341b4b5c5c55f39abde040aa4c591cfcf90 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 11 Dec 2003 17:01:20 +0000 Subject: Fix domain name --- BUGS | 4 ++-- INSTALL | 4 ++-- Makefile.devel | 12 ++++++------ README | 16 ++++++++-------- REGISTER | 4 ++-- doc/PG-adapting.texi | 22 +++++++++++----------- doc/ProofGeneral.texi | 36 ++++++++++++++++++------------------ doc/README.doc | 2 +- generic/proof-config.el | 2 +- generic/proof-indent.el | 3 ++- generic/proof-splash.el | 2 +- generic/proof-utils.el | 2 +- 12 files changed, 55 insertions(+), 54 deletions(-) diff --git a/BUGS b/BUGS index 60c9e877..e3838253 100644 --- a/BUGS +++ b/BUGS @@ -17,8 +17,8 @@ temporary workaround. * Known Bugs and Workarounds for Proof General. -Contact: mailto:bugs@proofgeneral.org -See also: http://www.proofgeneral.org/ProofGeneral/BUGS +Contact: mailto:da+pg-bugs@inf.ed.ac.uk +See also: http://proofgeneral.inf.ed.ac.uk/ProofGeneral/BUGS Generic bugs are listed here, which may affect all of the supported provers. See lego/BUGS coq/BUGS, etc, for specific bug lists for each diff --git a/INSTALL b/INSTALL index c36e664c..30d07bbe 100644 --- a/INSTALL +++ b/INSTALL @@ -28,13 +28,13 @@ notes below, the README file for each prover, and the file BUGS. If none of these files help, then contact us via the address below. - Proof General maintainer + Proof General maintainer LFCS, Division Of Informatics, University of Edinburgh. Edinburgh. - http://www.proofgeneral.org + http://proofgeneral.inf.ed.ac.uk diff --git a/Makefile.devel b/Makefile.devel index f1499679..a235d310 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -66,17 +66,17 @@ # NB: must use TAB as separator in list below. DEVELOPERS=\ --u "da David Aspinall da@proofgeneral.org" \ +-u "da David Aspinall da+pg-da@inf.ed.ac.uk" \ -u "gkein Gerwin Klein gklein@in.tum.de" \ -u "sberghof Stefan Berghofer berghofe@in.tum.de" \ --u "markus Markus Wenzel support+wenzelm@proofgeneral.org" \ +-u "markus Markus Wenzel da+pg-wenzelm@inf.ed.ac.uk" \ -u "pier Pierre Courtieu courtieu@lri.fr" \ -u "crr Christophe Raffalli Christophe.Raffalli@univ-savoie.fr" \ -u "pxc Paul Callaghan P.C.Callaghan@durham.ac.uk" \ --u "patrl Patrick Loiseleur support+patrl@proofgeneral.org" \ --u "tms Thomas Kleymann support+tms@proofgeneral.org" \ --u "djs Dilip Sequiera support+djs@proofgeneral.org" \ --u "hhg Healfdene Goguen support+hhg@proofgeneral.org" +-u "patrl Patrick Loiseleur da+pg-patrl@inf.ed.ac.uk" \ +-u "tms Thomas Kleymann da+pg-tms@inf.ed.ac.uk" \ +-u "djs Dilip Sequiera da+pg-djs@inf.ed.ac.uk" \ +-u "hhg Healfdene Goguen da+pg-hhg@inf.ed.ac.uk" # PRERELEASE_PREFIX is used to match PRERELEASE_TAG in sed diff --git a/README b/README index 244340da..c67e0185 100644 --- a/README +++ b/README @@ -1,5 +1,5 @@ -Proof General --- Organize your proofs! [www.proofgeneral.org] -================================================================= +Proof General --- Organize your proofs! [proofgeneral.inf.ed.ac.uk] +==================================================================== Proof General is a generic Emacs interface for proof assistants. @@ -14,16 +14,16 @@ toolbar and menus, which make use easier for all. 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 feedback@proofgeneral.org +Send ideas, comments, patches, code to da+pg-feedback@inf.ed.ac.uk See INSTALL for installation details. COPYING for license details. REGISTER for registration information (please register). FAQ, doc/ for documentation of Proof General. -See http://www.proofgeneral.org/mailinglist for the Proof General +See http://proofgeneral.inf.ed.ac.uk/mailinglist for the Proof General mailing lists. If you have problems, please contact -support@proofgeneral.org after checking the BUGS and CHANGES files. +da+pg-support@inf.ed.ac.uk after checking the BUGS and CHANGES files. For notes on the supported assistants, see the README files in the subdirectories: @@ -44,12 +44,12 @@ in the subdirectories: Check BUGS files for problems and issues, in this directory, and for specific issues, in each prover subdirectory. Please report bugs -not mentioned in any of these files to bugs@proofgeneral.org +not mentioned in any of these files to da+pg-bugs@inf.ed.ac.uk For the latest news and downloads, visit Proof General on the web -at: http://www.proofgeneral.org +at: http://proofgeneral.inf.ed.ac.uk -David Aspinall +David Aspinall March 2003. ----- diff --git a/REGISTER b/REGISTER index 8bcfbbf0..820c9517 100644 --- a/REGISTER +++ b/REGISTER @@ -1,6 +1,6 @@ Please register your use of Proof General on the web at: - http://www.proofgeneral.org/register + http://proofgeneral.inf.ed.ac.uk/register The information provided will only be used to help a case for support for Proof General in the future. @@ -9,4 +9,4 @@ There is also an opportunity to join the mailing list from this page. To add or remove yourself from the mailing list after registering, go to: - http://www.proofgeneral.org/mailinglist + http://proofgeneral.inf.ed.ac.uk/mailinglist diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index bb2527e6..19c579e1 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -17,7 +17,7 @@ @paragraphindent 0 @c A flag for whether to include the front image in the @c DVI file. You can download the front image from -@c http://www.proofgeneral.org/ProofGeneralPortrait.eps.gz +@c http://proofgeneral.inf.ed.ac.uk/ProofGeneralPortrait.eps.gz @c then put it into this directory and 'make dvi' (pdf,ps) @c will set the flag below automatically. @clear haveeps @@ -31,10 +31,10 @@ @c so removed for now. @set URLxsymbol http://x-symbol.sourceforge.net/ @set URLisamode http://zermelo.dcs.ed.ac.uk/~isamode -@set URLpghome http://www.proofgeneral.org -@set URLpglatestrpm http://www.proofgeneral.org/ProofGeneral-latest.noarch.rpm -@set URLpglatesttar http://www.proofgeneral.org/ProofGeneral-latest.tar.gz -@set URLpglatestdev http://www.proofgeneral.org/ProofGeneral-devel-latest.tar.gz +@set URLpghome http://proofgeneral.inf.ed.ac.uk +@set URLpglatestrpm http://proofgeneral.inf.ed.ac.uk/ProofGeneral-latest.noarch.rpm +@set URLpglatesttar http://proofgeneral.inf.ed.ac.uk/ProofGeneral-latest.tar.gz +@set URLpglatestdev http://proofgeneral.inf.ed.ac.uk/ProofGeneral-devel-latest.tar.gz @c @c @@ -97,7 +97,7 @@ END-INFO-DIR-ENTRY @sp 1 @subtitle Adapting Proof General @value{version} to new provers @subtitle @value{last-update} -@subtitle @b{www.proofgeneral.org} +@subtitle @b{proofgeneral.inf.ed.ac.uk} @c nested ifs fail here completely, WHY? @iftex @@ -145,7 +145,7 @@ General Public License (GPL); please check the accompanying file @sp 1 -Visit Proof General on the web at @code{http://www.proofgeneral.org} +Visit Proof General on the web at @code{http://proofgeneral.inf.ed.ac.uk} Version control: @code{@value{rcsid}} @end titlepage @@ -222,7 +222,7 @@ development method: if you require changes in the generic support, please contact us (or make adjustments yourself and send them to us). Proof General has a home page at -@uref{http://www.proofgeneral.org}. Visit this page +@uref{http://proofgeneral.inf.ed.ac.uk}. Visit this page for the latest version of the manuals, other documentation, system downloads, etc. @@ -264,7 +264,7 @@ provers to communicate using PGIP. At the time of writing, these ideas are in early stages. For latest details, or to become involved, see -@uref{http://www.proofgeneral.org/kit, the Proof General Kit +@uref{http://proofgeneral.inf.ed.ac.uk/kit, the Proof General Kit webpage}. @@ -1939,7 +1939,7 @@ output format. The goals buffer settings allow configuration of Proof General for proof by pointing or similar features. -See the Proof General @uref{http://www.proofgeneral.org/doc, documentation web page} +See the Proof General @uref{http://proofgeneral.inf.ed.ac.uk/doc, documentation web page} for a link to the technical report ECS-LFCS-97-368 which hints at how to use these settings. @@ -2052,7 +2052,7 @@ Proof General name used internally and in menu titles. @defopt proof-general-home-page Web address for Proof General -The default value is @code{"http://www.proofgeneral.org"}. +The default value is @code{"http://proofgeneral.inf.ed.ac.uk"}. @end defopt @c TEXI DOCSTRING MAGIC: proof-universal-keys @defvar proof-universal-keys diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 6e6498e6..3395af5d 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -14,7 +14,7 @@ @paragraphindent 0 @c A flag for whether to include the front image in the @c DVI file. You can download the front image from -@c http://www.proofgeneral.org/ProofGeneralPortrait.eps.gz +@c http://proofgeneral.inf.ed.ac.uk/ProofGeneralPortrait.eps.gz @c then put it into this directory and 'make dvi' (pdf,ps) @c will set the flag below automatically. @clear haveeps @@ -27,11 +27,11 @@ @c FIXME: unfortunately, broken in buggy pdftexinfo. @c so removed for now. @set URLxsymbol http://x-symbol.sourceforge.net -@set URLisamode http://www.proofgeneral.org/~isamode -@set URLpghome http://www.proofgeneral.org -@set URLpglatestrpm http://www.proofgeneral.org/ProofGeneral-latest.noarch.rpm -@set URLpglatesttar http://www.proofgeneral.org/ProofGeneral-latest.tar.gz -@set URLpglatestdev http://www.proofgeneral.org/ProofGeneral-devel-latest.tar.gz +@set URLisamode http://proofgeneral.inf.ed.ac.uk/~isamode +@set URLpghome http://proofgeneral.inf.ed.ac.uk +@set URLpglatestrpm http://proofgeneral.inf.ed.ac.uk/ProofGeneral-latest.noarch.rpm +@set URLpglatesttar http://proofgeneral.inf.ed.ac.uk/ProofGeneral-latest.tar.gz +@set URLpglatestdev http://proofgeneral.inf.ed.ac.uk/ProofGeneral-devel-latest.tar.gz @c @c @@ -99,7 +99,7 @@ END-INFO-DIR-ENTRY @sp 1 @subtitle User Manual for Proof General @value{version} @subtitle @value{last-update} -@subtitle @b{www.proofgeneral.org} +@subtitle @b{proofgeneral.inf.ed.ac.uk} @c nested ifs fail here completely, WHY? @iftex @@ -146,7 +146,7 @@ General Public License (GPL); please check the accompanying file @sp 1 -Visit Proof General on the web at @code{http://www.proofgeneral.org} +Visit Proof General on the web at @code{http://proofgeneral.inf.ed.ac.uk} @sp 1 @@ -205,7 +205,7 @@ news about previous releases, and notes on the development of Proof General. Proof General has a home page at -@uref{http://www.proofgeneral.org}. +@uref{http://proofgeneral.inf.ed.ac.uk}. Visit this page for the latest version of this manual, other documentation, system downloads, etc. @@ -288,7 +288,7 @@ PGIP. There is a similarity however; the design of PGIP was based heavily on the Emacs Proof General framework. At the moment little work has been done: collaborations are eagerly -sought. For more details, see @uref{http://www.proofgeneral.org/kit, +sought. For more details, see @uref{http://proofgeneral.inf.ed.ac.uk/kit, the Proof General Kit webpage}. @@ -3386,7 +3386,7 @@ switch modes once Proof General has been started. The classic version of Isabelle Proof General includes a mode for editing theory files taken from David Aspinall's Isamode interface, see -@uref{http://www.proofgeneral.org/~isamode}. Detailed documentation for +@uref{http://proofgeneral.inf.ed.ac.uk/~isamode}. Detailed documentation for the theory file mode is included with @code{Isamode}, there are some notes on the special functions available and customization settings below. @@ -3829,7 +3829,7 @@ General and support and improve it. Please volunteer! @appendix Obtaining and Installing Proof General has its own -@uref{http://www.proofgeneral.org,home page} hosted at +@uref{http://proofgeneral.inf.ed.ac.uk,home page} hosted at Edinburgh. Visit this page for the latest news! @menu @@ -3846,17 +3846,17 @@ Edinburgh. Visit this page for the latest news! You can obtain Proof General from the URL @example -@uref{http://www.proofgeneral.org}. +@uref{http://proofgeneral.inf.ed.ac.uk}. @end example The distribution is available in three forms @itemize @bullet @item A source tarball, @* -@uref{http://www.proofgeneral.org/ProofGeneral-devel-latest.tar.gz} +@uref{http://proofgeneral.inf.ed.ac.uk/ProofGeneral-devel-latest.tar.gz} @item A Linux RPM package (for any architecture), @* -@uref{http://www.proofgeneral.org/ProofGeneral-latest.noarch.rpm} +@uref{http://proofgeneral.inf.ed.ac.uk/ProofGeneral-latest.noarch.rpm} @item A developer's tarball, @* -@uref{http://www.proofgeneral.org/ProofGeneral-devel-latest.tar.gz} +@uref{http://proofgeneral.inf.ed.ac.uk/ProofGeneral-devel-latest.tar.gz} @end itemize Both the source tarball and the RPM package include the generic elisp @@ -4019,7 +4019,7 @@ the @file{coq} directory in the Proof General home directory. This appendix has been removed. Please consult the file -@uref{http://www.proofgeneral.org/ProofGeneral/BUGS,@file{BUGS}} in the +@uref{http://proofgeneral.inf.ed.ac.uk/ProofGeneral/BUGS,@file{BUGS}} in the distribution for an up-to-date description of bugs and other issues. If you discover a problem which isn't mentioned in @file{BUGS}, please @@ -4078,7 +4078,7 @@ interact with the LEGO system. David Aspinall convinced Thomas Kleymann that programming in Emacs Lisp wasn't so difficult after all. In fact, Aspinall had already implemented an Emacs interface for Isabelle with bells and whistles, -called @uref{http://www.proofgeneral.org/~isamode,Isamode}. Soon +called @uref{http://homepages.inf.ed.ac.uk/da/Isamode,Isamode}. Soon after, the package @code{lego-mode} was born. Users were able to develop proof scripts in one buffer. Support was provided to automatically send parts of the script to the proof process. The last official version with diff --git a/doc/README.doc b/doc/README.doc index e350baea..374bd121 100644 --- a/doc/README.doc +++ b/doc/README.doc @@ -20,7 +20,7 @@ If you want a front image on the printed dvi/gs manuals, you need to have the ProofGeneral.eps file in this directory. You can download a compressed version from -http://www.proofgeneral.org/ProofGeneral/doc/ProofGeneral.eps.gz +http://proofgeneral.inf.ed.ac.uk/ProofGeneral/doc/ProofGeneral.eps.gz This file is not included with the distribution because it is rather large (1.6M). diff --git a/generic/proof-config.el b/generic/proof-config.el index 3fbc4680..2b827366 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -2499,7 +2499,7 @@ If this table is empty or needs adjusting, please make changes using :group 'proof-general-internals) (defcustom proof-general-home-page - "http://www.proofgeneral.org" + "http://proofgeneral.inf.ed.ac.uk" "*Web address for Proof General" :type 'string :group 'proof-general-internals) diff --git a/generic/proof-indent.el b/generic/proof-indent.el index 22ff742c..5f58fa1b 100644 --- a/generic/proof-indent.el +++ b/generic/proof-indent.el @@ -48,7 +48,8 @@ (defun proof-indent-goto-prev () ; Note: may change point, even in case of failure! "Goto to previous syntax element for script indentation, ignoring string/comment contexts." (and - (proof-re-search-backward proof-indent-any-regexp nil t) + (proof-re-search-backward proof-indent-any-regexp + (proof-queue-or-locked-end) t) (or (not (proof-looking-at-syntactic-context)) (proof-indent-goto-prev)))) diff --git a/generic/proof-splash.el b/generic/proof-splash.el index 6c326968..ed64fdba 100644 --- a/generic/proof-splash.el +++ b/generic/proof-splash.el @@ -44,7 +44,7 @@ Proof General." "(C) LFCS, University of Edinburgh, 2003." nil nil -" Please send problems and suggestions to support@proofgeneral.org, +" Please send problems and suggestions to da+pg-support@inf.ed.ac.uk, or use the menu command Proof-General -> Submit bug report." nil (unless (or proof-running-on-XEmacs proof-running-on-Emacs21) diff --git a/generic/proof-utils.el b/generic/proof-utils.el index c7d9a1cb..61e3d040 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -688,7 +688,7 @@ or if the window is the only window of its frame." "[ When reporting a bug, please include a small test case for us to repeat it. Please also check that it is not already covered in the BUGS files that came with the distribution, or the latest versions at - http://www.proofgeneral.org/ProofGeneral/BUGS ]"))) + http://proofgeneral.inf.ed.ac.uk/ProofGeneral/BUGS ]"))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -- cgit v1.2.3