Fix domain name

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 <support@proofgeneral.org>
+   Proof General maintainer <da+pg-support@inf.ed.ac.uk>
    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 <da@proofgeneral.org>
+David Aspinall <da+pg@inf.ed.ac.uk>
 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 ]")))
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;