Tidy whitespace

11 files changed, 207 insertions, 208 deletions

diff --git a/lib/bufhist.el b/lib/bufhist.el
index 8864c425..a593de5f 100644
--- a/lib/bufhist.el
+++ b/lib/bufhist.el
@@ -6,14 +6,14 @@
 ;; License:    GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Keywords:   tools
 ;;
-;; $Id$ 
+;; $Id$
 ;;
 ;; This file is distributed under the terms of the GNU General Public
 ;; License, Version 2.  Find a copy of the GPL with your version of
 ;; GNU Emacs or Texinfo.
-;; 
+;;
 ;; This library implements a minor mode for which keeps a ring history of
-;; buffer contents.  Intended to be used for small buffers which are 
+;; buffer contents.  Intended to be used for small buffers which are
 ;; intermittently updated (e.g. status panels/displays), for which history
 ;; browsing is useful.
 ;;
@@ -23,7 +23,7 @@
 ;; copying strings in and out.  That way we can use cloned (indirect)
 ;; buffers which allow independent browsing of the history.
 ;;
-;; FIXMEs: autoloading this doesn't work too well.  
+;; FIXMEs: autoloading this doesn't work too well.
 ;;         advice on erase-buffer doesn't work
 ;;         duplicated first item in ring after clear (& on startup).
 
@@ -71,7 +71,7 @@
 	   (desc      (format "History %d of %d; mouse-1 previous; mouse-3 next"
 			      histpos histsize))
 	   (indicator (format "[%d/%d]" histpos histsize)))
-      (propertize 
+      (propertize
        indicator
        'help-echo desc
        'keymap (eval-when-compile
@@ -84,11 +84,11 @@
 		   ;; (define-key map [mode-line control mouse-3] 'bufhist-last)
 		   map))
        'mouse-face 'mode-line-highlight))))
-     
+
 ;simple:
-;  '(" [hist:" 
+;  '(" [hist:"
 ;    (:eval (int-to-string (- (ring-length bufhist-)
-;			     bufhist-ring-pos))) "/" 
+;			     bufhist-ring-pos))) "/"
 ;    (:eval (int-to-string (ring-length bufhist-ring))) "]"))
 
 (make-variable-buffer-local 'bufhist-ring)
@@ -100,7 +100,7 @@
   "Return the stored representation of the current buffer contents."
   ;; First: make all extents in the buffer duplicable to recreate them
   (if (fboundp 'mapcar-extents)
-      (mapcar-extents (lambda (ext) 
+      (mapcar-extents (lambda (ext)
 			(set-extent-property ext 'duplicable t))))
   (cons (point)
 	(buffer-substring (point-max) (point-min))))
@@ -126,7 +126,7 @@
 ;; We could provide advice for erase-buffer, but instead make this part of API.
 (defun bufhist-erase-buffer ()
   "Erase buffer contents, maybe running bufhist-before-change-function first."
-  (if (and 
+  (if (and
        bufhist-mode
        (memq 'bufhist-before-change-function before-change-functions))
       (let ((before-change-functions nil)
@@ -143,7 +143,7 @@
 (defun bufhist-switch-to-index (n &optional nosave browsing)
   "Switch to position N in buffer history, maybe updating history.
 If optional NOSAVE is non-nil, do not try to save current contents."
-  (unless (equal n bufhist-ring-pos) 
+  (unless (equal n bufhist-ring-pos)
     ;; we're moving to different position
     (let ((tick (buffer-modified-tick)))
       ;; Save changes back to history for most recent contents or for
@@ -153,7 +153,7 @@ If optional NOSAVE is non-nil, do not try to save current contents."
 		  (equal tick bufhist-lastswitch-modified-tick))
 	;; If we're browsing away from position 0, checkpoint instead
 	;; of updating.
-	;; NB: logic here should ideally keep flag to say whether 
+	;; NB: logic here should ideally keep flag to say whether
 	;; changes are "during" a browse or not.  This is going
 	;; to result in too many checkpoints if we have manual
 	;; editing.
@@ -162,19 +162,19 @@ If optional NOSAVE is non-nil, do not try to save current contents."
 	    (bufhist-checkpoint)
 	  ; (setq n (1+ n)))
 	  ;; Otherwise update in-position
-	  (bufhist-ring-update bufhist-ring bufhist-ring-pos 
+	  (bufhist-ring-update bufhist-ring bufhist-ring-pos
 			       (bufhist-get-buffer-contents))))
       (setq bufhist-lastswitch-modified-tick tick)
       (let ((before-change-functions nil)
 	    (buffer-read-only nil))
 	(bufhist-restore-buffer-contents (ring-ref bufhist-ring n)))
       (if bufhist-read-only-history
-	  (setq buffer-read-only 
+	  (setq buffer-read-only
 		(if (eq n 0) bufhist-normal-read-only t)))
       (setq bufhist-ring-pos n)
       (force-mode-line-update)
       (if browsing
-	  (message "History position %d of %d in %s" 
+	  (message "History position %d of %d in %s"
 		   (- (ring-length bufhist-ring) n)
 		   (ring-length bufhist-ring)
 		   (buffer-name))))))
@@ -188,7 +188,7 @@ If optional NOSAVE is non-nil, do not try to save current contents."
   "Switch to last (most recent; current) buffer contents."
   (interactive)
   (bufhist-switch-to-index 0 nil 'browsing))
-  
+
 (defun bufhist-prev (&optional n)
   "Browse backward in the history of buffer contents."
   (interactive "p")
@@ -212,13 +212,13 @@ If optional NOSAVE is non-nil, do not try to save current contents."
 
 ;; FIXME: glitch here: we get duplicated first item after clear.
 ;; Bit like on startup: we always get empty buffer/current contents
-;; twice.  Reason is because of invariant of non-empty ring; 
-;; when we checkpoint we always add to ring. 
+;; twice.  Reason is because of invariant of non-empty ring;
+;; when we checkpoint we always add to ring.
 (defun bufhist-clear ()
   "Clear history."
   (interactive)
   (message "Buffer history in %s cleared." (buffer-name))
-  (bufhist-switch-to-index 0 'nosave) 
+  (bufhist-switch-to-index 0 'nosave)
   (setq bufhist-ring (make-ring (ring-size bufhist-ring)))
   (setq bufhist-ring-pos 0)
   (bufhist-checkpoint)
@@ -241,12 +241,12 @@ The size defaults to `bufhist-ring-size'."
   (setq bufhist-ring-pos 0)
   (setq bufhist-saved-mode-line-format mode-line-format)
   (bufhist-checkpoint)
-  (setq mode-line-format 
-	(cons '(bufhist-mode 
+  (setq mode-line-format
+	(cons '(bufhist-mode
 		(:eval (bufhist-mode-line-format-entry)))
 	      ;; surely it's always a list, but in case not
-	      (if (listp mode-line-format) 
-		  mode-line-format 
+	      (if (listp mode-line-format)
+		  mode-line-format
 		(list mode-line-format))))
   (force-mode-line-update)
   (make-local-variable 'before-change-functions)
@@ -289,21 +289,21 @@ The size defaults to `bufhist-ring-size'."
 ;	    (bufhist-last)))
 ;      (ad-activate-on 'erase-buffer)))
 
-;;; Buttons 
+;;; Buttons
 
 (defun bufhist-make-buttons ()
   (widget-create 'push-button
-                :notify (lambda (&rest ignore) 
+		:notify (lambda (&rest ignore)
 			   (bufhist-prev))
-                 "Prev")
+		 "Prev")
   (widget-create 'push-button
-                :notify (lambda (&rest ignore) 
+		:notify (lambda (&rest ignore)
 			   (bufhist-next))
-                 "Next")
+		 "Next")
   (widget-setup))
 
 
-;;; Minor mode 
+;;; Minor mode
 
 (defconst bufhist-minor-mode-map
   (let ((map (make-sparse-keymap)))
@@ -322,8 +322,8 @@ The size defaults to `bufhist-ring-size'."
   "Minor mode retaining an in-memory history of the buffer contents.
 
 Commands:\\<bufhist-minor-mode-map>
-\\[bufhist-prev]    bufhist-prev    go back in history  
-\\[bufhist-next]    bufhist-next    go forward in history  
+\\[bufhist-prev]    bufhist-prev    go back in history
+\\[bufhist-next]    bufhist-next    go forward in history
 \\[bufhist-first]   bufhist-first   go to first item in history
 \\[bufhist-last]    bufhist-last    go to last (current) item in history.
 \\[bufhist-clear]   bufhist-clear   clear history.
@@ -333,13 +333,13 @@ Commands:\\<bufhist-minor-mode-map>
 ; For newer versions of define-minor-mode we can use extra
 ; args above instead of hook function below:
 ;  :group 'bufhist
-;  (if bufhist-mode 
+;  (if bufhist-mode
 ;      (bufhist-init)
 ;    (bufhist-exit)))
 ; This doesn't work, e.g. with XEmacs 21.4.15.
 
 (defun bufhist-toggle-fn ()
-  (if bufhist-mode 
+  (if bufhist-mode
       (bufhist-init)
     (bufhist-exit)))
 
diff --git a/lib/holes.el b/lib/holes.el
index 492502b0..0865cd4c 100644
--- a/lib/holes.el
+++ b/lib/holes.el
@@ -6,18 +6,18 @@
 ;;
 ;; This file uses spans, an interface for extent (XEmacs) and overlays
 ;; (emacs), by Healfdene Goguen for the proofgeneral mode.
-;; 
+;;
 ;; Credits also to Stefan Monnier for great help in making this file
 ;; cleaner.
-;; 
+;;
 ;; This software is free software; you can redistribute it and/or
 ;; modify it under the terms of the GNU General Public
 ;; License version 2, as published by the Free Software Foundation.
-;; 
+;;
 ;; This software is distributed in the hope that it will be useful,
 ;; but WITHOUT ANY WARRANTY; without even the implied warranty of
 ;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
-;; 
+;;
 ;; See the GNU General Public License version 2 for more details
 ;; (enclosed in the file GPL).
 ;;
@@ -28,7 +28,7 @@
 ;; See documentation in variable holes-doc.
 
 ;;; History:
-;; 
+;;
 
 (eval-when-compile (require 'span))
 (require 'cl)
@@ -41,7 +41,7 @@ It is useful to build complicated expressions by copy pasting several
 peaces of text from different parts of a buffer (or even from
 different buffers).
 
-                          HOLES
+			  HOLES
 
 A hole is a piece of (highlighted) text that may be replaced by
 another part of text later.  There is no information stored on the
@@ -49,7 +49,7 @@ file for holes, so you can save and modify files containing holes with
 no harm... You can even insert or delete characters inside holes like
 any other characters.
 
-                          USE
+			  USE
 
 At any time only one particular hole, called \"active\", can be
 \"filled\".  Holes can be in several buffers but there is always one or
@@ -112,9 +112,9 @@ COMBINING HOLES AND SKELETONS
 `holes' minor mode is made to work with minor mode `skeleton' minor
 mode. For the moment only Emacs version of `skeleton' is compatible
 with `holes', not XEmacs's. When you insert a skeleton, each
-interesting position will be replaced by a hole. 
+interesting position will be replaced by a hole.
 
-                          KNOWN BUGS
+			  KNOWN BUGS
 
  o Don't try to make overlapping holes, it doesn't work. (what would
 it mean anyway?)
@@ -126,7 +126,7 @@ holes highlighted as the active one (whereas only one of them really
 is), which is annoying.
 ")
 
- 
+
 ;;; Code:
 
 ;;; initialization
@@ -254,7 +254,7 @@ active hole doesn't exist (the marker is set to nothing)."
   "Return the position of the start of the active hole.
 See `active-hole-buffer' to get its buffer.  Returns an error if
 active hole doesn't exist (the marker is set to nothing)."
-  
+
   (assert (holes-active-hole-exist-p) t
 	  "holes-active-hole-end-position: no active hole")
   (holes-hole-end-position holes-active-hole)
@@ -273,10 +273,10 @@ active hole is empty."
   )
 
 (defun holes-goto-active-hole ()
-  
+
   "Set point to active hole.
 Raises an error if active-hole is not set."
-  
+
   (interactive)
   (assert (holes-active-hole-exist-p) t
 	  "holes-goto-active-hole: no active hole")
@@ -327,7 +327,7 @@ the active hole is already disable."
 
   "Set active hole to HOLE.
 Error if HOLE is not a hole."
-  
+
   (assert (holes-is-hole-p HOLE) t
 	  "holes-set-active-hole: %s is not a hole")
   (if (holes-active-hole-exist-p) (holes-highlight-hole holes-active-hole))
@@ -374,7 +374,7 @@ Error if HOLE is not a hole."
 If no arg default hole after point.  If only one arg: error.  Return
 the span."
   (interactive)
-  
+
   (let* ((rstart (or start (holes-region-beginning-or-nil) (point)))
 	 (rend (or end (holes-region-end-or-nil) (point))))
     (if (eq rstart rend)
@@ -394,7 +394,7 @@ the span."
   "Internal."
   (assert (holes-is-hole-p HOLE) t
 	  "holes-clear-hole: %s is not a hole")
-  
+
   (if (and (holes-active-hole-exist-p) (eq holes-active-hole HOLE))
       (holes-disable-active-hole)
     )
@@ -456,7 +456,7 @@ Default pos = point and buffer = current."
   (interactive)
   (let ((nxthole (holes-next (or pos (point))
 			     (or buffer (current-buffer)))))
-    (if nxthole 
+    (if nxthole
 	(holes-set-active-hole nxthole)
       (holes-disable-active-hole)
       )
@@ -588,12 +588,12 @@ Sets `holes-active-hole' to the next hole if it exists."
       ;; Emacs-21's mouse-drag-region has a bug that makes it behave more or
       ;; less like we want it as long as transient-mark-mode is active.
       (let ((transient-mark-mode nil))
-        (mouse-drag-region event)))
+	(mouse-drag-region event)))
     (defsubst holes-track-mouse-clicks ()
       "see `mouse-selection-click-count'"
       (+ mouse-selection-click-count 1)))
    (t
-    (unless noninteractive 
+    (unless noninteractive
       ;; da: ^^^^ avoid error in "make doc" (mouse functions undefined?)
       (error
      "Your (X)Emacs version is not compatible with holes (too old or
@@ -777,7 +777,7 @@ created.  Return the number of holes created."
 	    (holes-make-hole (match-beginning 0) (match-end 0))
 	  (holes-make-hole (match-beginning 1) (match-end 1))
 	  ;; delete end first to avoid shifting of marks
-	  (delete-region (match-end 1) (match-end 0)) 
+	  (delete-region (match-end 1) (match-end 0))
 	  (delete-region (match-beginning 0) (match-beginning 1)))
 	(holes-set-active-hole-next)))
     n))
@@ -791,7 +791,7 @@ created.  Return the number of holes created."
       (dolist (pos skeleton-positions)	;; put holes here
 	(holes-set-make-active-hole pos pos)))))
 
-(defconst holes-jump-doc 
+(defconst holes-jump-doc
   (concat "Hit \\[holes-set-point-next-hole-destroy] to jump "
 	  "to active hole.  C-h v holes-doc to see holes doc.")
   "Shortcut reminder string for jumping to active hole.")
diff --git a/lib/local-vars-list.el b/lib/local-vars-list.el
index c55cee44..0310f73f 100644
--- a/lib/local-vars-list.el
+++ b/lib/local-vars-list.el
@@ -9,11 +9,11 @@
 ;; This software is free software; you can redistribute it and/or
 ;; modify it under the terms of the GNU General Public
 ;; License version 2, as published by the Free Software Foundation.
-;; 
+;;
 ;; This software is distributed in the hope that it will be useful,
 ;; but WITHOUT ANY WARRANTY; without even the implied warranty of
 ;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
-;; 
+;;
 ;; See the GNU General Public License version 2 for more details
 ;; (enclosed in the file GPL).
 
@@ -21,7 +21,7 @@
 ;; See documentation in variable local-var-list-doc
 
 ;;; History:
-;; 
+;;
 
 ;;; Help:
 
@@ -30,7 +30,7 @@
 
 A file can contain a \"local variables list\", which specifies the values to use for
 certain Emacs variables when that file is edited. See info node \"(emacs)File
-Variables\". 
+Variables\".
 
 local-vars-list provides two useful functions:
 
@@ -47,17 +47,17 @@ Indents the zone according to mode after insertion."
   (save-excursion
     (goto-char (point-max))
     (let ((pt (point)))
-      (cond 
+      (cond
        ((not comment-start)
-	(insert 
+	(insert
 	 "
 *** Local Variables: ***
 *** End: ***
-" 
+"
 	 ))
 
        ((string-equal comment-end "")
-	(insert 
+	(insert
 	 (format
 	  "
 %s** Local Variables: ***
@@ -66,7 +66,7 @@ Indents the zone according to mode after insertion."
 	  comment-start comment-start)))
 
        (t
-	(insert 
+	(insert
 	 (format
 	  "
 %s
@@ -80,13 +80,13 @@ Indents the zone according to mode after insertion."
 
 
 (defun local-vars-list-find ()
-  "Find the local variable definition paragraph. 
+  "Find the local variable definition paragraph.
 Return a list containing the prefix and the suffix of its first line,
 or throw 'notfound if not found. Sets the point at the beginning of
 the second line of the paragraph."
   (goto-char (point-max))
   (catch 'notfound
-    (if (not (re-search-backward "Local Variables:" nil t)) (throw 'notfound nil))  
+    (if (not (re-search-backward "Local Variables:" nil t)) (throw 'notfound nil))
     (let ((bol (save-excursion (beginning-of-line) (point)))
 	  (eol (save-excursion (end-of-line) (point)))
 	  (lpattern)
@@ -94,17 +94,17 @@ the second line of the paragraph."
       (setq lpattern (buffer-substring bol (point)))
       (re-search-forward "Local Variables:" eol t)
       (setq rpattern (buffer-substring (point) eol))
-      (forward-line 1) 
+      (forward-line 1)
       (beginning-of-line)
       (cons lpattern (cons rpattern nil)))))
 
 (defun local-vars-list-goto-var (symb lpat rpat)
-  "Search a line defining local variable symb at current line and below. 
+  "Search a line defining local variable symb at current line and below.
 If successful set point to the beginning of the *value* and return t.
 Otherwise set point to the beginning of the last line of the local
 variables list (the one containing \"End:\"), and return nil.
 
-lpat and rpat are the suffix and prefix of the local variable list. 
+lpat and rpat are the suffix and prefix of the local variable list.
 
 Note: this function must be called when at the beginning of a local
 variable definition (or at the \"End:\" line)."
@@ -116,7 +116,7 @@ variable definition (or at the \"End:\" line)."
       (search-forward lpat eol)
       (re-search-forward "\\([^ :]+\\):" eol)
       (let ((varname (match-string 1)))
-	(cond 
+	(cond
 	 ((string-equal varname "End") (setq endreached t) (beginning-of-line))
 	 ((string-equal varname symbname) (setq found t))
 	 (t (forward-line 1) (beginning-of-line)))))
@@ -164,7 +164,7 @@ variable definition (or at the \"End:\" line)."
       (kill-region boexp (point))
       (insert (format " %S " val))
       )
-    )  
+    )
   )
 
 
@@ -172,7 +172,7 @@ variable definition (or at the \"End:\" line)."
   "Return the value written in the local variable list for variable symb.
 Raises an error if symb is not in the list."
   (save-excursion
-    (let* 
+    (let*
 	((lrpat (local-vars-list-find))
 	 (dummy (if lrpat t (error "local variables zone not found. ")))
 	 (lpat (car lrpat))
@@ -180,7 +180,7 @@ Raises an error if symb is not in the list."
 	 )
       (beginning-of-line)
       (if (local-vars-list-goto-var symb lpat rpat)
-	  t 
+	  t
 	(error "variable %s not found" symb))
       (beginning-of-line)
       (local-vars-list-get-current lpat rpat))))
@@ -220,6 +220,3 @@ of the buffer first."
 ;;; fill-column: 85 ***
 ;;; indent-tabs-mode: nil ***
 ;;; End: ***
-
-
-
diff --git a/lib/maths-menu.el b/lib/maths-menu.el
index 1a114c86..d02ff02e 100644
--- a/lib/maths-menu.el
+++ b/lib/maths-menu.el
@@ -58,7 +58,7 @@
 
 (defvar maths-menu-tokenise-insert '(lambda (char) (insert char))
   "Function used to insert possibly formatted or escaped character.")
-  
+
 (defun maths-menu-build-menu (spec)
   (let ((map (make-sparse-keymap "Characters")))
     (dolist (pane spec)
@@ -67,10 +67,10 @@
 	(define-key-after map (vector (intern name)) (cons name pane-map))
 	(dolist (elt pane)
 	  (let ((fname (intern
-			(concat "maths-menu-insert-" 
+			(concat "maths-menu-insert-"
 				(replace-regexp-in-string " " "-" (cadr elt))))))
-	    (fset fname 
-		  `(lambda () 
+	    (fset fname
+		  `(lambda ()
 		     (interactive)
 		     (funcall maths-menu-tokenise-insert ,(car elt))))
 	    (define-key-after pane-map
diff --git a/lib/pg-dev.el b/lib/pg-dev.el
index 6ac24bce..22aba6e5 100644
--- a/lib/pg-dev.el
+++ b/lib/pg-dev.el
@@ -7,20 +7,23 @@
 ;; $Id$
 ;;
 ;;; Commentary:
-;; 
+;;
 ;; Some configuration of Emacs Lisp mode for developing PG, not needed
 ;; for ordinary users.
 ;;
 
-;; Use checkdoc, eldoc, Flyspell:
-
 ;;; Code:
-(add-hook 'emacs-lisp-mode-hook
-	  '(lambda () (checkdoc-minor-mode 1)))
 
-(add-hook 'emacs-lisp-mode-hook 'turn-on-eldoc-mode)
+;; Use checkdoc, eldoc, Flyspell, whitespace cleanup:
 
-(add-hook 'emacs-lisp-mode-hook 'flyspell-prog-mode)
+(add-hook 'emacs-lisp-mode-hook
+	  '(lambda ()
+	     (checkdoc-minor-mode 1)
+	     (turn-on-eldoc-mode)
+	     (flyspell-prog-mode)
+	     (customize-set-variable 'whitespace-action '(cleanup))
+	     (add-hook 'write-file-functions
+		       'whitespace-write-file-hook nil t)))
 
 
 ;; Configure indentation for our macros
@@ -77,11 +80,11 @@
    '(proof-splash pg-assoc pg-xml proof-depends proof-indent proof-site
      proof-shell proof-menu pg-pbrpm pg-pgip proof-script
      proof-autoloads pg-response pg-goals proof-toolbar
-     proof-easy-config proof-config proof-mmm proof 
+     proof-easy-config proof-config proof-mmm proof
      proof-utils proof-syntax pg-user pg-custom
      proof-maths-menu proof-unicode-tokens
      pg-thymodes pg-autotest
-     ;; 
+     ;;
      isar-syntax isar-find-theorems isar-unicode-tokens
      isar-autotest interface-setup isabelle-system isar isar-mmm
      isar-keywords
@@ -89,7 +92,7 @@
      coq-abbrev coq-db coq-unicode-tokens coq-local-vars coq coq-syntax
      coq-indent coq-autotest)))
 
-     
+
 
 ;;
 ;; Proling interesting packages
@@ -112,9 +115,9 @@
 (defun pg-bug-references ()
   (interactive)
   (bug-reference-mode 1)
-  (setq bug-reference-bug-regexp 
+  (setq bug-reference-bug-regexp
 	"\\(?:[Tt]rac ?#\\)\\([0-9]+\\)"
-	bug-reference-url-format 
+	bug-reference-url-format
 	"http://proofgeneral.inf.ed.ac.uk/trac/ticket/%s"))
 
 (add-hook 'emacs-lisp-mode-hook 'pg-bug-references)
@@ -127,4 +130,3 @@
 (provide 'pg-dev)
 
 ;;; pg-dev.el ends here
-
diff --git a/lib/pg-fontsets.el b/lib/pg-fontsets.el
index 29fd38f8..cf170621 100644
--- a/lib/pg-fontsets.el
+++ b/lib/pg-fontsets.el
@@ -7,11 +7,11 @@
 ;; $Id$
 ;;
 ;;; Commentary:
-;; 
+;;
 ;; Define some fontsets to try to select fonts that display many symbols.
 ;;
 ;; Select one of these fontsets via the menu Options -> Set Font/Fontset
-;; or, with M-x set-default-font 
+;; or, with M-x set-default-font
 ;;
 ;; Recommended & free fonts to install on your system are:
 ;;
@@ -37,11 +37,11 @@
   (dolist (size '(10 12 14 18 22))
     (add-to-list 'pg-fontsets-names
 	(create-fontset-from-fontset-spec
-	 (replace-regexp-in-string 
+	 (replace-regexp-in-string
 	  "%T" (car (split-string basefont))
-	 (replace-regexp-in-string 
+	 (replace-regexp-in-string
 	  "%S" (int-to-string size)
-	  (replace-regexp-in-string 
+	  (replace-regexp-in-string
 	   "%F" basefont
 "-*-%F-*-*-*--%S-*-*-*-*-*-fontset-PG%T,
 gnu-unifont:-*-%F-*-*-*--%S-*-*-*-*-*-iso10646-1"
@@ -52,17 +52,17 @@ gnu-unifont:-*-%F-*-*-*--%S-*-*-*-*-*-iso10646-1"
 ;mule-unicode-e000-ffff:-*-%F-medium-r-normal--%S--*-*-*-*-*-iso10646-1"
 )))))))
 
-(defconst pg-fontsets-base-fonts 
+(defconst pg-fontsets-base-fonts
   '("dejavu lgc sans mono"
-    "liberation mono" 
+    "liberation mono"
     "stixregular"
     "lucidasanstypewriter"))
 
 (defun pg-fontsets-make-fontsets ()
   (setq pg-fontsets-names nil)
-  (mapcar 'pg-fontsets-make-fontsetsizes 
+  (mapcar 'pg-fontsets-make-fontsetsizes
 	  pg-fontsets-base-fonts))
-;    (custom-initialize-default 'pg-fontsets-default-fontset 
+;    (custom-initialize-default 'pg-fontsets-default-fontset
 ;			       (nth 2 pg-fontsets-names))
 ;  (setq pg-fontsets-default-fontset (nth 2 pg-fontsets-names))
 ;  (set-default-font pg-fontsets-default-fontset))
diff --git a/lib/proof-compat.el b/lib/proof-compat.el
index a37ddab9..3f84481a 100644
--- a/lib/proof-compat.el
+++ b/lib/proof-compat.el
@@ -1,6 +1,6 @@
 ;; proof-compat.el   Operating system and Emacs version compatibility
 ;;
-;; Copyright (C) 2000-2009 LFCS Edinburgh. 
+;; Copyright (C) 2000-2009 LFCS Edinburgh.
 ;; Author:      David Aspinall <David.Aspinall@ed.ac.uk> and others
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
@@ -11,7 +11,7 @@
 ;; track of them.
 ;;
 ;; The development policy for Proof General (since v3.7) is for the
-;; main codebase to be written for the latest stable version of 
+;; main codebase to be written for the latest stable version of
 ;; GNU Emacs, following GNU Emacs advice on obsolete function calls.
 ;;
 ;; Since Proof General 4.0, XEmacs is not supported at all.
@@ -34,7 +34,7 @@
 
 
 ;; Workaround a small bug in Carbon Emacs Winter 2008 (at least)
-;; Menu presses query this variable, but it's not bound unless 
+;; Menu presses query this variable, but it's not bound unless
 ;; mode engaged.  Not noticeable in normal use, but it is as soon
 ;; as debug-on-error is engaged.
 (if (and (boundp 'carbon-emacs-package-version)
@@ -53,9 +53,9 @@
   "Remove a custom setting SYMBOL.
 Done by `makunbound' and removing all properties mentioned by custom library."
   (mapcar (lambda (prop) (remprop symbol prop))
-	  '(default 
-	     standard-value 
-	     force-value 
+	  '(default
+	     standard-value
+	     force-value
 	     variable-comment
 	     saved-variable-comment
 	     variable-documentation
@@ -87,8 +87,8 @@ The value returned is the value of the last form in BODY."
   (let ((old-frame (gensym "ssf")))
     `(let ((,old-frame (selected-frame)))
        (unwind-protect
-           (progn ,@body)
-         (select-frame ,old-frame))))))
+	   (progn ,@body)
+	 (select-frame ,old-frame))))))
 
 ;; An implemenation of buffer-syntactic-context for GNU Emacs
 (defun proof-buffer-syntactic-context-emulate (&optional buffer)
@@ -114,7 +114,7 @@ The returned value is one of the following symbols:
 
 
 ;; These functions are used in the intricate logic around
-;; shrink-to-fit.  
+;; shrink-to-fit.
 
 ;; window-leftmost-p, window-rightmost-p: my implementations
 (or (fboundp 'window-leftmost-p)
@@ -142,7 +142,7 @@ The returned value is one of the following symbols:
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
-;;; A naughty hack to completion.el 
+;;; A naughty hack to completion.el
 ;;;
 ;;; At the moment IMO completion too eagerly adds stuff to
 ;;; its database: the completion-before-command function
@@ -152,16 +152,16 @@ The returned value is one of the following symbols:
 '(defun completion-before-command ()
   (if (and (symbolp this-command) (get this-command 'completion-function))
 	(funcall (get this-command 'completion-function)))))
-      
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
 ;;; General Emacs version compatibility
 ;;;
 
-(defalias 'proof-buffer-syntactic-context 
+(defalias 'proof-buffer-syntactic-context
 	  'proof-buffer-syntactic-context-emulate)
 
-   
+
 ;; End of proof-compat.el
 (provide 'proof-compat)
diff --git a/lib/scomint.el b/lib/scomint.el
index f185ffb1..a8e0a300 100644
--- a/lib/scomint.el
+++ b/lib/scomint.el
@@ -7,13 +7,13 @@
 ;; $Id$
 
 ;;; Commentary:
-;; 
+;;
 ;; This is a heavily simplified comint for Proof General.
 ;; Much of the code is taken from comint.el.
 ;;
 ;; The reason to provide this is to remove some of
-;; the interactive features which are otherwise 
-;; hard to disentangle.  
+;; the interactive features which are otherwise
+;; hard to disentangle.
 ;;
 
 (defface scomint-highlight-input '((t (:weight bold)))
@@ -186,9 +186,9 @@ buffer.  The hook `scomint-exec-hook' is run after each exec."
 			 ;; If the command has slashes, make sure we
 			 ;; first look relative to the current directory.
 			 (cons default-directory exec-path) exec-path)))
-      (setq proc (apply (if (fboundp 'start-file-process) 
+      (setq proc (apply (if (fboundp 'start-file-process)
 			    ;; da: start-file-process is Emacs23 only
-			    'start-file-process 'start-process) 
+			    'start-file-process 'start-process)
 			name buffer command switches)))
     ;; Some file name handler cannot start a process, fe ange-ftp.
     (unless (processp proc) (error "No process started"))
@@ -218,7 +218,7 @@ buffer.  The hook `scomint-exec-hook' is run after each exec."
 (defun scomint-send-input (&optional no-newline artificial)
   "Send input to process.
 After the process output mark, sends all text from the process mark to
-point as input to the process.  
+point as input to the process.
 
 This command also sends and inserts a final newline, unless
 NO-NEWLINE is non-nil."
@@ -228,34 +228,34 @@ NO-NEWLINE is non-nil."
     (if (not proc) (error "Current buffer has no process")
       (widen)
       (let* ((pmark (process-mark proc))
-             (input (if (>= (point) (marker-position pmark))
+	     (input (if (>= (point) (marker-position pmark))
 			(buffer-substring pmark (point)))))
-	
-        (unless no-newline
-          (insert ?\n))
-
-        (let ((beg (marker-position pmark))
-              (end (if no-newline (point) (1- (point))))
-              (inhibit-modification-hooks t))
-          ;; (when (> end beg)
-          ;;   (add-text-properties beg end
-          ;;                        '(front-sticky t
-          ;;                          font-lock-face scomint-highlight-input))
-
-          ;; (unless no-newline
-          ;;   ;; Cover the terminating newline
-          ;;   (add-text-properties end (1+ end)
-          ;;                        '(rear-nonsticky t
-          ;;                          field boundary
-          ;;                          inhibit-line-move-field-capture t))))
-
-        ;; Update the markers before we send the input
-        ;; in case we get output amidst sending the input.
-        (set-marker scomint-last-input-start pmark)
-        (set-marker scomint-last-input-end (point))
-        (set-marker (process-mark proc) (point))
-	(scomint-send-string 
-	 proc 
+
+	(unless no-newline
+	  (insert ?\n))
+
+	(let ((beg (marker-position pmark))
+	      (end (if no-newline (point) (1- (point))))
+	      (inhibit-modification-hooks t))
+	  ;; (when (> end beg)
+	  ;;   (add-text-properties beg end
+	  ;;                        '(front-sticky t
+	  ;;                          font-lock-face scomint-highlight-input))
+
+	  ;; (unless no-newline
+	  ;;   ;; Cover the terminating newline
+	  ;;   (add-text-properties end (1+ end)
+	  ;;                        '(rear-nonsticky t
+	  ;;                          field boundary
+	  ;;                          inhibit-line-move-field-capture t))))
+
+	;; Update the markers before we send the input
+	;; in case we get output amidst sending the input.
+	(set-marker scomint-last-input-start pmark)
+	(set-marker scomint-last-input-end (point))
+	(set-marker (process-mark proc) (point))
+	(scomint-send-string
+	 proc
 	 (concat input (unless no-newline "\n"))))))))
 
 
@@ -270,7 +270,7 @@ NO-NEWLINE is non-nil."
 	  (if (> (point-max) scomint-buffer-maximum-size)
 	      (let ((inhibit-read-only t))
 		(delete-region (point-min)
-			       (- (point-max) 
+			       (- (point-max)
 				  scomint-buffer-maximum-size))))))))
 
 (defun scomint-strip-ctrl-m (&optional string)
@@ -295,7 +295,7 @@ NO-NEWLINE is non-nil."
       (with-current-buffer oprocbuf
 	;; Insert STRING
 	(let ((inhibit-read-only t)
-              ;; The point should float after any insertion we do.
+	      ;; The point should float after any insertion we do.
 	      (saved-point (copy-marker (point) t)))
 
 	  ;; We temporarly remove any buffer narrowing, in case the
@@ -324,40 +324,40 @@ NO-NEWLINE is non-nil."
 	    (goto-char (process-mark process)) ; in case a filter moved it
 
 	    ;; (let ((inhibit-read-only t)
-	    ;; 	  (inhibit-modification-hooks t))
+	    ;;	  (inhibit-modification-hooks t))
 	    ;;   (add-text-properties scomint-last-output-start (point)
-	    ;; 			   '(front-sticky
-	    ;; 			     (field inhibit-line-move-field-capture)
-	    ;; 			     rear-nonsticky t
-	    ;; 			     field output
-	    ;; 			     inhibit-line-move-field-capture t)))
+	    ;;			   '(front-sticky
+	    ;;			     (field inhibit-line-move-field-capture)
+	    ;;			     rear-nonsticky t
+	    ;;			     field output
+	    ;;			     inhibit-line-move-field-capture t)))
 
 	    ;; Highlight the prompt, where we define `prompt' to mean
 	    ;; the most recent output that doesn't end with a newline.
 ;;	    (let ((prompt-start (save-excursion (forward-line 0) (point)))
 ;;		  (inhibit-read-only t)
 ;;		  (inhibit-modification-hooks t))
-;; 	      (when comint-prompt-read-only
-;; 		(or (= (point-min) prompt-start)
-;; 		    (get-text-property (1- prompt-start) 'read-only)
-;; 		    (put-text-property
-;; 		     (1- prompt-start) prompt-start 'read-only 'fence))
-;; 		(add-text-properties
-;; 		 prompt-start (point)
-;; 		 '(read-only t rear-nonsticky t front-sticky (read-only))))
-;; 	      (unless (and (bolp) (null comint-last-prompt-overlay))
-;; 		;; Need to create or move the prompt overlay (in the case
-;; 		;; where there is no prompt ((bolp) == t), we still do
-;; 		;; this if there's already an existing overlay).
-;; 		(if comint-last-prompt-overlay
-;; 		    ;; Just move an existing overlay
-;; 		    (move-overlay comint-last-prompt-overlay
-;; 				  prompt-start (point))
-;; 		  ;; Need to create the overlay
-;; 		  (setq comint-last-prompt-overlay
-;; 			(make-overlay prompt-start (point)))
-;; 		  (overlay-put comint-last-prompt-overlay
-;; 			       'font-lock-face 'scomint-highlight-prompt))))
+;;	      (when comint-prompt-read-only
+;;		(or (= (point-min) prompt-start)
+;;		    (get-text-property (1- prompt-start) 'read-only)
+;;		    (put-text-property
+;;		     (1- prompt-start) prompt-start 'read-only 'fence))
+;;		(add-text-properties
+;;		 prompt-start (point)
+;;		 '(read-only t rear-nonsticky t front-sticky (read-only))))
+;;	      (unless (and (bolp) (null comint-last-prompt-overlay))
+;;		;; Need to create or move the prompt overlay (in the case
+;;		;; where there is no prompt ((bolp) == t), we still do
+;;		;; this if there's already an existing overlay).
+;;		(if comint-last-prompt-overlay
+;;		    ;; Just move an existing overlay
+;;		    (move-overlay comint-last-prompt-overlay
+;;				  prompt-start (point))
+;;		  ;; Need to create the overlay
+;;		  (setq comint-last-prompt-overlay
+;;			(make-overlay prompt-start (point)))
+;;		  (overlay-put comint-last-prompt-overlay
+;;			       'font-lock-face 'scomint-highlight-prompt))))
 
 	    (goto-char saved-point)))))))
 
diff --git a/lib/span.el b/lib/span.el
index 5f87e015..aa1cf9a6 100644
--- a/lib/span.el
+++ b/lib/span.el
@@ -8,9 +8,9 @@
 ;; $Id$
 ;;
 ;;; Commentary:
-;; 
+;;
 ;; Spans are our abstraction of extents/overlays.  Nowadays
-;; we implement them directly with overlays.  
+;; we implement them directly with overlays.
 ;;
 ;; In future this module should be used to implement the abstraction
 ;; for script buffers (only) more directly.
@@ -56,7 +56,7 @@ Optional argument FUN is used in place of `span-give-warning'."
   (unless fun (setq fun 'span-give-warning))
   (lexical-let ((fun fun))
     (let ((funs (list (lambda (span afterp beg end &rest args)
-                        (if (not afterp) (funcall fun beg end))))))
+			(if (not afterp) (funcall fun beg end))))))
       (span-set-property span 'modification-hooks funs)
       (span-set-property span 'insert-in-front-hooks funs))))
 
@@ -116,13 +116,13 @@ A span is before PT if it begins before the character before PT."
     ;; "Get the smallest".  I have no idea what that means, so I just do
     ;; something somewhat random but vaguely meaningful.  -Stef
     (car (last (sort ols 'span-lt)))))
-  
+
 (defun prev-span (span prop)
   "Return span before SPAN with property PROP."
   (span-at-before (span-start span) prop))
 
 ; overlays are [start, end)
- 
+
 (defun next-span (span prop)
   "Return span after SPAN with property PROP."
   ;; Presuming the span-extents.el is the reference, its code does the same
@@ -202,7 +202,7 @@ A span is before PT if it begins before the character before PT."
 
 ;;
 ;; Generic functions built on low-level concrete ones.
-;; 
+;;
 
 (defsubst span-delete-spans (start end prop)
   "Delete all spans between START and END with property PROP set."
@@ -211,7 +211,7 @@ A span is before PT if it begins before the character before PT."
 (defsubst span-property-safe (span name)
   "Like span-property, but return nil if SPAN is nil."
   (and span (span-property span name)))
-  
+
 (defsubst span-set-start (span value)
   "Set the start point of SPAN to VALUE."
   (span-set-endpoints span value (span-end span)))
diff --git a/lib/texi-docstring-magic.el b/lib/texi-docstring-magic.el
index 5cb383b9..d95f12fc 100644
--- a/lib/texi-docstring-magic.el
+++ b/lib/texi-docstring-magic.el
@@ -10,7 +10,7 @@
 ;; This file is distributed under the terms of the GNU General Public
 ;; License, Version 2.  Find a copy of the GPL with your version of
 ;; GNU Emacs or Texinfo.
-;; 
+;;
 ;;
 ;; This package generates Texinfo source fragments from Emacs
 ;; docstrings.  This avoids documenting functions and variables in
@@ -25,7 +25,7 @@
 ;;  * Arguments to functions should be written in upper case: ARG1..ARGN
 ;;  * User options (variables users may want to set) should have docstrings
 ;;    beginning with an asterisk.
-;;  
+;;
 ;; Usage:
 ;;
 ;;  Write comments of the form:
@@ -38,7 +38,7 @@
 ;;
 ;;  This will insert @defopt, @deffn and the like underneath the
 ;;  magic comment strings.
-;;  
+;;
 ;;  The default value for user options will be printed.
 ;;
 ;;  Symbols are recognized if they are defined for faces, functions,
@@ -47,7 +47,7 @@
 ;; Automatic markup rules:
 ;;
 ;; 1. Indented lines are gathered into a @lisp environment.
-;; 2. Pieces of text `stuff' or surrounded in quotes marked up with @samp. 
+;; 2. Pieces of text `stuff' or surrounded in quotes marked up with @samp.
 ;; 3. Words *emphasized* are made @strong{emphasized}
 ;; 4. Words sym-bol which are symbols become @code{sym-bol}.
 ;; 5. Upper cased words ARG corresponding to arguments become @var{arg}.
@@ -67,7 +67,7 @@
 ;; Useful enhancements to do:
 ;;
 ;;  * Tweak replacement: at the moment it skips blank lines
-;;    under magic comment. 
+;;    under magic comment.
 ;;  * Use customize properties (e.g. group, simple types)
 ;;  * Look for a "texi-docstring" property for symbols
 ;;    so TeXInfo can be defined directly in case automatic markup
@@ -80,7 +80,7 @@
 ;;
 ;; Thanks to: Christoph Conrad for an Emacs compatibility fix.
 ;;
-;; 
+;;
 
 (eval-when-compile
   (require 'cl))
@@ -174,17 +174,17 @@
     ("\\(\\(^\\s-*$\\)\n@end lisp\\)" t "@end lisp")
     ;; 9. Hack to remove @samp{@var{...}} sequences.
     ;; Changed to just @samp of uppercase.
-    ("\\(@samp{@var{\\([^}]+\\)}}\\)" 
+    ("\\(@samp{@var{\\([^}]+\\)}}\\)"
      t
      (concat "@samp{" (upcase (match-string 2 docstring)) "}")))
     "Table of regexp matches and replacements used to markup docstrings.
 Format of table is a list of elements of the form
    (regexp predicate replacement-form)
 If regexp matches and predicate holds, then replacement-form is
-evaluated to get the replacement for the match.  
+evaluated to get the replacement for the match.
 predicate and replacement-form can use variables arg,
 and forms such as (match-string 1 docstring)
-Match string 1 is assumed to determine the 
+Match string 1 is assumed to determine the
 length of the matched item, hence where parsing restarts from.
 The replacement must cover the whole match (match string 0),
 including any whitespace included to delimit matches.")
@@ -210,7 +210,7 @@ including any whitespace included to delimit matches.")
 	    (replace    (nth 2 test))
 	    (i		0)
 	    in-quoted-region)
-	
+
 	(while (and
 		(< i (length docstring))
 		(string-match regexp docstring i))
@@ -228,14 +228,14 @@ including any whitespace included to delimit matches.")
   ;; if not already a new paragraph.
   (let*
       ((pos      (string-match "\n" docstring))
-       (needscr  (and pos 
-		      (not (string= "\n" 
-				    (substring docstring 
-					       (1+ pos) 
+       (needscr  (and pos
+		      (not (string= "\n"
+				    (substring docstring
+					       (1+ pos)
 					       (+ pos 2)))))))
     (if (and pos needscr)
 	(concat (substring docstring 0 pos)
-		"@*\n" 
+		"@*\n"
 		(substring docstring (1+ pos)))
       docstring)))
 
@@ -258,7 +258,7 @@ Markup as @code{stuff} or @lisp stuff @end lisp."
   ;; NB: might be nice to use a 'default-value-description
   ;; property here, in case the default value is computed.
   (let ((text       (format "%S" default)))
-    (concat 
+    (concat
      "\nThe default value is "
      (if (string-match "\n" text)
 	 ;; Carriage return will break @code, use @lisp
@@ -266,7 +266,7 @@ Markup as @code{stuff} or @lisp stuff @end lisp."
 	     (concat "the string: \n@lisp\n" default "\n@end lisp\n")
 	   (concat "the value: \n@lisp\n" text "\n@end lisp\n"))
        (concat "@code{" text "}.\n")))))
- 
+
 
 (defun texi-docstring-magic-texi-for (symbol &optional noerror)
   (cond
@@ -320,7 +320,7 @@ Markup as @code{stuff} or @lisp stuff @end lisp."
 	(texi-docstring-magic-texi "fn" "Macro" name docstring args))
        (t
 	(texi-docstring-magic-texi "un" nil name docstring args)))))
-   (noerror 
+   (noerror
     (message "Warning: symbol `%s' not defined" (symbol-name symbol))
     "")
    (t
@@ -360,7 +360,7 @@ With prefix arg, no errors on unknown symbols.  (This results in
 	      (forward-line)
 	      (delete-region p (point))
 	      (setq deleted t)))
-	(insert 
+	(insert
 	 (texi-docstring-magic-texi-for symbol noerror))
 	(unless deleted
 	  ;; Follow newly inserted @def with a single blank.
@@ -382,17 +382,17 @@ With prefix arg, no errors on unknown symbols.  (This results in
 	(set-syntax-table stab)))))
 
 (defun texi-docstring-magic-insert-magic (symbol)
-  (interactive 
+  (interactive
    (let* ((v (or (variable-at-point)
 		 (and (fboundp 'function-at-point) (function-at-point))
 		 (and (fboundp 'function-called-at-point) (function-called-at-point))
 		 (texi-docstring-magic-face-at-point)))
 	  (val (let ((enable-recursive-minibuffers t))
-                 (completing-read
+		 (completing-read
 		  (if v
 		      (format "Magic docstring for symbol (default %s): " v)
 		     "Magic docstring for symbol: ")
-                   obarray '(lambda (sym)
+		   obarray '(lambda (sym)
 			      (or (boundp sym)
 				  (fboundp sym)
 				  (texi-docstring-magic-find-face sym)))
@@ -400,5 +400,5 @@ With prefix arg, no errors on unknown symbols.  (This results in
      (list (if (equal val "") v (intern val)))))
   (insert "\n" texi-docstring-magic-comment " " (symbol-name symbol)))
 
-	
+
 (provide 'texi-docstring-magic)
diff --git a/lib/unicode-chars.el b/lib/unicode-chars.el
index dfab97c9..5b566fb3 100644
--- a/lib/unicode-chars.el
+++ b/lib/unicode-chars.el
@@ -1,4 +1,4 @@
-;; unicode-chars.el --- table of Unicode characters 
+;; unicode-chars.el --- table of Unicode characters
 ;;
 ;; Author:    David Aspinall
 ;; $Id$
@@ -5048,7 +5048,7 @@
 ;; Modified a bit by me to use its own help-style buffer
 
 (defun unicode-chars-list-chars ()
-  "Insert each Unicode character into a buffer. 
+  "Insert each Unicode character into a buffer.
 Lets you see which characters are available for literal display
 in your emacs font."
   (interactive)