Clean whitespace

28 files changed, 820 insertions, 823 deletions

diff --git a/acl2/acl2.el b/acl2/acl2.el
index da745d06..809c62fa 100644
--- a/acl2/acl2.el
+++ b/acl2/acl2.el
@@ -1,6 +1,6 @@
 ;; acl2.el   Basic Proof General instance for ACL2
 ;;
-;; Copyright (C) 2000 LFCS Edinburgh. 
+;; Copyright (C) 2000 LFCS Edinburgh.
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Author:    David Aspinall <David.Aspinall@ed.ac.uk>
 ;;
@@ -15,11 +15,11 @@
 (require 'proof-syntax)			; functions for making regexps
 
 (setq auto-mode-alist                   ; ACL2 uses two file extensions
-      (cons				; Only grab .lisp extension after 
+      (cons				; Only grab .lisp extension after
        (cons "\\.lisp$" 'acl2-mode)	; an acl2 file has been loaded
-       auto-mode-alist))	
+       auto-mode-alist))
 
-(proof-easy-config  'acl2 "ACL2" 
+(proof-easy-config  'acl2 "ACL2"
  proof-assistant-home-page       "http://www.cs.utexas.edu/users/moore/acl2"
  proof-prog-name		 "acl2"
 
@@ -32,7 +32,7 @@
  proof-goal-command-regexp       "(def\\w+\\s "
  proof-save-with-hole-regexp     "(def\\w+[ \t\n]+\\(\\w+\\)"
  proof-save-with-hole-result	 1
- proof-shell-error-regexp	 
+ proof-shell-error-regexp
  "^Error: \\|Error in TOP-LEVEL: \\|\\*\\*\\*\\* FAILED \\*\\*\\*"
  proof-shell-interrupt-regexp    "Correctable error: Console interrupt."
 
@@ -52,7 +52,7 @@
  proof-script-syntax-table-entries
  '(?\[ "(]  "
    ?\] "([  "
-   ?\( "()  " 
+   ?\( "()  "
    ?\) ")(  "
    ?.  "w   "
    ?_  "w   "
@@ -62,7 +62,7 @@
    ?\' "'    "
    ?`  "'    "
    ?,  "'    "
-   ?\| "."   
+   ?\| "."
    ?\; "<    "
    ?\n ">    "
    )
diff --git a/ccc/ccc.el b/ccc/ccc.el
index 0fdf77de..9b5c35e4 100644
--- a/ccc/ccc.el
+++ b/ccc/ccc.el
@@ -1,27 +1,27 @@
 ;; ccc.el - Proof General for the Casl Consistency Checker
-;; 
+;;
 ;; Author: Christoph Lüth <cxl@informatik.uni-bremen.de>
-;;        
+;;
 ;; This is a fairly straightforward instantiation of Proof General for
-;; the Casl Consistency Checker, CCC. 
+;; the Casl Consistency Checker, CCC.
 ;;
 ;; CASL is the standard algebraic specification language, and CCC is a
 ;; tool to check consistency of CASL specifications.
-;; 
+;;
 ;; For more information, hasten thee browser yonder:
 ;;   http://www.informatik.uni-bremen.de/cofi/ccc
 
 (require 'proof-easy-config)            ; nice and easy does it
 (require 'proof-syntax)			; functions for making regexps
 
-(proof-easy-config  'ccc "CASL Consistency Checker" 
+(proof-easy-config  'ccc "CASL Consistency Checker"
  proof-prog-name		 "ccc" ;; must be in your path.
  proof-terminal-char             ?\;
  proof-script-comment-start      "(*"
  proof-script-comment-end        "*)"
  proof-goal-command-regexp       "\\(ccc\\|holcasl\\) \".*\";"
  proof-save-command-regexp       "^qeccc"
- proof-goal-with-hole-regexp     "\\(ccc\\|holcasl\\) \"\\(\\(.*\\)\\)\"" 
+ proof-goal-with-hole-regexp     "\\(ccc\\|holcasl\\) \"\\(\\(.*\\)\\)\""
  proof-save-with-hole-regexp     "qeccc \"\\(\\(.*\\)\\)\""
  proof-non-undoables-regexp      "undo\\|back"
  proof-goal-command              "ccc \"%s\";"
@@ -29,7 +29,7 @@
  proof-kill-goal-command         "abort ();"
  proof-showproof-command         "prt()"
  proof-undo-n-times-cmd          "undo_steps %s;"
- proof-auto-multiple-files       nil 
+ proof-auto-multiple-files       nil
  proof-shell-cd-cmd              "cd \"%s\""
  proof-shell-interrupt-regexp    "Interrupt"
  proof-shell-start-goals-regexp  "^No subgoals\\|^[0-9]* subgoals\\|^Wts:"
@@ -43,35 +43,35 @@
  proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading" ;;; ???
 
  ;;
- ;; Some basic fontlocking and syntax table entries, as taken from the 
+ ;; Some basic fontlocking and syntax table entries, as taken from the
  ;; hol98 instance (it's all SML anyway :-)
  ;;
  proof-script-syntax-table-entries
  '(?\` "\""
-   ?\$ "."   
-   ?\/ "."   
-   ?\\ "."   
-   ?+  "."   
-   ?-  "."   
-   ?=  "."   
-   ?%  "."   
-   ?<  "."   
-   ?>  "."   
-   ?\& "."   
-   ?.  "w"   
-   ?_  "w"   
-   ?\' "w"   
+   ?\$ "."
+   ?\/ "."
+   ?\\ "."
+   ?+  "."
+   ?-  "."
+   ?=  "."
+   ?%  "."
+   ?<  "."
+   ?>  "."
+   ?\& "."
+   ?.  "w"
+   ?_  "w"
+   ?\' "w"
    ?\| "."
    ?\[ "(]"
-   ?\] ")["   
+   ?\] ")["
    ?\* ". 23"
-   ?\( "()1" 
+   ?\( "()1"
    ?\) ")(4")
 
  ccc-keywords  '("use" "ap" "holcasl" "ccc" "load_lib" "qeccc")
  ccc-tactics   '("compose" "compose'" "prove" "prove_free_type")
  ccc-tacticals '("Repeat" "Orelse" "Then" "ThenList" "OrelseList")
- proof-script-font-lock-keywords	
+ proof-script-font-lock-keywords
  (list
   (cons (proof-ids-to-regexp ccc-keywords) 'font-lock-keyword-face)
   (cons (proof-ids-to-regexp ccc-tactics) 'font-lock-keyword-face)
@@ -80,6 +80,3 @@
 
 
 )
-
-
-
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 7a24bf6c..a5131f10 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -1,5 +1,5 @@
 ;;; coq-abbrev.el --- coq abbrev table and menus for ProofGeneral mode
-;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
+;; Copyright (C) 1994 - 1998 LFCS Edinburgh.
 ;; Authors: Healfdene Goguen, Pierre Courtieu
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
@@ -172,4 +172,3 @@
 
 
 (provide 'coq-abbrev)
-
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index 35e21030..ec5465e2 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -16,4 +16,3 @@
 
   (pg-autotest-quit-prover)
   (pg-autotest-finished))
-
diff --git a/coq/coq-db.el b/coq/coq-db.el
index bcc4a1e4..1be7719a 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -12,7 +12,7 @@
 ;;; real value defined below
 
 ;;; Commentary:
-;; 
+;;
 
 ;;; Code:
 
@@ -71,11 +71,11 @@ Insert corresponding string with holes at point.  If an insertion function is
 present for the keyword, call it instead.  see `coq-syntax-db' for DB
 structure."
   (let* ((tac (completing-read (concat prompt " (tab for completion) : ")
-                               db nil nil))
-         (infos (cddr (assoc tac db)))
-         (s (car infos)) ; completion to insert
-         (f (car-safe (cdr-safe (cdr-safe (cdr infos))))) ; insertion function
-         (pt (point)))
+			       db nil nil))
+	 (infos (cddr (assoc tac db)))
+	 (s (car infos)) ; completion to insert
+	 (f (car-safe (cdr-safe (cdr-safe (cdr infos))))) ; insertion function
+	 (pt (point)))
     (if f (funcall f) ; call f if present
       (insert (or s tac)) ; insert completion and indent otherwise
       (holes-replace-string-by-holes-backward-jump pt)
@@ -91,16 +91,16 @@ regexp.  See `coq-syntax-db' for DB structure."
   (let ((l db) (res ()))
     (while l
       (let* ((hd (car l)) (tl (cdr l))	; hd is the first infos list
-             (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
-             (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
-             (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion
-             (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing
-             (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string
-             )
-        ;; TODO delete doublons
-        (when (and e5 (or (not filter) (funcall filter hd)))
-          (setq res (nconc res (list e5)))) ; careful: nconc destructive!
-        (setq l tl)))
+	     (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
+	     (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
+	     (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion
+	     (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing
+	     (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string
+	     )
+	;; TODO delete doublons
+	(when (and e5 (or (not filter) (funcall filter hd)))
+	  (setq res (nconc res (list e5)))) ; careful: nconc destructive!
+	(setq l tl)))
     res
     ))
 
@@ -162,9 +162,9 @@ for DB structure."
 	  (car-safe (car-safe (nthcdr (- size 1) db)))))
 
 (defun coq-sort-menu-entries (menu)
-  (sort menu 
-	'(lambda (x y) (string< 
-			(downcase (elt x 0)) 
+  (sort menu
+	'(lambda (x y) (string<
+			(downcase (elt x 0))
 			(downcase (elt y 0))))))
 
 (defun coq-build-menu-from-db (db &optional size)
@@ -178,11 +178,11 @@ structure."
     (while l
       (if (<= lgth sz)
 	  (setq res ;; careful: nconc destructive!
-		(nconc res (list (cons 
+		(nconc res (list (cons
 				  (coq-build-title-menu l lgth)
 				  (coq-build-menu-from-db-internal l lgth wdth)))))
 	(setq res ; careful: nconc destructive!
-	      (nconc res (list (cons 
+	      (nconc res (list (cons
 				(coq-build-title-menu l sz)
 				(coq-build-menu-from-db-internal l sz wdth))))))
       (setq l (nthcdr sz l))
@@ -226,7 +226,7 @@ See `coq-syntax-db' for DB structure."
 
 
 ;;A new face for tactics which fail when they don't kill the current goal
-(defface coq-solve-tactics-face 
+(defface coq-solve-tactics-face
   (proof-face-specs
    (:foreground "red") ; pour les fonds clairs
    (:foreground "red") ; pour les fond foncés
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index d16b635a..bf506d7f 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -9,7 +9,7 @@
 
 
 ;;; Commentary:
-;; 
+;;
 
 (require 'coq-syntax)
 
@@ -73,7 +73,7 @@ detect if they start something or not."
          (with (coq-count-match "\\<with\\>" str))
          (letwith (+ (coq-count-match "\\<let\\>" str) (- with match)))
          (affect (coq-count-match ":=" str)))
-		  
+
     (and (proof-string-match coq-goal-command-regexp str)
          (not
           (and (proof-string-match "\\`\\(Local\\|Definition\\|Lemma\\|Module\\)\\>" str)
@@ -195,9 +195,9 @@ found, go as far as possible and return nil."
 
 (defun coq-find-not-in-comment-forward (reg &optional lim submatch)
   "Moves to the first not commented occurrence of REG found looking down.
-The point is put exactly before the occurrence if SUBMATCH is nil, 
-otherwise the point is put before SUBMATCHnth matched sub-expression 
-\(see `match-string').  If no occurrence is found, go as far as possible 
+The point is put exactly before the occurrence if SUBMATCH is nil,
+otherwise the point is put before SUBMATCHnth matched sub-expression
+\(see `match-string').  If no occurrence is found, go as far as possible
 and return nil."
   ;; da: PATCH here for http://proofgeneral.inf.ed.ac.uk/trac/ticket/173
   ;; (nasty example).  But I don't understand this code!
@@ -312,7 +312,7 @@ not inside the {} of a record)."
     (let ((oldpt (point))
           (topnotreached (= (forward-line -1) 0))) ;;; nil if going one line backward
                                                    ;;; is not possible
-      
+
       (while (and topnotreached
                   (not (coq-find-no-syntactic-on-line))
                   t ;;(> (line-number (point)) (line-number (point-min)))
@@ -345,16 +345,16 @@ not inside the {} of a record)."
 
 (defun coq-find-unclosed (&optional optlvl limit openreg closereg)
   "Finds the first unclosed open item (backward), counter starts to optlvl (default 1) and stops when reaching limit (default point-min)."
-  
+
   (let* ((lvl (or optlvl 1))
-         (open-re  (if openreg 
+         (open-re  (if openreg
                        (proof-regexp-alt openreg proof-indent-open-regexp)
                      proof-indent-open-regexp))
-         (close-re (if closereg 
+         (close-re (if closereg
                        (proof-regexp-alt closereg proof-indent-close-regexp)
                      proof-indent-close-regexp))
          (both-re (proof-regexp-alt "\\`" close-re open-re))
-         (nextpt (save-excursion 
+         (nextpt (save-excursion
                    (proof-re-search-backward both-re))))
     (while
         (and (not (= lvl 0))
@@ -374,17 +374,17 @@ not inside the {} of a record)."
 
 
 (defun coq-find-at-same-level-zero (limit openreg)
-  "Move to open or openreg (first found) at same parenthesis level as point. 
+  "Move to open or openreg (first found) at same parenthesis level as point.
 Returns point if found."
   (let* ((found nil)
-         (open-re (if openreg 
+         (open-re (if openreg
                       (proof-regexp-alt openreg proof-indent-open-regexp)
                     proof-indent-open-regexp))
          (close-re proof-indent-close-regexp)
          (both-re (proof-regexp-alt "\\`" close-re open-re))
-         (nextpt (save-excursion 
+         (nextpt (save-excursion
                    (proof-re-search-backward both-re))))
-    
+
     (while
         (and (not found)
              (>= nextpt (or limit (point-min)))
@@ -403,7 +403,7 @@ Returns point if found."
 
 (defun coq-find-unopened (&optional optlvl limit)
   "Finds the last unopened close item (looking forward from point), counter starts to OPTLVL (default 1) and stops when reaching limit (default point-max). This function only works inside an expression."
-  
+
   (let ((lvl (or optlvl 1)) after nextpt endpt)
     (save-excursion
       (proof-re-search-forward
@@ -421,10 +421,10 @@ Returns point if found."
       (setq endpt (point))
       (cond
        ((proof-looking-at-syntactic-context) ())
-       
+
        ((proof-looking-at-safe proof-indent-close-regexp)
         (setq lvl (- lvl 1)))
-       
+
        ((proof-looking-at-safe proof-indent-open-regexp)
         (setq lvl (+ lvl 1))))
 
@@ -466,13 +466,13 @@ Returns point if found."
         (proof-re-search-backward anyreg)
         (cond
          ((proof-looking-at-syntactic-context) ())
-       
+
          ((proof-looking-at-safe proof-indent-close-regexp)
           (coq-find-unclosed))
-       
+
          ((proof-looking-at-safe proof-indent-open-regexp)
           (setq found t))
-       
+
          (t ())))
 
       (if found (current-column)
@@ -536,7 +536,7 @@ argument must be t if inside the {}s of a record, nil otherwise."
   (let ((pt (point)) real-start)
     (save-excursion
       (setq real-start (coq-find-real-start)))
-  
+
     (cond
 
      ;; at a ) -> same indent as the *line* of corresponding (
@@ -599,7 +599,7 @@ argument must be t if inside the {}s of a record, nil otherwise."
 ;;		(+ prevcol proof-indent))
 
      ((and (goto-char prevpoint) nil)) ; just for side effect: jump to previous line
-	
+
      ;; find the last unopened ) -> indentation of line + indent
      ((coq-find-last-unopened 1 pt) ; side effect, nil if no unopenned found
       (save-excursion
@@ -611,10 +611,10 @@ argument must be t if inside the {}s of a record, nil otherwise."
      ((and (goto-char prevpoint)
            (or (and (end-of-line) nil)
                (and (forward-char -1) t)) nil))
-     
+
      ((and  (proof-looking-at-safe ";") ;prev line has ";" at the end
             record)                     ; and we are inside {}s of a record
-      (save-excursion 
+      (save-excursion
         (coq-find-unclosed 1 real-start)
         (back-to-indentation)
         (+ (current-column) proof-indent)))
@@ -623,7 +623,7 @@ argument must be t if inside the {}s of a record, nil otherwise."
      ((and (goto-char prevpoint)  (not (= (coq-back-to-indentation-prevline) 0))
            (or (and (end-of-line) nil)
                (and (forward-char -1) t)) nil))
-     
+
      ((and (proof-looking-at-safe ";") ;prev prev line has ";" at the end
            record)                     ; and we are inside {}s of a record
       (save-excursion (+ prevcol proof-indent)))
@@ -632,14 +632,14 @@ argument must be t if inside the {}s of a record, nil otherwise."
 
      ;; There is a indent keyword (fun, forall etc)
      ;; and we are not in {}s of a record just after a ";"
-     ((coq-find-at-same-level-zero prevpoint coq-indent-kw) 
+     ((coq-find-at-same-level-zero prevpoint coq-indent-kw)
       (+ prevcol proof-indent))
 
      ((and (goto-char prevpoint) nil)) ;; just for side effect: go back to previous line
      ;; "|" at previous line
      ((proof-looking-at-safe coq-indent-pattern-regexp)
       (+ prevcol proof-indent))
-     
+
      (t prevcol))))
 
 
@@ -666,7 +666,7 @@ argument must be t if inside the {}s of a record, nil otherwise."
          ((and (not atstart) (proof-looking-at-syntactic-context))
           (skip-chars-forward " \t")
           (current-column))
-         
+
             ;;we were at the first line of a comment and the current line is the
             ;;previous one
          (t (goto-char oldpt)
@@ -690,7 +690,7 @@ argument must be t if inside the {}s of a record, nil otherwise."
            (coq-indent-expr-offset kind prevcol prevpoint nil))
 	  ((= kind 4) ; we are at the expression level inside {}s of a record
            (coq-indent-expr-offset kind prevcol prevpoint t))
-	  ((= kind 3) 
+	  ((= kind 3)
            (if notcomments nil (coq-indent-comment-offset))))))
 
 (defun coq-indent-calculate (&optional notcomments)
@@ -726,7 +726,7 @@ argument must be t if inside the {}s of a record, nil otherwise."
           (coq-indent-line-not-comments))
       (forward-line 1))
     (goto-char fin)))
- 
+
 
 ;;;   Local Variables: ***
 ;;;   fill-column: 85 ***
diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el
index 0d7e5926..ed001679 100644
--- a/coq/coq-local-vars.el
+++ b/coq/coq-local-vars.el
@@ -7,11 +7,11 @@
 
 
 ;;; Commentary:
-;; 
+;;
 
 
 ;;; History:
-;; 
+;;
 
 ;;; Code:
 (defconst coq-local-vars-doc nil
diff --git a/coq/coq-mmm.el b/coq/coq-mmm.el
index 068543fb..21fa678e 100644
--- a/coq/coq-mmm.el
+++ b/coq/coq-mmm.el
@@ -5,7 +5,7 @@
 ;; Licence:	 GPL
 ;;
 ;; $Id$
-;; 
+;;
 ;; We only spot some simple cases of embedded LaTeX/HTML/verbatim.
 ;;
 ;; At the moment, the insertion has a bad interaction with the holes
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 00dbcf60..bc861f06 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1,5 +1,5 @@
 ;; coq-syntax.el Font lock expressions for Coq
-;; Copyright (C) 1997-2007 LFCS Edinburgh. 
+;; Copyright (C) 1997-2007 LFCS Edinburgh.
 ;; Authors: Thomas Kleymann, Healfdene Goguen, Pierre Courtieu
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
@@ -33,14 +33,14 @@
 ;; this one is temporary, for compatibility
 (defvar coq-version-is-V8 nil "Obsolete, use `coq-version-is-V8-0' instead.")
 
-(defvar coq-version-is-V8-0 nil 
+(defvar coq-version-is-V8-0 nil
   "This variable can be set to t to force ProofGeneral to coq version
  coq-8.0. To do that, put (setq coq-version-is-V8-0 t) in your .emacs and
  restart emacs. This variable cannot be true simultaneously with
  coq-version-is-V8-1. If none of these 2 variables is set to t, then
  ProofGeneral guesses the version of coq by doing 'coqtop -v'." )
 
-(defvar coq-version-is-V8-1 nil 
+(defvar coq-version-is-V8-1 nil
   "This variable can be set to t to force ProofGeneral to coq version
  coq-8.1 and above(use it for coq-8.0cvs after january 2005). To do
  that, put \(setq coq-version-is-V8-1 t) in your .emacs and restart
@@ -52,7 +52,7 @@
 (defun coq-determine-version ()
   "Intuit the version of Coq we're using and configure accordingly."
   ;; post-cond: one of the variables is set to t
-  (let* 
+  (let*
       (
        (seedoc (concat " (to force another version, see for example"
                        " C-h v `coq-version-is-V8-0)'."))
@@ -180,7 +180,7 @@
 
 
 (defvar coq-tactics-db
-  (append 
+  (append
    coq-user-tactics-db
    '(
      ("absurd " "abs" "absurd " t "absurd")
@@ -354,12 +354,12 @@
      ("solve" nil "solve [ # | # ]" nil "solve")
      ("tauto" "ta" "tauto" t "tauto")
      ))
-  "Coq tactic(al)s that solve a subgoal." 
+  "Coq tactic(al)s that solve a subgoal."
   )
 
 
 (defvar coq-tacticals-db
-  (append 
+  (append
    coq-user-tacticals-db
    '(
      ("info" nil "info #" nil "info")
@@ -398,7 +398,7 @@
     ("Parameters" "par" "Parameter #: #" t "Parameters")
     ("Conjecture" "conj" "Conjecture #: #." t "Conjecture")
     ("Variable" "v" "Variable #: #." t "Variable")
-    ("Variables" "vs" "Variables # , #: #." t "Variables")	
+    ("Variables" "vs" "Variables # , #: #." t "Variables")
     ("Coercion" "coerc" "Coercion @{id} : @{typ1} >-> @{typ2}." t "Coercion")
     )
   "Coq declaration keywords information list. See `coq-syntax-db' for syntax."
@@ -407,7 +407,7 @@
 (defvar coq-defn-db
   '(
     ("CoFixpoint" "cfix" "CoFixpoint # (#:#) : # :=\n#." t "CoFixpoint")
-    ("CoInductive" "coindv" "CoInductive # : # :=\n|# : #." t "CoInductive") 
+    ("CoInductive" "coindv" "CoInductive # : # :=\n|# : #." t "CoInductive")
     ("Declare Module : :=" "dm" "Declare Module # : # := #." t "Declare\\s-+Module")
     ("Declare Module <: :=" "dm2" "Declare Module # <: # := #." t);; careful
     ("Declare Module Import : :=" "dmi" "Declare Module # : # := #." t)
@@ -451,7 +451,7 @@
     ("Scheme" "sc" "Scheme @{name} := #." t "Scheme")
     ("Scheme Induction" "sci" "Scheme @{name} := Induction for # Sort #." t)
     ("Scheme Minimality" "scm" "Scheme @{name} := Minimality for # Sort #." t)
-    ("Structure" "str" "Structure # : # := {\n# : #;\n# : # }" t "Structure")	
+    ("Structure" "str" "Structure # : # := {\n# : #;\n# : # }" t "Structure")
     )
   "Coq definition keywords information list. See `coq-syntax-db' for syntax. "
   )
@@ -604,14 +604,14 @@
      ("Unset Printing Notations" "unsprn" "Unset Printing Notations" nil "Unset\\s-+Printing\\s-+Notations")
      ("Unset Undo" nil "Unset Undo." nil "Unset\\s-+Undo")
  ;    ("print" "pr" "print #" "print")
-     )   
+     )
    "Command that are not declarations, definition or goal starters."
   )
 
 (defvar coq-commands-db
   (append coq-decl-db coq-defn-db coq-goal-starters-db
           coq-other-commands-db coq-user-commands-db)
-  "Coq all commands keywords information list. See `coq-syntax-db' for syntax. "      
+  "Coq all commands keywords information list. See `coq-syntax-db' for syntax. "
   )
 
 
@@ -650,7 +650,7 @@
 
 ;; FIXME da: this one function breaks the nice configuration of Proof General:
 ;; would like to have proof-goal-regexp instead.
-;; Unfortunately Coq allows "Definition" and friends to perhaps have a goal, 
+;; Unfortunately Coq allows "Definition" and friends to perhaps have a goal,
 ;; so it appears more difficult than just a proof-goal-regexp setting.
 ;; Future improvement may simply to be allow a function value for
 ;; proof-goal-regexp.
@@ -668,19 +668,19 @@
 ;;    uniquement hors d'un MT
 ;;    - si :=MEXPR est absent, elle demarre un nouveau module interactif
 ;;    - si :=MEXPR est present, elle definit un module
-;;    (la fonction vernac_define_module dans toplevel/vernacentries) 
+;;    (la fonction vernac_define_module dans toplevel/vernacentries)
 ;;
 ;; *) la nouvelle commande Declare Module M [ ( : | <: ) MTYP ] [ := MEXPR ]
 ;;    est valable uniquement dans un MT
 ;;    - si :=MEXPR absent, :MTYP absent, elle demarre un nouveau module
 ;;      interactif
-;;    - si (:=MEXPR absent, :MTYP present) 
+;;    - si (:=MEXPR absent, :MTYP present)
 ;;      ou (:=MEXPR present, :MTYP absent)
 ;;      elle declare un module.
 ;;    (la fonction vernac_declare_module dans toplevel/vernacentries)
 
 (defun coq-count-match (regexp strg)
-  "Count the number of (maximum, non overlapping) matching substring 
+  "Count the number of (maximum, non overlapping) matching substring
  of STRG matching REGEXP. Empty match are counted once."
   (let ((nbmatch 0) (str strg))
     (while (and (proof-string-match regexp str) (not (string-equal str "")))
@@ -706,12 +706,12 @@
 	 (affect (coq-count-match ":=" str)))
 
     (and (proof-string-match coq-goal-command-regexp str)
- 	 (not				; 
- 	  (and 
- 	   (proof-string-match "\\`\\(Local\\|Definition\\|Lemma\\|Module\\)\\>" str)
- 	   (not (= letwith affect))))
- 	 (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str))
- 	 )
+	 (not				;
+	  (and
+	   (proof-string-match "\\`\\(Local\\|Definition\\|Lemma\\|Module\\)\\>" str)
+	   (not (= letwith affect))))
+	 (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str))
+	 )
     )
   )
 
@@ -722,14 +722,14 @@
 ;; TODO: have opened section/chapter in the prompt too, and get rid of
 ;; syntactical tests everywhere
 (defun coq-module-opening-p (str)
-  "Decide whether STR is a module or section opening or not. 
+  "Decide whether STR is a module or section opening or not.
 Used by `coq-goal-command-p'"
   (let* ((match (coq-count-match "\\<match\\>" str))
- 	 (with (coq-count-match "\\<with\\>" str))
- 	 (letwith (+ (coq-count-match "\\<let\\>" str) (- with match)))
- 	 (affect (coq-count-match ":=" str)))
+	 (with (coq-count-match "\\<with\\>" str))
+	 (letwith (+ (coq-count-match "\\<let\\>" str) (- with match)))
+	 (affect (coq-count-match ":=" str)))
     (and (proof-string-match "\\`\\(Module\\)\\>" str)
- 	 (= letwith affect))
+	 (= letwith affect))
     ))
 
 (defun coq-section-command-p (str)
@@ -756,15 +756,15 @@ Used by `coq-goal-command-p'"
   (or (span-property span 'goalcmd)
       ;; module and section starts are detected here
       (let ((str (or (span-property span 'cmd) "")))
- 	(or (coq-section-command-p str)
- 	    (coq-module-opening-p str))
+	(or (coq-section-command-p str)
+	    (coq-module-opening-p str))
         )))
 
 ;; In coq > 8.1 This is used only for indentation.
 (defun coq-goal-command-str-p (str)
   "Decide whether argument is a goal or not.  Use
    `coq-goal-command-p' on a span instead if posible."
-  (cond 
+  (cond
    (coq-version-is-V8-1 (coq-goal-command-str-v81-p str))
    (coq-version-is-V8-0 (coq-goal-command-str-v80-p str))
    (t (coq-goal-command-str-v80-p str));; this is temporary
@@ -773,7 +773,7 @@ Used by `coq-goal-command-p'"
 ;; This is used for backtracking
 (defun coq-goal-command-p (span)
   "Decide whether argument is a goal or not."
-  (cond 
+  (cond
    (coq-version-is-V8-1 (coq-goal-command-p-v81 span))
    (coq-version-is-V8-0 (coq-goal-command-str-v80-p (span-property span 'cmd)))
    (t (coq-goal-command-str-v80-p (span-property span 'cmd)));; this is temporary
@@ -801,7 +801,7 @@ Used by `coq-goal-command-p'"
   )
 
 
-(defvar coq-keywords-kill-goal 
+(defvar coq-keywords-kill-goal
   '("Abort"))
 
 ;; Following regexps are all state changing
@@ -826,7 +826,7 @@ Used by `coq-goal-command-p'"
    coq-keywords-goal))                  ; idem
 
 
-;; 
+;;
 (defvar coq-keywords-state-preserving-commands
   (coq-build-regexp-list-from-db coq-commands-db 'filter-state-preserving))
 
@@ -834,7 +834,7 @@ Used by `coq-goal-command-p'"
 ;; whole commands-db
 (defvar coq-keywords-commands
   (append coq-keywords-state-changing-commands
- 	  coq-keywords-state-preserving-commands)
+	  coq-keywords-state-preserving-commands)
   "All commands keyword.")
 
 (defvar coq-solve-tactics
@@ -848,7 +848,7 @@ Used by `coq-goal-command-p'"
 
  ;; From JF Monin:
 (defvar coq-reserved
-  (append 
+  (append
    coq-user-reserved-db
    '(
      "False" "True" "after" "as" "cofix" "fix" "forall" "fun" "match"
@@ -877,7 +877,7 @@ Used by `coq-goal-command-p'"
 
 (defvar coq-keywords
   (append coq-keywords-goal coq-keywords-save coq-keywords-decl
- 	  coq-keywords-defn coq-keywords-commands)
+	  coq-keywords-defn coq-keywords-commands)
   "All keywords in a Coq script.")
 
 
@@ -910,7 +910,7 @@ Used by `coq-goal-command-p'"
 (defvar coq-ids (proof-ids coq-id " "))
 
 (defun coq-first-abstr-regexp (paren end)
-  (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end)) 
+  (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end))
 
 (defcustom coq-variable-highlight-enable t
   "Activates partial bound variable highlighting"
@@ -927,7 +927,7 @@ Used by `coq-goal-command-p'"
    (list (coq-first-abstr-regexp "\\<forall\\>" "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face)
                                         ;   (list "\\<forall\\>"
                                         ;         (list 0 font-lock-type-face)
-                                        ;         (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil 
+                                        ;         (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil
                                         ;               (list 0 font-lock-variable-name-face)))
    ;; parenthesized binders
    (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face)
@@ -940,27 +940,27 @@ Used by `coq-goal-command-p'"
 ;; It is understood here as being a goal.  This is important for
 ;; recognizing global identifiers, see coq-global-p.
 (defconst coq-save-command-regexp-strict
-  (proof-anchor-regexp 
+  (proof-anchor-regexp
    (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict)
            "\\)")))
 (defconst coq-save-command-regexp
-  (proof-anchor-regexp 
+  (proof-anchor-regexp
    (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save)
            "\\)")))
 (defconst coq-save-with-hole-regexp
   (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict)
- 	  "\\)\\s-+\\(" coq-id "\\)\\s-*\\."))
+	  "\\)\\s-+\\(" coq-id "\\)\\s-*\\."))
 
 (defconst coq-goal-command-regexp
   (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-goal)))
 
 (defconst coq-goal-with-hole-regexp
   (concat "\\(" (proof-ids-to-regexp coq-keywords-goal)
- 	  "\\)\\s-+\\(" coq-id "\\)\\s-*:?"))
+	  "\\)\\s-+\\(" coq-id "\\)\\s-*:?"))
 
 (defconst coq-decl-with-hole-regexp
   (concat "\\(" (proof-ids-to-regexp coq-keywords-decl)
- 	  "\\)\\s-+\\(" coq-ids "\\)\\s-*:"))
+	  "\\)\\s-+\\(" coq-ids "\\)\\s-*:"))
 
 ;;  (defconst coq-decl-with-hole-regexp
 ;;    (if coq-variable-highlight-enable coq-decl-with-hole-regexp-1 'nil))
@@ -973,10 +973,10 @@ Used by `coq-goal-command-p'"
 ;; "with f x y :" (followed by = or not)
 ;; "with f x y (z:" (not followed by =)
 ;; BUT NOT:
-;; "with f ... (x:=" 
+;; "with f ... (x:="
 ;; "match ... with .. => "
 (defconst coq-with-with-hole-regexp
-  (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^=(.]*:\\|[^(]*(\\s-*" 
+  (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^=(.]*:\\|[^(]*(\\s-*"
           coq-id "\\s-*:[^=]\\)"))
 ;; marche aussi a peu pres
 ;;  (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(.]*:\\|.*)[^(.]*:=\\)"))
@@ -999,7 +999,7 @@ Used by `coq-goal-command-p'"
           (list 1 'font-lock-function-name-face t))
 
     (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face))
-    (if coq-variable-highlight-enable 
+    (if coq-variable-highlight-enable
         (list (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face)))
     (list
     (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face)
@@ -1028,7 +1028,7 @@ Used by `coq-goal-command-p'"
   (modify-syntax-entry ?\| ".")
 
 ;; should maybe be "_" but it makes coq-find-and-forget (in coq.el) bug
-  (modify-syntax-entry ?\. ".") 
+  (modify-syntax-entry ?\. ".")
 
   (condition-case nil
       ;; Try to use Emacs-21's nested comments.
@@ -1040,11 +1040,11 @@ Used by `coq-goal-command-p'"
 
 
 (defconst coq-generic-expression
-  (mapcar (lambda (kw) 
- 	    (list (capitalize kw)
- 		  (concat "\\<" kw "\\>" "\\s-+\\(\\w+\\)\\W" )
- 		  1))
- 	  (append coq-keywords-decl coq-keywords-defn coq-keywords-goal)))
+  (mapcar (lambda (kw)
+	    (list (capitalize kw)
+		  (concat "\\<" kw "\\>" "\\s-+\\(\\w+\\)\\W" )
+		  1))
+	  (append coq-keywords-decl coq-keywords-defn coq-keywords-goal)))
 
 (provide 'coq-syntax)
  ;;; coq-syntax.el ends here
diff --git a/coq/coq-unicode-tokens.el b/coq/coq-unicode-tokens.el
index b7a0692a..84beb4b6 100644
--- a/coq/coq-unicode-tokens.el
+++ b/coq/coq-unicode-tokens.el
@@ -161,7 +161,7 @@ You can adjust this table to add more entries, or to change entries for
 glyphs that not are available in your Emacs or chosen font.
 
 These shortcuts are only used for input; no reverse conversion is
-performed.  This means that the target strings need to have a defined 
+performed.  This means that the target strings need to have a defined
 meaning to be useful."
   :type '(repeat (cons (string :tag "Shortcut sequence")
 		       (string :tag "Unicode string")))
@@ -169,24 +169,24 @@ meaning to be useful."
   :group 'coq
   :tag "Coq Unicode Input Shortcuts")
 
-  
+
 ;;
 ;; Controls
 ;;
 
-(defconst coq-control-char-format-regexp 
+(defconst coq-control-char-format-regexp
   ;; FIXME: fix Coq identifier syntax below
   "\\(\s*%s\s*\\)\\([a-zA-Z0-9']+\\)")
 
 (defconst coq-control-char-format " %s ")
 
-(defconst coq-control-characters 
-  '(("Subscript" "__" sub) 
+(defconst coq-control-characters
+  '(("Subscript" "__" sub)
     ("Superscript" "^^" sup)))
 
 (defconst coq-control-region-format-regexp "\\(\s*%s\{\\)\\([^}]*\\)\\(\}\s*\\)")
 
-(defconst coq-control-regions 
+(defconst coq-control-regions
   '(("Subscript" "," "" sub)
     ("Superscript" "^" "" sup)
     ("Bold" "BOLD" "" bold)
diff --git a/demoisa/demoisa.el b/demoisa/demoisa.el
index 70886a85..45c712e7 100644
--- a/demoisa/demoisa.el
+++ b/demoisa/demoisa.el
@@ -1,6 +1,6 @@
 ;; demoisa.el Example Proof General instance for Isabelle
 ;;
-;; Copyright (C) 1999 LFCS Edinburgh. 
+;; Copyright (C) 1999 LFCS Edinburgh.
 ;;
 ;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
 ;;
@@ -19,8 +19,8 @@
 ;;
 ;; From this it loads this file "demoisa/demoisa.el" whenever
 ;; a .ML file is visited, and sets the mode to `demoisa-mode'
-;; (defined below).  
-;; 
+;; (defined below).
+;;
 ;; I've called this instance "Isabelle Demo Proof General" just to
 ;; avoid confusion with the real "Isabelle Proof General" in case the
 ;; demo gets loaded by accident.
@@ -46,7 +46,7 @@
 ;;			   (constants, but may be nice to tweak)
 ;;
 ;; The first group appears in the menu
-;;   ProofGeneral -> Customize -> Isabelledemo 
+;;   ProofGeneral -> Customize -> Isabelledemo
 ;; The second group appears in the menu:
 ;;   ProofGeneral -> Internals -> Isabelledemo config
 ;;
@@ -100,7 +100,7 @@
    proof-shell-proof-completed-regexp   "^No subgoals!"
    proof-shell-eager-annotation-start   "^\\[opening \\|^###\\|^Reading"
    proof-shell-init-cmd  ; define a utility function, in a lib somewhere?
-   "fun pg_repeat f 0 = () 
+   "fun pg_repeat f 0 = ()
       | pg_repeat f n = (f(); pg_repeat f (n-1));"
    proof-shell-quit-cmd			"quit();"))
 
diff --git a/etc/isar/AThousandTheorems.thy b/etc/isar/AThousandTheorems.thy
index 68f3c474..233dc1ed 100644
--- a/etc/isar/AThousandTheorems.thy
+++ b/etc/isar/AThousandTheorems.thy
@@ -1010,3 +1010,6 @@ ML {* Output.warning (#message (end_timing start)); *}
 (* ELISP: -- (message "Time taken: %f seconds" (time-to-seconds (time-since start))) -- *)
 
 end
+
+
+
diff --git a/hol98/hol98.el b/hol98/hol98.el
index 653bbcb8..57172649 100644
--- a/hol98/hol98.el
+++ b/hol98/hol98.el
@@ -1,6 +1,6 @@
 ;; hol98.el   Basic Proof General instance for HOL 98
 ;;
-;; Copyright (C) 2000 LFCS Edinburgh. 
+;; Copyright (C) 2000 LFCS Edinburgh.
 ;;
 ;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
 ;;
@@ -14,7 +14,7 @@
 (require 'proof-easy-config)            ; easy configure mechanism
 (require 'proof-syntax)			; functions for making regexps
 
-(proof-easy-config  'hol98 "HOL" 
+(proof-easy-config  'hol98 "HOL"
  proof-prog-name		 "hol.unquote"
  proof-terminal-char             ?\;
  proof-script-comment-start             "(*"
@@ -34,26 +34,26 @@
  proof-shell-cd-cmd              "FileSys.chDir \"%s\""
  proof-shell-filename-escapes    '(("\\\\" . "\\\\") ("\""   . "\\\""))
  proof-shell-interrupt-regexp    "Interrupted"
- proof-shell-start-goals-regexp  
- (proof-regexp-alt "Proof manager status" 
-		   "OK.." 
+ proof-shell-start-goals-regexp
+ (proof-regexp-alt "Proof manager status"
+		   "OK.."
 		   "val it =\n")
- proof-shell-end-goals-regexp    
+ proof-shell-end-goals-regexp
  (proof-regexp-alt "^[ \t]*: GoalstackPure.goalstack"
 		   "^[ \t]*: GoalstackPure.proofs")
  proof-shell-quit-cmd            "quit();"
- proof-assistant-home-page       
+ proof-assistant-home-page
  "http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html"
- proof-shell-annotated-prompt-regexp 
+ proof-shell-annotated-prompt-regexp
  "^- "
  ;; This one is nice but less reliable, I think.
  ;; "\\(> val it = () : unit\n\\)?- "
  proof-shell-error-regexp "^! "
- proof-shell-init-cmd		  
+ proof-shell-init-cmd
  "Help.displayLines:=3000;
   fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));
   fun pg_top_thm_and_drop () = let val t = top_thm(); in (drop(); t) end;"
- ;; FIXME: add optional help topic parameter to help command. 
+ ;; FIXME: add optional help topic parameter to help command.
  proof-info-command		    "help \"hol\""
  proof-shell-proof-completed-regexp "Initial goal proved"
  ;; FIXME: next one needs setting so that "urgent" messages are displayed
@@ -67,27 +67,27 @@
  ;; (on Linux, presumably on Solaris too).
  proof-shell-process-connection-type t
 
- ;; 
+ ;;
  ;; Syntax table entries for proof scripts
  ;;
  proof-script-syntax-table-entries
  '(?\` "\""
-   ?\$ "."   
-   ?\/ "."   
-   ?\\ "."   
-   ?+  "."   
-   ?-  "."   
-   ?=  "."   
-   ?%  "."   
-   ?<  "."   
-   ?>  "."   
-   ?\& "."   
-   ?.  "w"   
-   ?_  "w"   
-   ?\' "w"   
-   ?\| "."   
+   ?\$ "."
+   ?\/ "."
+   ?\\ "."
+   ?+  "."
+   ?-  "."
+   ?=  "."
+   ?%  "."
+   ?<  "."
+   ?>  "."
+   ?\& "."
+   ?.  "w"
+   ?_  "w"
+   ?\' "w"
+   ?\| "."
    ?\* ". 23"
-   ?\( "()1" 
+   ?\( "()1"
    ?\) ")(4")
 
  ;;
@@ -104,11 +104,11 @@
 		   "Induct" "Cases" "Cases_on" "Induct_on"
 		   "std_ss" "arith_ss" "list_ss"
 		   "define_type")
- hol98-rules	 '("ASSUME" "REFL" "BETA_CONV" "SUBST" 
+ hol98-rules	 '("ASSUME" "REFL" "BETA_CONV" "SUBST"
 		   "ABS" "INST_TYPE" "DISCH" "MP"
 		   "T_DEF" "FORALL_DEF" "AND_DEF" "OR_DEF" "F_DEF"
 		   "NOT_DEF" "EXISTS_UNIQUE_DEF" "BOOL_CASES_AX"
-		   "IMP_ANTISYM_AX" "ETA_AX" "SELECT_AX" "ONE_ONE_DEF" 
+		   "IMP_ANTISYM_AX" "ETA_AX" "SELECT_AX" "ONE_ONE_DEF"
 		   "ONTO_DEF" "INFINITY_AX" "LET_DEF" "COND_DEF" "ARB_DEF")
  hol98-tactics   '("ACCEPT_TAC" "ASSUME_TAC" "GEN_TAC"
 		   "CONJ_TAC" "DISCH_TAC" "STRIP_TAC"
@@ -122,7 +122,7 @@
  hol98-tacticals '("ORELSE" "FIRST" "CHANGED_TAC" "THEN"
 		   "THENL" "EVERY" "REPEAT"
 		   "MAP_EVERY")
- proof-script-font-lock-keywords	
+ proof-script-font-lock-keywords
  (list
   (cons (proof-ids-to-regexp hol98-keywords) 'font-lock-keyword-face)
   (cons (proof-ids-to-regexp hol98-tactics) 'font-lock-keyword-face)
@@ -134,7 +134,7 @@
  ;;
  proof-goals-font-lock-keywords
  (list
-  (cons (proof-ids-to-regexp '("Proof manager status" 
+  (cons (proof-ids-to-regexp '("Proof manager status"
 			       "proof" "Incomplete"
 			       "Initial goal proved"
 			       "Initial goal"
@@ -147,7 +147,7 @@
   (cons ": GoalstackPure.proofs"    'proof-boring-face)
   (cons ": Thm.thm"		    'proof-boring-face)
   (cons "val it ="		    'proof-boring-face))
- 
+
  ;; End of easy config.
  )
 
diff --git a/isar/Example.thy b/isar/Example.thy
index 34c840fe..720e5480 100644
--- a/isar/Example.thy
+++ b/isar/Example.thy
@@ -4,6 +4,7 @@
       $Id$
 *)
 
+
 theory Example imports Main begin
 
 text {* Proper proof text -- \textit{naive version}. *}
@@ -28,4 +29,5 @@ theorem  "A & B --> B & A"
   apply assumption
 done
 
+
 end
diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el
index e206822a..a370654e 100644
--- a/isar/isabelle-system.el
+++ b/isar/isabelle-system.el
@@ -43,7 +43,7 @@
       (getenv "ISABELLE_TOOL")
       (proof-locate-executable "isabelle" nil
 			       (list
-				;; support default unpack in home dir situation 
+				;; support default unpack in home dir situation
 				(concat (getenv "HOME") "/Isabelle/bin/")))
       "path_to_isabelle_is_unknown")
   "Command to invoke the main Isabelle wrapper 'isabelle'.
@@ -61,12 +61,12 @@ working."
   "Make sure `isa-isabelle-command' points to a valid executable.
 If it does not, or if prefix arg supplied, prompt the user for
 the proper setting.  If `proof-rsh-command' is set, leave this
-unverified.  Otherwise, returns non-nil if isa-isabelle-command 
+unverified.  Otherwise, returns non-nil if isa-isabelle-command
 is surely an executable with full path."
   (interactive "p")
   (when (and (not noninteractive)
 	     (not proof-rsh-command)
-	     (or force 
+	     (or force
 		 isabelle-not-found
 		 (not (file-executable-p isa-isabelle-command))))
     (setq isa-isabelle-command
@@ -155,17 +155,17 @@ at the top of your theory file, like this:
 
 (defvar isabelle-chosen-logic-prev nil
   "Value of `isabelle-chosen-logic' on last call of `isabelle-set-prog-name'.")
-  
+
 (defun isabelle-hack-local-variables-function ()
   "Hook function for `hack-local-variables-hook'."
   (if (and isabelle-chosen-logic
-	   (not (equal isabelle-chosen-logic 
+	   (not (equal isabelle-chosen-logic
 		       isabelle-chosen-logic-prev))
 	   (proof-shell-live-buffer))
       (message "Warning: chosen logic %s does not match running Isabelle instance"
 	       isabelle-chosen-logic)))
 
-(add-hook 'hack-local-variables-hook 
+(add-hook 'hack-local-variables-hook
 	  'isabelle-hack-local-variables-function)
 
 (defun isabelle-set-prog-name (&optional filename)
@@ -177,9 +177,9 @@ This function sets `isabelle-prog-name' and `proof-prog-name'."
       ;; is set in current Isabelle settings environment.
       ((isabelle (or
 		  isabelle-program-name-override  ; override in Emacs
-		  (getenv "ISABELLE_PROCESS")	  ; command line override 
+		  (getenv "ISABELLE_PROCESS")	  ; command line override
 		  (isa-getenv "ISABELLE_PROCESS") ; choose to match isabelle
-		  "isabelle-process"))		  ; to 
+		  "isabelle-process"))		  ; to
        (isabelle-opts (getenv "ISABELLE_OPTIONS"))
        (opts (concat " -PI"  ;; Proof General + Isar
 	      (if proof-shell-unicode " -m PGASCII" "")
@@ -218,7 +218,7 @@ This function sets `isabelle-prog-name' and `proof-prog-name'."
       (apply 'start-process
 	     "isa-view-doc" nil
 	     (append (split-string
-		      isa-isabelle-command) 
+		      isa-isabelle-command)
 		     (list "doc" docname)))))
 
 (defun isa-tool-list-docs ()
@@ -257,7 +257,7 @@ for you, you should disable this behaviour."
   :type 'boolean
   :group 'isabelle)
 
-(defvar isabelle-docs-menu 
+(defvar isabelle-docs-menu
   (let ((vc '(lambda (docdes)
 	       (vector (car (cdr docdes))
 		       (list 'isa-view-doc (car docdes)) t))))
@@ -311,7 +311,7 @@ for you, you should disable this behaviour."
   "Update logics menu."
   (and (current-local-map)
        (keymapp (lookup-key (current-local-map)
- 			    (vector 'menu-bar (intern proof-assistant))))
+			    (vector 'menu-bar (intern proof-assistant))))
        (isabelle-logics-menu-refresh)))
 
 (add-hook 'menu-bar-update-hook 'isabelle-menu-bar-update-logics)
diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el
index 8d6aae95..da83aabb 100644
--- a/isar/isar-autotest.el
+++ b/isar/isar-autotest.el
@@ -30,8 +30,6 @@
   (pg-autotest assert-unprocessed "etc/isar/multiple/C.thy")
   (pg-autotest assert-processed   "etc/isar/multiple/A.thy")
 
-  
+
   (pg-autotest-quit-prover)
   (pg-autotest-finished))
-
-
diff --git a/isar/isar-find-theorems.el b/isar/isar-find-theorems.el
index 2e007e78..0d40f392 100644
--- a/isar/isar-find-theorems.el
+++ b/isar/isar-find-theorems.el
@@ -122,7 +122,7 @@
   (widget-insert
     (concat "\n  "
       (if (fboundp 'propertize)
-        (propertize "Find Theorems" 'face 'bold)
+	(propertize "Find Theorems" 'face 'bold)
       "Find Theorems")
       "\n\n"))
 
@@ -190,7 +190,7 @@
   (widget-create 'push-button
     :help-echo "Click <mouse-2> for help."
     :notify (lambda (&rest ignore) (isar-find-theorems-create-help))
-    "?")  
+    "?")
 
   ;; num
   (widget-insert "\n\n  Number of results:      ")
@@ -210,15 +210,15 @@
     :help-echo "Click <mouse-2> to submit this form."
     :notify (lambda (&rest ignore)
       (let ((num     (widget-value isar-find-theorems-widget-number))
-            (pattern (widget-value isar-find-theorems-widget-pattern))
-            (intro   (widget-value isar-find-theorems-widget-intro))
-            (elim    (widget-value isar-find-theorems-widget-elim))
-            (dest    (widget-value isar-find-theorems-widget-dest))
-            (name    (widget-value isar-find-theorems-widget-name))
-            (simp    (widget-value isar-find-theorems-widget-simp)))
+	    (pattern (widget-value isar-find-theorems-widget-pattern))
+	    (intro   (widget-value isar-find-theorems-widget-intro))
+	    (elim    (widget-value isar-find-theorems-widget-elim))
+	    (dest    (widget-value isar-find-theorems-widget-dest))
+	    (name    (widget-value isar-find-theorems-widget-name))
+	    (simp    (widget-value isar-find-theorems-widget-simp)))
       (kill-buffer "*Find Theorems*")
       (isar-find-theorems-submit-searchform
-        num pattern intro elim dest name simp)))
+	num pattern intro elim dest name simp)))
     "Find")
 
   ;; Reset form
@@ -228,7 +228,7 @@
     :notify (lambda (&rest ignore)
       (kill-buffer "*Find Theorems*")
       (isar-find-theorems-create-searchform
-        "" "" "none" "none" "none" "" ""))
+	"" "" "none" "none" "none" "" ""))
     "Reset Form")
     (widget-insert "\n")
 
@@ -236,7 +236,7 @@
   (if errmsg
     (widget-insert (concat "\n    "
       (if (fboundp 'propertize)
-        (propertize (concat errmsg "\n    See help for details.") 'face 'bold)
+	(propertize (concat errmsg "\n    See help for details.") 'face 'bold)
       (concat errmsg "\n    See help for details."))
       "\n")))
 
@@ -351,7 +351,7 @@
   (setq searchstring (format "find_theorems %s"
     (mapconcat 'identity
       (isar-find-theorems-filter-empty
-        (list num_ pattern_ intro_ elim_ dest_ name_ simp_))
+	(list num_ pattern_ intro_ elim_ dest_ name_ simp_))
       " ")))
 
   ;; note that proof-find-theorems with an argument provided
@@ -391,30 +391,30 @@ escaped by double-quotes."
     ;;       well.
     (if (equal (elt criteria-string 0) ?-)
       (progn
-        (setq tokens (cons "-" tokens))
-        (setq criteria-string (substring criteria-string 1)))
+	(setq tokens (cons "-" tokens))
+	(setq criteria-string (substring criteria-string 1)))
 
     ;; " starts a token: search for the next ", regard as one token
     ;; Note: This is still a bit weird, as it does not require the
     ;;       closing double-quotes to be followed by a space. Oh well.
     (if (equal (elt criteria-string 0) ?\")
       (let ((i 1))
-        (while (and (< i (length criteria-string))
-                    (not (equal (elt criteria-string i) ?\")))
-          (setq i (1+ i)))
-        (if (equal i (length criteria-string))
-          (setq errmsg "missing closing double-quotes.")
-        (setq i (1+ i))
-        (setq tokens (cons (substring criteria-string 0 i) tokens))
-        (setq criteria-string (substring criteria-string i))))
+	(while (and (< i (length criteria-string))
+		    (not (equal (elt criteria-string i) ?\")))
+	  (setq i (1+ i)))
+	(if (equal i (length criteria-string))
+	  (setq errmsg "missing closing double-quotes.")
+	(setq i (1+ i))
+	(setq tokens (cons (substring criteria-string 0 i) tokens))
+	(setq criteria-string (substring criteria-string i))))
 
     ;; everything else: search for the next space, regard as one token
     ;; Note: This is still a bit weird, as it scans over double-quotes.
     ;;       Oh well.
     (let ((i 1))
       (while (and (< i (length criteria-string))
-                  (not (equal (elt criteria-string i) ?\ )))
-        (setq i (1+ i)))
+		  (not (equal (elt criteria-string i) ?\ )))
+	(setq i (1+ i)))
       (setq tokens (cons (substring criteria-string 0 i) tokens))
       (setq criteria-string (substring criteria-string i)))
     )))
@@ -433,13 +433,13 @@ escaped by double-quotes."
     (let ((token (car tokens)))
     (if (equal token "-")
       (if negated
-        (setq errmsg "- may not be followed by another -.")
+	(setq errmsg "- may not be followed by another -.")
       (setq negated t)
       (setq tokens (cdr tokens)))
     (setq strings (cons
       (concat (if negated "-" "") option-string
-        ;; wrap token in double-quotes if necessary
-        (if (equal (elt token 0) ?\") token (concat "\"" token "\"")))
+	;; wrap token in double-quotes if necessary
+	(if (equal (elt token 0) ?\") token (concat "\"" token "\"")))
       strings))
     (setq negated nil)
     (setq tokens (cdr tokens))))
diff --git a/isar/isar-keywords.el b/isar/isar-keywords.el
index d42c682e..c7e0c7c2 100644
--- a/isar/isar-keywords.el
+++ b/isar/isar-keywords.el
@@ -1,5 +1,5 @@
 ;; NB: this copy of isar-keywords is NOT usually the one that is loaded.
-;; It will only be used if Isabelle is not properly installed and the 
+;; It will only be used if Isabelle is not properly installed and the
 ;; isatool command cannot be found.  It is needed as a fallback in this case.
 ;;
 ;; =================================================================
diff --git a/isar/isar-mmm.el b/isar/isar-mmm.el
index a36b484e..3ecc9f7b 100644
--- a/isar/isar-mmm.el
+++ b/isar/isar-mmm.el
@@ -5,11 +5,11 @@
 ;; Licence:	 GPL
 ;;
 ;; $Id$
-;; 
+;;
 ;; Presently, we deal with several cases of {* text *}.
 ;; It's not a good idea to do too much, since searching for the
 ;; regions and fontifying them is slow.
-;; 
+;;
 ;; TODO:
 ;;  --- fontification for antiquotations has been lost, could
 ;;      add that into LaTeX mode somehow.
@@ -21,22 +21,22 @@
 (require 'mmm-auto)
 (require 'proof-syntax)			; proof-ids-to-regexp
 
-(defconst isar-start-latex-regexp 
+(defconst isar-start-latex-regexp
   (concat
-   "\\(" 
-   (proof-ids-to-regexp 
+   "\\("
+   (proof-ids-to-regexp
     ;; Perhaps section is too much?  The fontification is nice but
     ;; section headers are a bit short to use LaTeX mode in.
-    (list "text" "header" ".*section"))  
+    (list "text" "header" ".*section"))
    ;; Next one is nice but hammers font lock a bit too much
    ;; if there are lots of -- {* short comments *}
    ;; "\\|\-\-" ;; NB: doesn't work with \\<--\\>
    "\\)[ \t]+{\\*"))
 
-(defconst isar-start-sml-regexp 
+(defconst isar-start-sml-regexp
   (concat
-   "\\(" 
-   (proof-ids-to-regexp 
+   "\\("
+   (proof-ids-to-regexp
     (list "ML" "ML_command" "ML_setup" "typed_print_translation"))
    "\\)[ \t]+{\\*"))
 
@@ -46,7 +46,7 @@
  `((isar-latex
    :submode LaTeX-mode
    :face mmm-comment-submode-face
-   :front ,isar-start-latex-regexp 
+   :front ,isar-start-latex-regexp
    :back  "\\*}"
    :insert ((?t isar-text nil @ "text {*" @ " " _ " " @ "*}" @)
 	    (?t isar-text_raw nil @ "text_raw {*" @ " " _ " " @ "*}" @)
@@ -62,7 +62,7 @@
 	    (?c isar-ML-command nil @ "ML_command {*" @ " " _ " " @ "*}" @)
 	    (?m isar-ML nil @ "ML {*" @ " " _ " " @ "*}" @)
 	    (?p isar-print-trans nil @ "typed_print_translation {*" @ " " _ " " @ "*}" @)))))
-	    
+
 
 (provide 'isar-mmm)
 
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 1af9e545..2e024eac 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -42,7 +42,7 @@ This list is in the right format for proof-easy-config.")
 (defconst isar-script-syntax-table-alist
   ;; NB: this is used for imenu.  Probably only need word syntax
   (let ((syn isar-script-syntax-table-entries)
-        al)
+	al)
     (while syn
       (setq al (cons (cons (char-to-string (car syn)) (cadr syn)) al))
       (setq syn (cddr syn)))
@@ -78,74 +78,74 @@ This list is in the right format for proof-easy-config.")
 (defconst isar-keywords-theory-enclose
   (append isar-keywords-theory-begin
 	  isar-keywords-theory-switch
-          isar-keywords-theory-end))
+	  isar-keywords-theory-end))
 
 (defconst isar-keywords-theory
   (append isar-keywords-theory-heading
-          isar-keywords-theory-decl
-          isar-keywords-theory-goal))
+	  isar-keywords-theory-decl
+	  isar-keywords-theory-goal))
 
 (defconst isar-keywords-save
   (append isar-keywords-qed
-          isar-keywords-qed-block
-          isar-keywords-qed-global))
+	  isar-keywords-qed-block
+	  isar-keywords-qed-global))
 
 (defconst isar-keywords-proof-enclose
   (append isar-keywords-proof-block
-          isar-keywords-proof-open
-          isar-keywords-proof-close
-          isar-keywords-qed-block))
+	  isar-keywords-proof-open
+	  isar-keywords-proof-close
+	  isar-keywords-qed-block))
 
 (defconst isar-keywords-proof
   (append isar-keywords-proof-heading
-          isar-keywords-proof-goal
-          isar-keywords-proof-chain
-          isar-keywords-proof-decl
-          isar-keywords-qed))
+	  isar-keywords-proof-goal
+	  isar-keywords-proof-chain
+	  isar-keywords-proof-decl
+	  isar-keywords-qed))
 
 (defconst isar-keywords-proof-context
   (append isar-keywords-proof-asm
-          isar-keywords-proof-asm-goal))
+	  isar-keywords-proof-asm-goal))
 
 (defconst isar-keywords-local-goal
   (append isar-keywords-proof-goal
-          isar-keywords-proof-asm-goal))
+	  isar-keywords-proof-asm-goal))
 
 (defconst isar-keywords-proper
   (append isar-keywords-theory
-          isar-keywords-proof-enclose
-          isar-keywords-proof))
+	  isar-keywords-proof-enclose
+	  isar-keywords-proof))
 
 (defconst isar-keywords-improper
   (append isar-keywords-theory-script
-          isar-keywords-proof-script
-          isar-keywords-qed-global))
+	  isar-keywords-proof-script
+	  isar-keywords-qed-global))
 
 (defconst isar-keywords-outline
   isar-keywords-theory-heading)
 
 (defconst isar-keywords-fume
   (append isar-keywords-theory-begin
-          isar-keywords-theory-heading
-          isar-keywords-theory-decl
-          isar-keywords-theory-script
-          isar-keywords-theory-goal))
+	  isar-keywords-theory-heading
+	  isar-keywords-theory-decl
+	  isar-keywords-theory-script
+	  isar-keywords-theory-goal))
 
 (defconst isar-keywords-indent-open
   (append isar-keywords-theory-goal
-          isar-keywords-proof-goal
-          isar-keywords-proof-asm-goal
-          isar-keywords-proof-open))
+	  isar-keywords-proof-goal
+	  isar-keywords-proof-asm-goal
+	  isar-keywords-proof-open))
 
 (defconst isar-keywords-indent-close
   (append isar-keywords-save
-          isar-keywords-proof-close))
+	  isar-keywords-proof-close))
 
 (defconst isar-keywords-indent-enclose
   (append isar-keywords-proof-block
-          isar-keywords-proof-close
-          isar-keywords-qed-block
-          (list isar-keyword-begin)))
+	  isar-keywords-proof-close
+	  isar-keywords-qed-block
+	  (list isar-keyword-begin)))
 
 
 ;; ----- regular expressions
@@ -173,9 +173,9 @@ This list is in the right format for proof-easy-config.")
 (defun isar-ids-to-regexp (l)
   "Maps a non-empty list of tokens `l' to a regexp matching all elements"
   (let* ((special (remove-if-not (lambda (s) (string-match "{\\|}" s)) l))
-         (normal (remove-if (lambda (s) (string-match "{\\|}" s)) l))
-         (s-reg (isar-regexp-simple-alt special))
-         (n-reg (concat "\\<\\(?:" (isar-regexp-simple-alt normal) "\\)\\>")))
+	 (normal (remove-if (lambda (s) (string-match "{\\|}" s)) l))
+	 (s-reg (isar-regexp-simple-alt special))
+	 (n-reg (concat "\\<\\(?:" (isar-regexp-simple-alt normal) "\\)\\>")))
     (cond
      ((null special) n-reg)
      ((null normal) s-reg)
@@ -258,12 +258,12 @@ matches contents of quotes for quoted identifiers.")
 		     (looking-at "[ \t\n]*--")
 		     'comment))))
       sc)))
-	  
+
 
 ;; antiquotations
 
-(defconst isar-antiq-regexp 
-  (concat "@{\\(?:[^\"{}]\\|" isar-string "\\)*}") 
+(defconst isar-antiq-regexp
+  (concat "@{\\(?:[^\"{}]\\|" isar-string "\\)*}")
   "Regexp matching Isabelle/Isar antiquotations.")
 
 ;; keyword nesting
@@ -277,10 +277,10 @@ matches contents of quotes for quoted identifiers.")
     (save-excursion
       (goto-char (point-min))
       (while (proof-re-search-forward isar-nesting-regexp limit t)
-        (cond
-         ((proof-buffer-syntactic-context))
-         ((equal (match-string 0) isar-keyword-begin) (incf nesting))
-         ((equal (match-string 0) isar-keyword-end) (decf nesting)))))
+	(cond
+	 ((proof-buffer-syntactic-context))
+	 ((equal (match-string 0) isar-keyword-begin) (incf nesting))
+	 ((equal (match-string 0) isar-keyword-end) (decf nesting)))))
     nesting))
 
 (defun isar-match-nesting (limit)
@@ -364,9 +364,9 @@ matches contents of quotes for quoted identifiers.")
    (cons isar-improper-regexp 'font-lock-reference-face)
    (cons isar-antiq-regexp '(0 'font-lock-variable-name-face t))))
 
-(put 'isar-goals-mode 
+(put 'isar-goals-mode
      'font-lock-extra-managed-props '(invisible sendback))
-(put 'isar-response-mode 
+(put 'isar-response-mode
      'font-lock-extra-managed-props '(invisible sendback))
 
 (defun isar-output-flkprops (start regexp end props)
@@ -381,31 +381,31 @@ matches contents of quotes for quoted identifiers.")
 (defvar isar-output-font-lock-keywords-1
   (list
    '("\^A[IJKLMNOPV]" (0 '(face nil invisible t) t))
-   (isar-output-flkprops 
-    "\^AW" "\\(?:[^\^A]\\|\^A[^X]\\)*" "\^AX" 
+   (isar-output-flkprops
+    "\^AW" "\\(?:[^\^A]\\|\^A[^X]\\)*" "\^AX"
     '(face (:underline t) mouse-face 'highlight sendback t))
 
-   (isar-output-flk "\^A0" 
-		    "\\(?:[^\^A]\\|\^A[^1]\\)*" "\^A1" 
+   (isar-output-flk "\^A0"
+		    "\\(?:[^\^A]\\|\^A[^1]\\)*" "\^A1"
 		    'proof-warning-face)
 
 ;; done generically at the moment:
 ;; (isar-output-flk "\^AM" "\\(?:[^\^A]\\|\^A[^N]\\)*" "\^AN" 'proof-error-face)
 
-   (isar-output-flk "\^AB" isar-long-id-stuff 
+   (isar-output-flk "\^AB" isar-long-id-stuff
 		    "\^AA" 'isabelle-class-name-face)
-   (isar-output-flk "\^AC" (concat "'" isar-id) 
+   (isar-output-flk "\^AC" (concat "'" isar-id)
 		    "\^AA" 'isabelle-tfree-name-face)
    (isar-output-flk "\^AD" (concat "\\??'" isar-idx)
 		    "\^AA" 'isabelle-tvar-name-face)
    (isar-output-flk "\^AE" isar-id "\^AA" 'isabelle-free-name-face)
    (isar-output-flk "\^AF" isar-id "\^AA" 'isabelle-bound-name-face)
-   (isar-output-flk "\^AG" (concat "\\??" isar-idx) 
+   (isar-output-flk "\^AG" (concat "\\??" isar-idx)
 		    "\^AA" 'isabelle-var-name-face)
    (isar-output-flk "\^AH" (concat "\\??" isar-idx)
 		    "\^AA" 'proof-declaration-name-face)
 
-   ;; may alternatively hide the spurious ASCII characters which 
+   ;; may alternatively hide the spurious ASCII characters which
    ;; aren't needed when working in colour (Isabelle printing switch
    ;; allows this for ?'s but not for 's):
    ; (isar-output-flk "\^AC'" isar-id "\^AA" 'isabelle-tfree-name-face)
@@ -468,8 +468,8 @@ matches contents of quotes for quoted identifiers.")
 
 (defconst isar-undo-commands
   (list
-   isar-linear-undo 
-   isar-undo 
+   isar-linear-undo
+   isar-undo
    "init_toplevel" "kill_thy"
    "undos_proof"
    "cannot_undo"))
@@ -478,7 +478,7 @@ matches contents of quotes for quoted identifiers.")
   (proof-anchor-regexp
    (isar-ids-to-regexp
     (append isar-keywords-theory-begin
-            isar-keywords-theory-switch))))
+	    isar-keywords-theory-switch))))
 
 (defconst isar-end-regexp
   (proof-anchor-regexp
@@ -504,20 +504,20 @@ matches contents of quotes for quoted identifiers.")
 
 (defconst isar-any-entity-regexp
   (concat "\\(?:" (isar-ids-to-regexp isar-keywords-fume) "\\)"
-          "\\(?:\\s-*(\\s-*in[^)]+)\\)?"
-          "\\(?:" isar-name-regexp "[[:=]\\)"))
+	  "\\(?:\\s-*(\\s-*in[^)]+)\\)?"
+	  "\\(?:" isar-name-regexp "[[:=]\\)"))
 
 (defconst isar-named-entity-regexp
   (concat "\\(" (isar-ids-to-regexp isar-keywords-fume) "\\)"
-          "\\(?:\\s-*(\\s-*in[^)]+)\\)?"
-          isar-name-regexp "[[:=]" ))
+	  "\\(?:\\s-*(\\s-*in[^)]+)\\)?"
+	  isar-name-regexp "[[:=]" ))
 
 (defconst isar-unnamed-entity-regexp
   (concat "\\(" (isar-ids-to-regexp isar-keywords-fume) "\\)"))
 
 (defconst isar-next-entity-regexps
   (list isar-any-entity-regexp
-        (list isar-named-entity-regexp '(1 3))))
+	(list isar-named-entity-regexp '(1 3))))
 ;; da: I've removed unnamed entities, they clutter the menu
 ;; NB: to add back, need ? at end of isar-any-entity-regexp
 ;;      (list isar-unnamed-entity-regexp 1)))
@@ -525,12 +525,12 @@ matches contents of quotes for quoted identifiers.")
 
 (defconst isar-generic-expression
   (mapcar (lambda (kw)
-            (list (capitalize kw)
-                  (concat "\\<" kw "\\>"
-                          "\\(?:\\s-*(\\s-*in[^)]+)\\)?"
-                          isar-name-regexp "[[:=]")
-                  1))
-          isar-keywords-fume))
+	    (list (capitalize kw)
+		  (concat "\\<" kw "\\>"
+			  "\\(?:\\s-*(\\s-*in[^)]+)\\)?"
+			  isar-name-regexp "[[:=]")
+		  1))
+	  isar-keywords-fume))
 
 ;; ----- indentation
 
diff --git a/lclam/lclam.el b/lclam/lclam.el
index 5d5c180b..8bbfb00d 100644
--- a/lclam/lclam.el
+++ b/lclam/lclam.el
@@ -1,4 +1,4 @@
-;; File name:      lclam.el        
+;; File name:      lclam.el
 ;; Description:    Proof General instance for Lambda-CLAM
 ;; Author:         James Brotherston <jjb@dai.ed.ac.uk>
 ;; Last modified:  23 October 2001
@@ -6,7 +6,7 @@
 ;; $Id$
 
 (require 'proof)            ; load generic parts
-(require 'proof-syntax)     
+(require 'proof-syntax)
 
 ;;
 ;; =========== User settings for Lambda-CLAM ============
@@ -31,7 +31,7 @@
 
 (defun lclam-config ()
   "Configure Proof General scripting for Lambda-CLAM."
-  (setq 
+  (setq
    proof-terminal-char             ?\.
    proof-comment-start             "/*"
    proof-comment-end               "*/"
@@ -41,12 +41,12 @@
    proof-save-with-hole-regexp     nil
    proof-non-undoables-regexp      nil
    proof-undo-n-times-cmd          nil
-   proof-showproof-command         nil 
+   proof-showproof-command         nil
    proof-goal-command              "^pds_plan %s."
    proof-save-command              nil
    proof-kill-goal-command         nil
    proof-assistant-homepage        lclam-web-page
-   proof-auto-multiple-files       nil 
+   proof-auto-multiple-files       nil
    proof-prog-name		   lclam-prog-name
    proof-shell-process-connection-type t
    ))
@@ -54,7 +54,7 @@
 (defun lclam-shell-config ()
   "Configure Proof General shell for Lambda-CLAM"
   (setq
-   proof-shell-annotated-prompt-regexp "^lclam:" 
+   proof-shell-annotated-prompt-regexp "^lclam:"
    proof-shell-cd-cmd                  nil
    proof-shell-interrupt-regexp        nil
    proof-shell-error-regexp            nil
@@ -135,39 +135,39 @@
 (defvar thy-mode-map nil)
 
 (defun thy-add-menus ()
-  "Add Lambda-CLAM menu to current menu bar."  
-  (require 'proof-script)    
+  "Add Lambda-CLAM menu to current menu bar."
+  (require 'proof-script)
   (easy-menu-define thy-mode-pg-menu
-                    thy-mode-map
-                    "PG Menu for Lambda-CLAM Proof General"
-                    (cons proof-general-name
-                          (append
-                           (list
-                           ;; A couple from the toolbar that make sense here
-                           ;; (also in proof-universal-keys)
-                            ["Issue command" proof-minibuffer-cmd t]
-                            ["Interrupt prover" proof-interrupt-process t])
+		    thy-mode-map
+		    "PG Menu for Lambda-CLAM Proof General"
+		    (cons proof-general-name
+			  (append
+			   (list
+			   ;; A couple from the toolbar that make sense here
+			   ;; (also in proof-universal-keys)
+			    ["Issue command" proof-minibuffer-cmd t]
+			    ["Interrupt prover" proof-interrupt-process t])
 			   (list proof-buffer-menu)
-                           (list proof-help-menu))))
+			   (list proof-help-menu))))
 
   (easy-menu-define thy-mode-lclam-menu
-                    thy-mode-map
-                    "Menu for Lambda-CLAM Proof General, theory file mode."
-                    (cons "Theory"
-                          (list
-                           ["Next section" thy-goto-next-section t]
-                           ["Prev section" thy-goto-prev-section t]
-                           ["Insert template" thy-insert-template t]
+		    thy-mode-map
+		    "Menu for Lambda-CLAM Proof General, theory file mode."
+		    (cons "Theory"
+			  (list
+			   ["Next section" thy-goto-next-section t]
+			   ["Prev section" thy-goto-prev-section t]
+			   ["Insert template" thy-insert-template t]
 ; da: commented out this, function is incomplete
 ;                           ["Include definitions" match-and-assert-defs
 ;                            :active (proof-locked-region-empty-p)]
-                           ["Process theory" process-thy-file
-                            :active (proof-locked-region-empty-p)]
+			   ["Process theory" process-thy-file
+			    :active (proof-locked-region-empty-p)]
 ; da: commented out this, there's no retract function provided
 ;                           ["Retract theory" isa-retract-thy-file
 ;                            :active (proof-locked-region-full-p)]
-                           ["Next error" proof-next-error t]
-                           ["Switch to script" thy-find-other-file t])))
+			   ["Next error" proof-next-error t]
+			   ["Switch to script" thy-find-other-file t])))
 
   (easy-menu-add thy-mode-pg-menu thy-mode-map)
   (easy-menu-add thy-mode-lclam-menu thy-mode-map)
diff --git a/lego/lego-syntax.el b/lego/lego-syntax.el
index 5cf7867a..44a17ade 100644
--- a/lego/lego-syntax.el
+++ b/lego/lego-syntax.el
@@ -1,5 +1,5 @@
 ;; lego-syntax.el Syntax of LEGO
-;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
+;; Copyright (C) 1994 - 1998 LFCS Edinburgh.
 ;; Author: Thomas Kleymann and Dilip Sequeira
 ;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Maintainer: Paul Callaghan <P.C.Callaghan@durham.ac.uk>
@@ -22,8 +22,8 @@
 	    "Cut" "Discharge" "DischargeKeep"
 	    "echo" "exE" "exI" "Expand" "ExpAll"
 	    "ExportState" "Equiv" "For" "Freeze" "Hnf" "Immed"
-	    "impE" "impI" "Induction" "Inductive" 
-	    "Invert" "Init" "intros" "Intros" "Module" "Next" 
+	    "impE" "impI" "Induction" "Inductive"
+	    "Invert" "Init" "intros" "Intros" "Module" "Next"
 	    "Normal" "notE" "notI" "orE" "orIL" "orIR" "qnify" "Qnify"
 	    "Qrepl" "Record" "Refine" "Repeat" "Try" "Unfreeze"))
   "Subset of LEGO keywords and tacticals which are terminated by a \?;")
@@ -37,7 +37,7 @@
 
 ;; ----- regular expressions for font-lock
 (defconst lego-error-regexp "^\\(cannot assume\\|Error\\|Lego parser\\)"
-  "A regular expression indicating that the LEGO process has identified an error.") 
+  "A regular expression indicating that the LEGO process has identified an error.")
 
 (defvar lego-id proof-id)
 
@@ -74,7 +74,7 @@
      ; Pi and Sigma binders
      (list (concat "[{<]\\s *\\(" lego-ids "\\)") 1
 	   'proof-declaration-name-face)
-   
+
      ;; Kinds
      (cons (concat "\\<Prop\\>\\|\\<Type\\s *\\(("
 		   lego-id ")\\)?") 'font-lock-type-face)
@@ -89,7 +89,7 @@
 (defconst lego-goal-with-hole-regexp
   (concat "\\(" (proof-ids-to-regexp lego-keywords-goal) "\\)\\s-+\\([^(){},:]+\\)")
   "Regular expression which matches an entry in `lego-keywords-goal'
-  and the name of the goal.") 
+  and the name of the goal.")
 
 (defconst lego-save-with-hole-regexp
   (concat "\\(" (proof-ids-to-regexp lego-keywords-save) "\\)\\s-+\\([^;]+\\)")
@@ -106,7 +106,7 @@
      (list lego-save-with-hole-regexp 2 'font-lock-function-name-face)
      ;; Remove spurious variable and function faces on commas.
      '(proof-zap-commas))))
-     
+
 (defun lego-init-syntax-table ()
   "Set appropriate values for syntax table in current buffer."
 
diff --git a/pgshell/pgshell.el b/pgshell/pgshell.el
index 665c63d1..bdf5c0e3 100644
--- a/pgshell/pgshell.el
+++ b/pgshell/pgshell.el
@@ -10,11 +10,11 @@
 ;; management, and nothing to do with theorem proving really!
 ;;
 ;; To use this instance of PG, visit a file with the ".pgsh" extension.
-;; 
+;;
 ;; Feedback welcome.
 
 
-(require 'proof-easy-config)           
+(require 'proof-easy-config)
 (require 'proof-syntax)
 
 (proof-easy-config 'pgshell "PG-Shell"
@@ -27,7 +27,7 @@
  proof-script-fly-past-comments  t	        ;; nice for single-line
 
  ;; Syntax table gets font-locking and editing features for comments.
- ;; see Elisp documentation of `modify-syntax-entry' 
+ ;; see Elisp documentation of `modify-syntax-entry'
  proof-script-syntax-table-entries '(?\# "<" ?\n ">")
 
  ;; next setting is just to prevent warning
diff --git a/plastic/plastic-syntax.el b/plastic/plastic-syntax.el
index 6c71aa34..c259a3b7 100644
--- a/plastic/plastic-syntax.el
+++ b/plastic/plastic-syntax.el
@@ -5,7 +5,7 @@
 
 ;; adapted from the following, by Paul Callaghan
 ;; ;; lego-syntax.el Syntax of LEGO
-;; ;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
+;; ;; Copyright (C) 1994 - 1998 LFCS Edinburgh.
 ;; ;; Author: Thomas Kleymann and Dilip Sequeira
 ;; ;; Maintainer: Paul Callaghan <P.C.Callaghan@durham.ac.uk>
 ;; ;; lego-syntax.el,v 2.10 1998/11/06 16:18:55 tms Exp
@@ -25,10 +25,10 @@
 	    "Cut" "Discharge" "DischargeKeep"
 	    "echo" "exE" "exI" "Expand" "ExpAll"
 	    "ExportState" "Equiv" "For" "Freeze" "Hnf" "Immed"
-	    "impE" "impI" "Induction" "Inductive" 
-	    "Invert" "Init" "intros" "Intros" "Module" "Next" 
+	    "impE" "impI" "Induction" "Inductive"
+	    "Invert" "Init" "intros" "Intros" "Module" "Next"
 	    "Normal" "notE" "notI" "orE" "orIL" "orIR" "qnify" "Qnify"
-	    "Qrepl" "Record" "Refine" "Repeat" "Return" "ReturnAll" 
+	    "Qrepl" "Record" "Refine" "Repeat" "Return" "ReturnAll"
 	    "Try" "Unfreeze"))
   "Subset of Plastic keywords and tacticals which are terminated by a \?;")
 
@@ -41,7 +41,7 @@
 
 ;; ----- regular expressions for font-lock
 (defconst plastic-error-regexp "^\\(FAIL\\)"
-  "A regular expression indicating that the Plastic process has identified an error.") 
+  "A regular expression indicating that the Plastic process has identified an error.")
 
 (defvar plastic-id proof-id)
 
@@ -78,7 +78,7 @@
      ; Pi and Sigma binders
      (list (concat "[{<]\\s *\\(" plastic-ids "\\)") 1
 	   'proof-declaration-name-face)
-   
+
      ;; Kinds
      (cons (concat "\\<Prop\\>\\|\\<Type\\s *\\(("
 		   plastic-id ")\\)?") 'font-lock-type-face))
@@ -89,7 +89,7 @@
 (defconst plastic-goal-with-hole-regexp
   (concat "\\(" (proof-ids-to-regexp plastic-keywords-goal) "\\)\\s-+\\([^:]+\\)")
   "Regular expression which matches an entry in `plastic-keywords-goal'
-  and the name of the goal.") 
+  and the name of the goal.")
 
 (defconst plastic-save-with-hole-regexp
   (concat "\\(" (proof-ids-to-regexp plastic-keywords-save) "\\)\\s-+\\([^;]+\\)")
@@ -107,13 +107,13 @@
 
 (defun plastic-init-syntax-table ()
   "Set appropriate values for syntax table in current buffer."
- 
+
   (modify-syntax-entry ?_ "_")
   (modify-syntax-entry ?\' "_")
   (modify-syntax-entry ?\| ".")
   (modify-syntax-entry ?\* ". 23")
   (modify-syntax-entry ?\( "()1")
   (modify-syntax-entry ?\) ")(4"))
- 
-     
+
+
 (provide 'plastic-syntax)
diff --git a/plastic/plastic.el b/plastic/plastic.el
index 8fc134ed..a6939f41 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -6,7 +6,7 @@
 
 ;; NOTES:
 ;;	remember to prefix all potential cmds with plastic-lit-string
-;;	alternative is to fix the filtering 
+;;	alternative is to fix the filtering
 
 
 (require 'proof)
@@ -31,8 +31,8 @@
   :group 'plastic)
 
 (eval-and-compile
-(defvar plastic-lit-string 
-  ">" 
+(defvar plastic-lit-string
+  ">"
   "*Prefix of literate lines. Set to empty string to get non-literate mode"))
 
 (defcustom plastic-help-menu-list
@@ -47,7 +47,7 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;; Configuration of Generic Proof Package ;;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Users should not need to change this. 
+;; Users should not need to change this.
 
 (defvar plastic-shell-process-output
   '((lambda (cmd string) (proof-string-match "^Module" cmd)) .
@@ -57,8 +57,8 @@
 	    (cons 'insert "\n\nImports done!"))))
   "Acknowledge end of processing import declarations.")
 
-(defconst plastic-process-config 
-  (concat plastic-lit-string 
+(defconst plastic-process-config
+  (concat plastic-lit-string
 	  " &S ECHO No PrettyPrinting configuration implemented;\n")
   "Command to enable pretty printing of the Plastic process.
    Proof-General annotations triggered by a cmd-line opt
@@ -66,7 +66,7 @@
 
 (defconst plastic-pretty-set-width "&S ECHO no PrettyWidth ;\n"
   "Command to adjust the linewidth for pretty printing of the Plastic
-  process.") 
+  process.")
 
 (defconst plastic-interrupt-regexp "Interrupt.."
   "Regexp corresponding to an interrupt")
@@ -84,7 +84,7 @@
   "The WWW address for the latest Plastic release."
   :type 'string
   :group 'plastic)
-	  
+
 (defcustom plastic-www-refcard
   plastic-www-home-page
   "URL for the Plastic reference card."
@@ -101,7 +101,7 @@
 
 ;; ----- plastic-shell configuration options
 
-(defcustom plastic-base 
+(defcustom plastic-base
   "/usr/local/plastic"
   ;; da: was
   ;; "PLASTIC_BASE:TO_BE_CUSTOMISED"
@@ -109,21 +109,21 @@
   :type 'string
   :group 'plastic)
 
-(defvar plastic-prog-name 
+(defvar plastic-prog-name
   (concat plastic-base "/bin/plastic")
   "*Name of program to run as plastic.")
 
 (defun plastic-set-default-env-vars ()
   "defaults for the expected lib vars."
-  (cond 
+  (cond
     ((not (getenv "PLASTIC_LIB"))
 		(setenv "PLASTIC_LIB" (concat plastic-base "/lib"))
 		(setenv "PLASTIC_TEST" (concat plastic-base "/test"))
 	)))
 
-(defvar plastic-shell-cd 
+(defvar plastic-shell-cd
   (concat plastic-lit-string " &S ECHO no cd ;\n")
-  "*Command of the inferior process to change the directory.") 
+  "*Command of the inferior process to change the directory.")
 
 (defvar plastic-shell-abort-goal-regexp "KillRef: ok, not in proof state"
   "*Regular expression indicating that the proof of the current goal
@@ -137,9 +137,9 @@
 (defvar plastic-goal-command-regexp
   (concat "^" (proof-ids-to-regexp plastic-keywords-goal)))
 
-(defvar plastic-kill-goal-command 
+(defvar plastic-kill-goal-command
   (concat plastic-lit-string " &S ECHO KillRef not applicable;"))
-(defvar plastic-forget-id-command 
+(defvar plastic-forget-id-command
   (concat plastic-lit-string " &S Forget "))
 
 (defvar plastic-undoable-commands-regexp
@@ -158,7 +158,7 @@
 
 (defvar plastic-outline-regexp
   (concat "[[*]\\|"
-	  (proof-ids-to-regexp 
+	  (proof-ids-to-regexp
 	   '("Discharge" "DischargeKeep" "Freeze" "$?Goal" "Module" "Record" "Inductive"
      "Unfreeze"))))
 
@@ -167,9 +167,9 @@
 (defvar plastic-shell-outline-regexp plastic-goal-regexp)
 (defvar plastic-shell-outline-heading-end-regexp plastic-goal-regexp)
 
-(defvar plastic-error-occurred 
-        nil
-        "flag for whether undo is required for try or minibuffer cmds")
+(defvar plastic-error-occurred
+	nil
+	"flag for whether undo is required for try or minibuffer cmds")
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -183,7 +183,7 @@
    (plastic-shell-mode-config))
 
 (define-derived-mode plastic-mode proof-mode
-   "Plastic script" 
+   "Plastic script"
      "Major mode for Plastic proof scripts.
 
 \\{plastic-mode-map}"
@@ -197,7 +197,7 @@
     (setq font-lock-keywords plastic-font-lock-terms)
     (plastic-init-syntax-table)
     (proof-response-config-done)))
-  
+
 (define-derived-mode plastic-goals-mode proof-goals-mode
   "PlasticGoals" "Plastic Goal State"
   (plastic-goals-mode-config))
@@ -221,7 +221,7 @@ Given is the first SPAN which needs to be undone."
 		 (setq ct (+ 1 ct))))
 	    ((eq (span-property span 'type) 'pbp)
 	     (setq i 0)
-	     (while (< i (length string)) 
+	     (while (< i (length string))
 	       (if (= (aref string i) proof-terminal-char) (setq ct (+ 1 ct)))
 	       (setq i (+ 1 i)))))
       (setq span (next-span span 'type)))
@@ -229,13 +229,13 @@ Given is the first SPAN which needs to be undone."
 
 (defun plastic-goal-command-p (span)
   "Decide whether argument is a goal or not"			;; NEED CHG.
-  (proof-string-match plastic-goal-command-regexp 
+  (proof-string-match plastic-goal-command-regexp
 		      (or (span-property span 'cmd) "")))
 
-(defun plastic-find-and-forget (span) 
+(defun plastic-find-and-forget (span)
 	;; count the number of spans to undo.
 	;; all spans are equal...
-    ;; (NB the 'x' before the id is required so xNN looks like an id, 
+    ;; (NB the 'x' before the id is required so xNN looks like an id,
     ;;  so that Undo can be implemented via the tmp_cmd route.)
   (let (string (spans 0))
     (while span
@@ -244,31 +244,31 @@ Given is the first SPAN which needs to be undone."
       (plastic-preprocessing)		;; dynamic scope, on string
 
       (cond
-         ((null string) nil)
-         ((or (string-match "^\\s-*import" string) 
+	 ((null string) nil)
+	 ((or (string-match "^\\s-*import" string)
 	      (string-match "^\\s-*test" string)
 	      (string-match "^\\s-*\\$" string)
 	      (string-match "^\\s-*#" string))
-           
-	    (popup-dialog-box 
+
+	    (popup-dialog-box
 		(list (concat "Can't Undo imports yet\n"
-                                   "You have to exit Plastic for this\n")
+				   "You have to exit Plastic for this\n")
 		      ["ok, I'll do this" (lambda () t) t]))
 	    (return)
-           )    ;; warn the user that undo of imports not yet working.
-         (t (incf spans))
+	   )    ;; warn the user that undo of imports not yet working.
+	 (t (incf spans))
       )
       (setq span (next-span span 'type))
 
     )
     (concat plastic-lit-string " &S Undo x" (int-to-string spans) proof-terminal-string) ))
-  
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Other stuff which is required to customise script management   ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (defun plastic-goal-hyp ()		;; not used.
-  (cond 
+  (cond
    ((looking-at plastic-goal-regexp)
     (cons 'goal (match-string 1)))
    ((looking-at proof-shell-assumption-regexp)
@@ -288,7 +288,7 @@ Given is the first SPAN which needs to be undone."
 
 (eval-after-load "plastic" ;; da: so that plastic-lit-string can be changed
   '(progn
-     (eval `(proof-defshortcut plastic-Intros 
+     (eval `(proof-defshortcut plastic-Intros
 			       ,(concat plastic-lit-string "Intros ")  [(control i)]))
      (eval `(proof-defshortcut plastic-Refine
 			       ,(concat plastic-lit-string "Refine ")  [(control r)]))
@@ -311,17 +311,17 @@ Given is the first SPAN which needs to be undone."
 
 (defun plastic-shell-adjust-line-width ()
   "Use Plastic's pretty printing facilities to adjust output line width.
-   Checks the width in the `proof-goals-buffer' 
+   Checks the width in the `proof-goals-buffer'
    ACTUALLY - still need to work with this. (pcc, may99)"
    (and (buffer-live-p proof-goals-buffer)
-        (proof-shell-live-buffer)
-        (save-excursion
-        (set-buffer proof-goals-buffer)
-        (let ((current-width
-               ;; Actually, one might sometimes
-               ;; want to get the width of the proof-response-buffer
-               ;; instead. Never mind.
-               (window-width (get-buffer-window proof-goals-buffer t))))
+	(proof-shell-live-buffer)
+	(save-excursion
+	(set-buffer proof-goals-buffer)
+	(let ((current-width
+	       ;; Actually, one might sometimes
+	       ;; want to get the width of the proof-response-buffer
+	       ;; instead. Never mind.
+	       (window-width (get-buffer-window proof-goals-buffer t))))
 
 	   (if (equal current-width plastic-shell-current-line-width) ()
 	     ; else
@@ -349,12 +349,12 @@ Given is the first SPAN which needs to be undone."
 
   (setq proof-showproof-command (concat plastic-lit-string " &S PrfCtxt")
 	proof-goal-command      (concat plastic-lit-string " Claim %s;")
-	proof-save-command      (concat plastic-lit-string " Save %s;") ;; analogue? 
+	proof-save-command      (concat plastic-lit-string " Save %s;") ;; analogue?
 	proof-context-command   (concat plastic-lit-string " &S Ctxt 20"))
 
   (setq proof-showproof-command  (concat plastic-lit-string " &S PrfCtxt")
 	proof-goal-command   (concat plastic-lit-string " Claim %s;")
-	proof-save-command   (concat plastic-lit-string " Save %s;") ;; analogue? 
+	proof-save-command   (concat plastic-lit-string " Save %s;") ;; analogue?
 	proof-context-command  (concat plastic-lit-string " &S Ctxt 20")
 	   ;; show 20 things; see ^c+C...
 	proof-info-command   (concat plastic-lit-string " &S Help"))
@@ -362,7 +362,7 @@ Given is the first SPAN which needs to be undone."
   (setq proof-goal-command-p 'plastic-goal-command-p
 	proof-count-undos-fn 'plastic-count-undos
 	proof-find-and-forget-fn 'plastic-find-and-forget
-        pg-topterm-goalhyplit-fn 'plastic-goal-hyp
+	pg-topterm-goalhyplit-fn 'plastic-goal-hyp
 	proof-state-preserving-p 'plastic-state-preserving-p)
 
   (setq	proof-save-command-regexp plastic-save-command-regexp
@@ -371,13 +371,13 @@ Given is the first SPAN which needs to be undone."
 	proof-goal-with-hole-regexp plastic-goal-with-hole-regexp
 	proof-kill-goal-command plastic-kill-goal-command
 	proof-indent-any-regexp
-	(proof-regexp-alt 
-	 (proof-ids-to-regexp plastic-commands) 
+	(proof-regexp-alt
+	 (proof-ids-to-regexp plastic-commands)
 	 "\\s(" "\\s)"))
 
   (plastic-init-syntax-table)
 
-  ;; da: I've moved these out of proof-config-done in proof-script.el 
+  ;; da: I've moved these out of proof-config-done in proof-script.el
   (setq pbp-goal-command (concat "UNIMPLEMENTED"))
   (setq pbp-hyp-command (concat "UNIMPLEMENTED"))
 
@@ -388,7 +388,7 @@ Given is the first SPAN which needs to be undone."
   (proof-config-done)
 
 ;; outline
-  
+
   (make-local-variable 'outline-regexp)
   (setq outline-regexp plastic-outline-regexp)
 
@@ -414,12 +414,12 @@ Given is the first SPAN which needs to be undone."
   (add-hook 'proof-shell-handle-error-or-interrupt-hook 'plastic-had-error)
   (add-hook 'proof-shell-insert-hook       'plastic-preprocessing)
 
-;; (add-hook 'proof-shell-handle-error-or-interrupt-hook 
+;; (add-hook 'proof-shell-handle-error-or-interrupt-hook
 ;; (lambda()(goto-char (search-forward (char-to-string  proof-terminal-char)))))
 
 ;;  (add-hook 'proof-shell-handle-delayed-output-hook `plastic-show-shell-buffer t)
 ;; this forces display of shell-buffer after each cmd, rather than goals-buffer
-;; it is not always necessary - could always add it as a toggle option? 
+;; it is not always necessary - could always add it as a toggle option?
 
 ;; set up the env.
   (plastic-set-default-env-vars)
@@ -443,7 +443,7 @@ The directory and extension is stripped of FILENAME before the test."
 It needs to return an up to date list of all processed files. Its
 output is stored in `proof-included-files-list'. Its input is the
 string of which `plastic-shell-retract-files-regexp' matched a
-substring. 
+substring.
 
 We assume that module identifiers coincide with file names."
   (let ((module (match-string 1 str)))
@@ -455,40 +455,40 @@ We assume that module identifiers coincide with file names."
 
 (defun plastic-shell-mode-config ()
   (setq proof-shell-cd-cmd plastic-shell-cd
-        proof-shell-abort-goal-regexp plastic-shell-abort-goal-regexp
-        proof-shell-proof-completed-regexp plastic-shell-proof-completed-regexp
-        proof-shell-error-regexp plastic-error-regexp
-        proof-shell-interrupt-regexp plastic-interrupt-regexp
-        ;; DEAD proof-shell-noise-regexp "Discharge\\.\\. "
-        proof-shell-assumption-regexp plastic-id
-        proof-shell-goal-regexp plastic-goal-regexp
-        pg-subterm-first-special-char ?\360
-        proof-shell-wakeup-char ?\371		;; only for first send? 
+	proof-shell-abort-goal-regexp plastic-shell-abort-goal-regexp
+	proof-shell-proof-completed-regexp plastic-shell-proof-completed-regexp
+	proof-shell-error-regexp plastic-error-regexp
+	proof-shell-interrupt-regexp plastic-interrupt-regexp
+	;; DEAD proof-shell-noise-regexp "Discharge\\.\\. "
+	proof-shell-assumption-regexp plastic-id
+	proof-shell-goal-regexp plastic-goal-regexp
+	pg-subterm-first-special-char ?\360
+	proof-shell-wakeup-char ?\371		;; only for first send?
 ;;      proof-shell-wakeup-char nil		;; NIL turns off annotations.
-        pg-subterm-start-char ?\372
-        pg-subterm-sep-char ?\373
-        pg-subterm-end-char ?\374
-        pg-topterm-regexp "\375"
-        proof-shell-eager-annotation-start "\376"
+	pg-subterm-start-char ?\372
+	pg-subterm-sep-char ?\373
+	pg-subterm-end-char ?\374
+	pg-topterm-regexp "\375"
+	proof-shell-eager-annotation-start "\376"
 	;; FIXME da: if p-s-e-a-s is implemented, you should set
 	;; proof-shell-eager-annotation-start-length=1 to
 	;; avoid possibility of duplicating short messages.
-        proof-shell-eager-annotation-end "\377"
+	proof-shell-eager-annotation-end "\377"
 
-        proof-shell-annotated-prompt-regexp "LF> \371"
-        proof-shell-result-start "\372 Pbp result \373"
-        proof-shell-result-end "\372 End Pbp result \373"
-        proof-shell-start-goals-regexp "\372 Start of Goals \373"
-        proof-shell-end-goals-regexp "\372 End of Goals \373"
+	proof-shell-annotated-prompt-regexp "LF> \371"
+	proof-shell-result-start "\372 Pbp result \373"
+	proof-shell-result-end "\372 End Pbp result \373"
+	proof-shell-start-goals-regexp "\372 Start of Goals \373"
+	proof-shell-end-goals-regexp "\372 End of Goals \373"
 
-        proof-shell-init-cmd plastic-process-config
+	proof-shell-init-cmd plastic-process-config
 	proof-shell-restart-cmd plastic-process-config
-        pg-subterm-anns-use-stack nil
-        proof-shell-classify-output-system-specific plastic-shell-process-output
-        plastic-shell-current-line-width nil
+	pg-subterm-anns-use-stack nil
+	proof-shell-classify-output-system-specific plastic-shell-process-output
+	plastic-shell-current-line-width nil
 
 	proof-shell-process-file
-	(cons "Creating mark \"\\(.*\\)\" \\[\\(.*\\)\\]"  
+	(cons "Creating mark \"\\(.*\\)\" \\[\\(.*\\)\\]"
 	  (lambda (str) (let ((match (match-string 2 str)))
 			  (if (equal match "") match
 			    (concat (file-name-sans-extension match) ".l")))))
@@ -505,7 +505,7 @@ We assume that module identifiers coincide with file names."
 
 (defun plastic-goals-mode-config ()
   (setq pg-goals-change-goal "Next %s;"
-        pg-goals-error-regexp plastic-error-regexp)
+	pg-goals-error-regexp plastic-error-regexp)
   (setq proof-goals-font-lock-keywords plastic-font-lock-terms)
   (plastic-init-syntax-table)
   (proof-goals-config-done))
@@ -525,25 +525,25 @@ We assume that module identifiers coincide with file names."
    ;; might want to use proof-string-match here if matching is going
    ;; to be case sensitive (see docs)
 
-   (if (= 0 (length plastic-lit-string)) 
+   (if (= 0 (length plastic-lit-string))
        string				; no-op if non-literate
-     					; remaining lines are the
-     					; Else. (what, no 'return'?)
+					; remaining lines are the
+					; Else. (what, no 'return'?)
    (setq string (concat "\n" string " "))   ;; seed routine below, & extra char
-   (let* ;; da: let* not really needed, added to nuke byte-comp warnings. 
-       (x 
+   (let* ;; da: let* not really needed, added to nuke byte-comp warnings.
+       (x
 	(i 0)
 	(l (length string))
-	(eat-rest (lambda () 
-                    (aset string i ?\ )  ;; kill the \n or "-" at least
-                    (incf i)
-                    (while (and (< i l) (/= (aref string i) ?\n))
+	(eat-rest (lambda ()
+		    (aset string i ?\ )  ;; kill the \n or "-" at least
+		    (incf i)
+		    (while (and (< i l) (/= (aref string i) ?\n))
 		      (aset string i ?\ )
 		      (incf i) )))
-	(keep-rest (lambda () 
+	(keep-rest (lambda ()
 		     (loop for x in (string-to-list plastic-lit-string)
 		       do (aset string i ?\ ) (incf i))
-		     (while (and (< i l) 
+		     (while (and (< i l)
 				 (/= (aref string i) ?\n)
 				 (/= (aref string i) ?-))
 		       (incf i) ))))
@@ -552,16 +552,16 @@ We assume that module identifiers coincide with file names."
 	((eq 0 (string-match "--" (substring string i)))
 	 (funcall eat-rest))		; comment.
 	((eq 0 (string-match "\n\n" (substring string i)))
-	 (aset string i ?\ ) 
+	 (aset string i ?\ )
 	 (incf i))			; kill repeat \n
 	((= (aref string i) ?\n)	; start of new line
 	 (aset string i ?\ ) (incf i)	; remove \n
-	 (if (eq 0 (string-match plastic-lit-string 
+	 (if (eq 0 (string-match plastic-lit-string
 				 (substring string i)))
 	     (funcall keep-rest)	; code line.
 	   (funcall eat-rest)		; non-code line
 	   ))
-	(t 
+	(t
 	 (incf i))))			; else include.
      (setq string (replace-regexp-in-string "  +" " " string))
      (setq string (replace-regexp-in-string "^ +" "" string))
@@ -570,19 +570,19 @@ We assume that module identifiers coincide with file names."
      string))))
 
 
-(defun plastic-all-ctxt () 
+(defun plastic-all-ctxt ()
 	"show the full ctxt"
 	(interactive)
-	(proof-shell-invisible-command 
-              (concat plastic-lit-string " &S Ctxt" proof-terminal-string))
+	(proof-shell-invisible-command
+	      (concat plastic-lit-string " &S Ctxt" proof-terminal-string))
 	)
 
 (defun plastic-send-one-undo ()
 	"send an Undo cmd"
     ;; FIXME etc
-    ;; is like this because I don't want the undo output to be shown. 
+    ;; is like this because I don't want the undo output to be shown.
     (proof-shell-insert (concat plastic-lit-string " &S Undo;")
-                        'proof-done-invisible))
+			'proof-done-invisible))
 
 ;; hacky expt version.
 ;; still don't understand the significance of cmd!
@@ -594,7 +594,7 @@ We assume that module identifiers coincide with file names."
     (print "hello")
     (plastic-reset-error)
     (if (and proof-state-preserving-p
-           (not (funcall proof-state-preserving-p cmd)))
+	   (not (funcall proof-state-preserving-p cmd)))
       (error "Command is not state preserving, I won't execute it!"))
     (proof-shell-invisible-command cmd)
     (plastic-call-if-no-error 'plastic-send-one-undo))
@@ -615,9 +615,9 @@ We assume that module identifiers coincide with file names."
     "take cmd from minibuffer - see doc for proof-minibuffer-cmd"
     (interactive)
     (let (cmd)
-        (setq cmd (read-string "Command: " nil 'proof-minibuffer-history))
-        (setq cmd (concat plastic-lit-string " " cmd proof-terminal-string))
-        (proof-shell-invisible-command cmd)))
+	(setq cmd (read-string "Command: " nil 'proof-minibuffer-history))
+	(setq cmd (concat plastic-lit-string " " cmd proof-terminal-string))
+	(proof-shell-invisible-command cmd)))
 
 (defun plastic-had-error ()
     "sets var plastic-error-occurred, called from hook"
@@ -652,7 +652,7 @@ We assume that module identifiers coincide with file names."
 
 ;;;;;;;;;;;;;;;;;
 ;; hacky overriding of the toolbar command and C-c C-v action
-;; my version handles literate characters. 
+;; my version handles literate characters.
 ;; (should do better for long-term though)
 
 (defalias 'proof-toolbar-command 'plastic-minibuf)
diff --git a/twelf/twelf-font.el b/twelf/twelf-font.el
index 012bfaa7..44e5468e 100644
--- a/twelf/twelf-font.el
+++ b/twelf/twelf-font.el
@@ -1,7 +1,7 @@
 ;; twelf-font.el  Font lock configuration for Twelf
 ;;
 ;; Author: Frank Pfenning
-;;	   Taken from Twelf's emacs mode and 
+;;	   Taken from Twelf's emacs mode and
 ;;	   adapted for Proof General by David Aspinall <David.Aspinall@ed.ac.uk>
 ;;
 ;; $Id$
@@ -49,7 +49,7 @@
        (twelf-font-create-face 'twelf-font-parm-face 'default "Orange")
        (twelf-font-create-face 'twelf-font-fvar-face 'default "SpringGreen")
        (twelf-font-create-face 'twelf-font-evar-face 'default "Aquamarine"))
-      (t 
+      (t
        (twelf-font-create-face 'twelf-font-keyword-face 'default nil)
        (twelf-font-create-face 'twelf-font-comment-face 'font-lock-comment-face
 			     nil)
@@ -79,7 +79,7 @@
     ;; for LLF, with punctuation marks
     ;;"\\([][:.(){},]\\|\\<<-\\>\\|\\<->\\>\\|\\<o-\\>\\|\\<-o\\>\\|\\<<T>\\>\\|\\<&\\>\\|\\^\\|()\\|\\<type\\>\\|\\<sigma\\>\\)"
     ;; for Elf, no punction marks
-    ;;"\\(\\<<-\\>\\|\\<->\\>\\|\\<type\\>\\|\\<sigma\\>\\)" 
+    ;;"\\(\\<<-\\>\\|\\<->\\>\\|\\<type\\>\\|\\<sigma\\>\\)"
     ;; for Elf, including punctuation marks
     ;;"\\([][:.(){}]\\|\\<<-\\>\\|\\<->\\>\\|\\<type\\>\\|\\<sigma\\>\\)"
    . twelf-font-keyword-face)
@@ -169,7 +169,7 @@ regular expressions."
 		     (t (error "Illegal font-lock-keyword instructions"))))
 	      (t (error "Illegal font-lock-keyword instructions")))
 	(cond ((symbolp fun-or-regexp)	; a function to call
-	       (while 
+	       (while
 		   (setq region (funcall fun-or-regexp end))
 		 ;; END is limit of forward search, start at point
 		 ;; and move point
@@ -320,7 +320,7 @@ For these purposes, an existential variable is a bound, upper-case identifier."
 ;;;
 ;;;
 ;;; This comes from twelf-old.el but is needed for fontification,
-;;; 
+;;;
 ;;; Perhaps some of these parsing functions will need reusing
 ;;; for sending input to server properly?
 ;;;
@@ -336,15 +336,15 @@ If declaration ends in `.' then COMPLETE is t, otherwise nil."
     (save-excursion
       ;; Skip backwards if between declarations
       (if (or (eobp) (looking-at (concat "[" *whitespace* "]")))
-          (skip-chars-backward (concat *whitespace* ".")))
+	  (skip-chars-backward (concat *whitespace* ".")))
       (setq par-end (point))
       ;; Move forward from beginning of decl until last
       ;; declaration before par-end is found.
       (if (not (bobp)) (backward-paragraph 1))
       (setq par-start (point))
       (while (and (twelf-end-of-par par-end)
-                  (< (point) par-end))
-        (setq par-start (point)))
+		  (< (point) par-end))
+	(setq par-start (point)))
       ;; Now par-start is at end of preceding declaration or query.
       (goto-char par-start)
       (skip-twelf-comments-and-whitespace)
@@ -359,23 +359,23 @@ If declaration ends in `.' then COMPLETE is t, otherwise nil."
 Return the declared identifier or `nil' if none was found.
 FILENAME and ERROR-BUFFER are used if something appears wrong."
   (let ((id nil)
-        end-of-id
+	end-of-id
 	beg-of-id)
     (skip-twelf-comments-and-whitespace)
     (while (and (not id) (not (eobp)))
       (setq beg-of-id (point))
       (if (zerop (skip-chars-forward *twelf-id-chars*))
-          ;; Not looking at id: skip ahead
-          (skip-ahead filename (current-line-absolute) "No identifier"
-                      error-buffer)
-        (setq end-of-id (point))
-        (skip-twelf-comments-and-whitespace)
-        (if (not (looking-at ":"))
-            ;; Not looking at valid decl: skip ahead
-            (skip-ahead filename (current-line-absolute end-of-id) "No colon"
-                        error-buffer)
-          (goto-char end-of-id)
-          (setq id (buffer-substring beg-of-id end-of-id))))
+	  ;; Not looking at id: skip ahead
+	  (skip-ahead filename (current-line-absolute) "No identifier"
+		      error-buffer)
+	(setq end-of-id (point))
+	(skip-twelf-comments-and-whitespace)
+	(if (not (looking-at ":"))
+	    ;; Not looking at valid decl: skip ahead
+	    (skip-ahead filename (current-line-absolute end-of-id) "No colon"
+			error-buffer)
+	  (goto-char end-of-id)
+	  (setq id (buffer-substring beg-of-id end-of-id))))
       (skip-twelf-comments-and-whitespace))
     id))
 
@@ -393,9 +393,9 @@ FILENAME and ERROR-BUFFER are used if something appears wrong."
   (skip-chars-forward *whitespace*)
   (while (looking-at *twelf-comment-start*)
     (cond ((looking-at "%{")		; delimited comment
-           (condition-case nil (forward-sexp 1)
+	   (condition-case nil (forward-sexp 1)
 	     (error (goto-char (point-max))))
-           (or (eobp) (forward-char 1)))
+	   (or (eobp) (forward-char 1)))
 	  (t				; single-line comment
 	   (end-of-line 1)))
     (skip-chars-forward *whitespace*)))
@@ -408,8 +408,8 @@ Skips over comments (single-line or balanced delimited).
 Optional argument LIMIT specifies limit of search for period."
   (if (not limit)
       (save-excursion
-        (forward-paragraph 1)
-        (setq limit (point))))
+	(forward-paragraph 1)
+	(setq limit (point))))
   (while (and (not (looking-at "\\."))
 	      (< (point) limit))
     (skip-chars-forward "^.%" limit)
@@ -418,10 +418,10 @@ Optional argument LIMIT specifies limit of search for period."
 	  ((looking-at "%")
 	   (forward-char 1))))
   (cond ((looking-at "\\.")
-         (forward-char 1)
-         t)
-        (t ;; stopped at limit
-         nil)))
+	 (forward-char 1)
+	 t)
+	(t ;; stopped at limit
+	 nil)))
 
 (defun skip-ahead (filename line message error-buffer)
   "Skip ahead when syntactic error was found.
diff --git a/twelf/twelf-old.el b/twelf/twelf-old.el
index 42d87d20..41664839 100644
--- a/twelf/twelf-old.el
+++ b/twelf/twelf-old.el
@@ -31,25 +31,25 @@
 ;;; ;; Tell Emacs where the Twelf libraries are.
 ;;; (setq load-path
 ;;;       (cons "/afs/cs/project/twelf/research/twelf/emacs" load-path))
-;;; 
+;;;
 ;;; ;; Autoload libraries when Twelf-related major modes are started.
 ;;; (autoload 'twelf-mode "twelf" "Major mode for editing Twelf source." t)
 ;;; (autoload 'twelf-server "twelf" "Run an inferior Twelf server." t)
 ;;; (autoload 'twelf-sml "twelf" "Run an inferior Twelf-SML process." t)
-;;; 
+;;;
 ;;; ;; Switch buffers to Twelf mode based on filename extension,
 ;;; ;; which is one of .elf, .quy, .thm, or .cfg.
 ;;; (setq auto-mode-alist
 ;;;       (cons '("\\.elf$" . twelf-mode)
-;;; 	    (cons '("\\.quy$" . twelf-mode)
-;;; 		  (cons '("\\.thm$" . twelf-mode)
-;;; 			(cons '("\\.cfg$" . twelf-mode)
-;;; 			      auto-mode-alist)))))
-;;; 
+;;;	    (cons '("\\.quy$" . twelf-mode)
+;;;		  (cons '("\\.thm$" . twelf-mode)
+;;;			(cons '("\\.cfg$" . twelf-mode)
+;;;			      auto-mode-alist)))))
+;;;
 ;;; ;; Default Twelf server program location
 ;;; (setq twelf-server-program
 ;;;       "/afs/cs/project/twelf/research/twelf/bin/twelf-server")
-;;; 
+;;;
 ;;; ;; Default Twelf SML program location
 ;;; (setq twelf-sml-program
 ;;;       "/afs/cs/project/twelf/misc/smlnj/bin/sml-cm")
@@ -57,7 +57,7 @@
 ;;; ;; Default documentation location (in info format)
 ;;; (setq twelf-info-file
 ;;;       "/afs/cs/project/twelf/research/twelf/doc/info/twelf.info")
-;;; 
+;;;
 ;;; ;; Automatically highlight Twelf sources using font-lock
 ;;; (add-hook 'twelf-mode-hook 'twelf-font-fontify-buffer)
 ;;;
@@ -203,7 +203,7 @@
 ;;; Added NT Emacs bug workaround
 
 (require 'comint)
-(require 'easymenu) 
+(require 'easymenu)
 
 ;;;----------------------------------------------------------------------
 ;;; User visible variables
@@ -467,9 +467,9 @@ Maintained to present reasonable menus.")
   (skip-chars-forward *whitespace*)
   (while (looking-at *twelf-comment-start*)
     (cond ((looking-at "%{")		; delimited comment
-           (condition-case nil (forward-sexp 1)
+	   (condition-case nil (forward-sexp 1)
 	     (error (goto-char (point-max))))
-           (or (eobp) (forward-char 1)))
+	   (or (eobp) (forward-char 1)))
 	  (t				; single-line comment
 	   (end-of-line 1)))
     (skip-chars-forward *whitespace*)))
@@ -482,8 +482,8 @@ Skips over comments (single-line or balanced delimited).
 Optional argument LIMIT specifies limit of search for period."
   (if (not limit)
       (save-excursion
-        (forward-paragraph 1)
-        (setq limit (point))))
+	(forward-paragraph 1)
+	(setq limit (point))))
   (while (and (not (looking-at "\\."))
 	      (< (point) limit))
     (skip-chars-forward "^.%" limit)
@@ -492,10 +492,10 @@ Optional argument LIMIT specifies limit of search for period."
 	  ((looking-at "%")
 	   (forward-char 1))))
   (cond ((looking-at "\\.")
-         (forward-char 1)
-         t)
-        (t ;; stopped at limit
-         nil)))
+	 (forward-char 1)
+	 t)
+	(t ;; stopped at limit
+	 nil)))
 
 (defun twelf-current-decl ()
   "Returns list (START END COMPLETE) for current Twelf declaration.
@@ -506,15 +506,15 @@ If declaration ends in `.' then COMPLETE is t, otherwise nil."
     (save-excursion
       ;; Skip backwards if between declarations
       (if (or (eobp) (looking-at (concat "[" *whitespace* "]")))
-          (skip-chars-backward (concat *whitespace* ".")))
+	  (skip-chars-backward (concat *whitespace* ".")))
       (setq par-end (point))
       ;; Move forward from beginning of decl until last
       ;; declaration before par-end is found.
       (if (not (bobp)) (backward-paragraph 1))
       (setq par-start (point))
       (while (and (twelf-end-of-par par-end)
-                  (< (point) par-end))
-        (setq par-start (point)))
+		  (< (point) par-end))
+	(setq par-start (point)))
       ;; Now par-start is at end of preceding declaration or query.
       (goto-char par-start)
       (skip-twelf-comments-and-whitespace)
@@ -528,8 +528,8 @@ If declaration ends in `.' then COMPLETE is t, otherwise nil."
   "Marks current Twelf declaration and moves point to its beginning."
   (interactive)
   (let* ((par (twelf-current-decl))
-         (par-start (nth 0 par))
-         (par-end (nth 1 par)))
+	 (par-start (nth 0 par))
+	 (par-end (nth 1 par)))
     (push-mark par-end)
     (goto-char par-start)))
 
@@ -537,8 +537,8 @@ If declaration ends in `.' then COMPLETE is t, otherwise nil."
   "Indent each line of the current Twelf declaration."
   (interactive)
   (let* ((par (twelf-current-decl))
-         (par-start (nth 0 par))
-         (par-end (nth 1 par)))
+	 (par-start (nth 0 par))
+	 (par-end (nth 1 par)))
     (goto-char par-start)
     (twelf-indent-lines (count-lines par-start par-end))))
 
@@ -546,12 +546,12 @@ If declaration ends in `.' then COMPLETE is t, otherwise nil."
   "Indent each line of the region as Twelf code."
   (interactive "r")
   (cond ((< from to)
-         (goto-char from)
-         (twelf-indent-lines (count-lines from to)))
-        ((> from to)
-         (goto-char to)
-         (twelf-indent-lines (count-lines to from)))
-        (t nil)))
+	 (goto-char from)
+	 (twelf-indent-lines (count-lines from to)))
+	((> from to)
+	 (goto-char to)
+	 (twelf-indent-lines (count-lines to from)))
+	(t nil)))
 
 (defun twelf-indent-lines (n)
   "Indent N lines starting at point."
@@ -565,12 +565,12 @@ If declaration ends in `.' then COMPLETE is t, otherwise nil."
   "Calculates the proper Twelf comment column.
 Currently does not deal specially with pragmas."
   (cond ((looking-at "%%%")
-         0)
-        ((looking-at "%[%{]")
-         (car (twelf-calculate-indent)))
-        (t
-         (skip-chars-backward " \t")
-         (max (if (bolp) 0 (1+ (current-column))) comment-column))))
+	 0)
+	((looking-at "%[%{]")
+	 (car (twelf-calculate-indent)))
+	(t
+	 (skip-chars-backward " \t")
+	 (max (if (bolp) 0 (1+ (current-column))) comment-column))))
 
 (defun looked-at ()
   "Returns the last string matched against.
@@ -584,44 +584,44 @@ This recognizes comments, matching delimiters, and standard infix operators."
   (let ((old-point (point)))
     (beginning-of-line)
     (let* ((indent-info (twelf-calculate-indent))
-           (indent-column (nth 0 indent-info))
-           (indent-type (nth 1 indent-info))
-           (indent-string (nth 2 indent-info)))
+	   (indent-column (nth 0 indent-info))
+	   (indent-type (nth 1 indent-info))
+	   (indent-string (nth 2 indent-info)))
       (skip-chars-forward " \t")        ; skip whitespace
       (let ((fwdskip (- old-point (point))))
-        (cond ((looking-at "%%%")
+	(cond ((looking-at "%%%")
 	       (twelf-indent-line-to 0 fwdskip)) ; %%% comment at column 0
-              ((looking-at "%[%{]")     ; delimited or %% comment
-               (twelf-indent-line-to indent-column fwdskip))
-              ((looking-at *twelf-comment-start*)    ; indent single-line comment
-               (indent-for-comment)
-               (forward-char -1))
+	      ((looking-at "%[%{]")     ; delimited or %% comment
+	       (twelf-indent-line-to indent-column fwdskip))
+	      ((looking-at *twelf-comment-start*)    ; indent single-line comment
+	       (indent-for-comment)
+	       (forward-char -1))
 	      ((looking-at "%")		; %keyword declaration
 	       (twelf-indent-line-to indent-column fwdskip))
-              ((looking-at twelf-infix-regexp) ; looking at infix operator
-               (if (string= indent-string (looked-at))
-                   ;; indent string is the same as the one we are looking at
-                   (twelf-indent-line-to indent-column fwdskip)
-                 (twelf-indent-line-to (+ indent-column twelf-indent) fwdskip)))
-              ((eq indent-type 'delimiter) ; indent after delimiter
-               (twelf-indent-line-to (+ indent-column twelf-indent) fwdskip))
-              ((eq indent-type 'limit)  ; no delimiter or infix found.
-               (twelf-indent-line-to indent-column fwdskip))
-              ((eq indent-type 'infix)
-               (twelf-indent-line-to (+ indent-column twelf-indent) fwdskip)))))))
+	      ((looking-at twelf-infix-regexp) ; looking at infix operator
+	       (if (string= indent-string (looked-at))
+		   ;; indent string is the same as the one we are looking at
+		   (twelf-indent-line-to indent-column fwdskip)
+		 (twelf-indent-line-to (+ indent-column twelf-indent) fwdskip)))
+	      ((eq indent-type 'delimiter) ; indent after delimiter
+	       (twelf-indent-line-to (+ indent-column twelf-indent) fwdskip))
+	      ((eq indent-type 'limit)  ; no delimiter or infix found.
+	       (twelf-indent-line-to indent-column fwdskip))
+	      ((eq indent-type 'infix)
+	       (twelf-indent-line-to (+ indent-column twelf-indent) fwdskip)))))))
 
 (defun twelf-indent-line-to (indent fwdskip)
   "Indent current line to INDENT then skipping to FWDSKIP if positive.
 Assumes point is on the first non-whitespace character of the line."
   (let ((text-start (point))
-        (shift-amount (- indent (current-column))))
+	(shift-amount (- indent (current-column))))
     (if (= shift-amount 0)
-        nil
+	nil
       (beginning-of-line)
       (delete-region (point) text-start)
       (indent-to indent))
     (if (> fwdskip 0)
-        (forward-char fwdskip))))
+	(forward-char fwdskip))))
 
 (defun twelf-calculate-indent ()
   "Calculate the indentation and return a list (INDENT INDENT-TYPE STRING).
@@ -630,12 +630,12 @@ INDENT-TYPE is 'DELIMITER, 'INFIX, or 'LIMIT, and
 STRING is the delimiter, infix operator, or the empty string, respectively."
   (save-excursion
     (let* ((par (twelf-current-decl))
-           (par-start (nth 0 par))
-           (par-end (nth 1 par))
-           (par-complete (nth 2 par))
-           (limit (cond ((> par-start (point)) (point))
-                        ((and (> (point) par-end) par-complete) par-end)
-                        (t par-start))))
+	   (par-start (nth 0 par))
+	   (par-end (nth 1 par))
+	   (par-complete (nth 2 par))
+	   (limit (cond ((> par-start (point)) (point))
+			((and (> (point) par-end) par-complete) par-end)
+			(t par-start))))
       (twelf-dsb limit))))
 
 (defun twelf-dsb (limit)
@@ -643,25 +643,25 @@ STRING is the delimiter, infix operator, or the empty string, respectively."
 This currently does not deal with comments or mis-matched delimiters.
 Argument LIMIT specifies bound for backwards search."
   (let ((result nil)
-        (lparens 0) (lbraces 0) (lbrackets 0))
+	(lparens 0) (lbraces 0) (lbrackets 0))
     (while (not result)
       (if (or (= lparens 1) (= lbraces 1) (= lbrackets 1))
-          (setq result (list (current-column) 'delimiter (looked-at)))
-        (if (re-search-backward (concat "[][{}()]\\|" twelf-infix-regexp)
-                                limit 'limit) ; return 'LIMIT if limit reached
-            (let ((found (looked-at)))
-              (cond
-               ((string= found "(") (setq lparens (1+ lparens)))
-               ((string= found ")") (setq lparens (1- lparens)))
-               ((string= found "{") (setq lbraces (1+ lbraces)))
-               ((string= found "}") (setq lbraces (1- lbraces)))
-               ((string= found "[") (setq lbrackets (1+ lbrackets)))
-               ((string= found "]") (setq lbrackets (1- lbrackets)))
-               (t;; otherwise, we are looking at an infix operator
-                (if (and (= lparens 0) (= lbraces 0) (= lbrackets 0))
-                    (setq result (list (current-column) 'infix found))
-                  nil))))               ; embedded - skip
-          (setq result (list 0 'limit ""))))) ; reached the limit, no indent
+	  (setq result (list (current-column) 'delimiter (looked-at)))
+	(if (re-search-backward (concat "[][{}()]\\|" twelf-infix-regexp)
+				limit 'limit) ; return 'LIMIT if limit reached
+	    (let ((found (looked-at)))
+	      (cond
+	       ((string= found "(") (setq lparens (1+ lparens)))
+	       ((string= found ")") (setq lparens (1- lparens)))
+	       ((string= found "{") (setq lbraces (1+ lbraces)))
+	       ((string= found "}") (setq lbraces (1- lbraces)))
+	       ((string= found "[") (setq lbrackets (1+ lbrackets)))
+	       ((string= found "]") (setq lbrackets (1- lbrackets)))
+	       (t;; otherwise, we are looking at an infix operator
+		(if (and (= lparens 0) (= lbraces 0) (= lbrackets 0))
+		    (setq result (list (current-column) 'infix found))
+		  nil))))               ; embedded - skip
+	  (setq result (list 0 'limit ""))))) ; reached the limit, no indent
     result))
 
 (defun twelf-mode-variables ()
@@ -926,12 +926,12 @@ read a file name from the minibuffer."
    "Regexp to extract fields of Twelf error.")
 
 (defconst twelf-error-decl-regexp
-  "^[-=? \t]*\\(.+\\)::\\([^ \t\n]+\\) "  
+  "^[-=? \t]*\\(.+\\)::\\([^ \t\n]+\\) "
   "Regexp to extract filename and identifier from declaration error.")
 
 (defun looked-at-nth (n)
   (let ((b (match-beginning n))
-        (e (match-end n)))
+	(e (match-end n)))
     (if (or (null b) (null e)) nil
       (buffer-substring (match-beginning n) (match-end n)))))
 
@@ -948,11 +948,11 @@ or (\"Local\" START-CHAR NIL END-CHAR NIL)."
     (goto-char pt)
     (re-search-forward twelf-error-fields-regexp)
     (list (looked-at-nth 1)		; file or "Local" or "stdIn"
-          (looked-at-nth-int 2)		; start line or char
-          (looked-at-nth-int 4)		; start column, if given, else nil
-          (looked-at-nth-int 6)		; end line, if given, else nil or char
-          (looked-at-nth-int 8)		; end column, if given, else nil
-          )))
+	  (looked-at-nth-int 2)		; start line or char
+	  (looked-at-nth-int 4)		; start column, if given, else nil
+	  (looked-at-nth-int 6)		; end line, if given, else nil or char
+	  (looked-at-nth-int 8)		; end column, if given, else nil
+	  )))
 
 (defun twelf-error-decl (pos)
   "Determines if the error is identified only by its declaration."
@@ -968,12 +968,12 @@ or (\"Local\" START-CHAR NIL END-CHAR NIL)."
   (forward-char (if (not (= line0 1)) (1- col0) (1- (1- col0))))
   ;; select region, if non-empty
   (cond ((not (null line1))
-         (push-mark (point))
-         (cond ((not (= line1 line0))
-                (forward-line (- line1 line0))
-                (forward-char (1- col1)))
-               (t (forward-char (- col1 col0))))
-         (exchange-point-and-mark)
+	 (push-mark (point))
+	 (cond ((not (= line1 line0))
+		(forward-line (- line1 line0))
+		(forward-char (1- col1)))
+	       (t (forward-char (- col1 col0))))
+	 (exchange-point-and-mark)
 	 (funcall twelf-highlight-range-function (point) (mark)))))
 
 (defun twelf-mark-absolute (line0 col0 line1 col1)
@@ -1023,13 +1023,13 @@ put the cursor at the beginning of the error source. If the
 error message specifies a range, the mark is placed at the end."
   (interactive)
   (let ((case-fold-search nil)
-        (twelf-buffer (or *twelf-last-input-buffer*
-                        (error "Cannot determine process buffer with last input")))
+	(twelf-buffer (or *twelf-last-input-buffer*
+			(error "Cannot determine process buffer with last input")))
 	error-begin)
     (pop-to-buffer twelf-buffer)
     (goto-char *twelf-error-pos*)   ; go to last error
     (if (not (re-search-forward twelf-error-regexp (point-max) t))
-        (error "No error message found.")
+	(error "No error message found.")
       (setq error-begin (match-beginning 0))
       (setq *twelf-error-pos* (point))
       (set-window-start (get-buffer-window twelf-buffer)
@@ -1089,7 +1089,7 @@ error message specifies a range, the mark is placed at the end."
 Also updates the error cursor to the current line."
   (interactive)
   (pop-to-buffer (or *twelf-last-input-buffer*
-                     (error "Cannot determine process buffer with last input")))
+		     (error "Cannot determine process buffer with last input")))
   (beginning-of-line)
   (setq *twelf-error-pos* (point))
   (twelf-next-error))
@@ -1206,9 +1206,9 @@ for purposes of error parsing."
 With prefix argument also displays Twelf server buffer."
   (interactive "P")
   (let* ((par (twelf-current-decl))
-         (par-start (nth 0 par))
-         (par-end (nth 1 par))
-         (decl (twelf-buffer-substring-dot par-start par-end)))
+	 (par-start (nth 0 par))
+	 (par-end (nth 1 par))
+	 (decl (twelf-buffer-substring-dot par-start par-end)))
     (twelf-focus par-start par-end)
     (twelf-server-send-command (concat "readDecl\n" decl))
     (twelf-server-wait displayp)))
@@ -1330,13 +1330,13 @@ type of the particular instance of the constant."
     (let ((end-of-id (point)))
       (skip-chars-backward *twelf-id-chars* (point-min))
       (let ((c (if (= (point) end-of-id)
-                   ;; we didn't move.  this should eventually become a
-                   ;; completing-read
-                   (read-string "Constant: ")
-                 (buffer-substring (point) end-of-id))))
-        (twelf-server-send-command (concat "decl " c))
-        (twelf-server-wait t)             ; Wait for and display reply
-        (goto-char previous-point)))))
+		   ;; we didn't move.  this should eventually become a
+		   ;; completing-read
+		   (read-string "Constant: ")
+		 (buffer-substring (point) end-of-id))))
+	(twelf-server-send-command (concat "decl " c))
+	(twelf-server-wait t)             ; Wait for and display reply
+	(goto-char previous-point)))))
 
 ;; Unused? -fp
 ;(defun twelf-backwards-parse-arglist ()
@@ -1346,7 +1346,7 @@ type of the particular instance of the constant."
 ;      (set-buffer twelf-server-buffer)
 ;      (goto-char *twelf-server-last-process-mark*)
 ;      ;; Should be right at the beginning of the output.
-;      ;; (re-search-forward "^arglist") ; 
+;      ;; (re-search-forward "^arglist") ;
 ;      ;; (beginning-of-line 2)
 ;      (let ((arglist-begin (point)))
 ;        (skip-chars-forward "^." (point-max))
@@ -1465,9 +1465,9 @@ server buffer."
   (setq *twelf-last-input-buffer* (current-buffer))
   (setq *twelf-error-pos* (marker-position (process-mark (twelf-server-process))))
   (cond ((string-match twelf-server-cd-regexp input)
-         (let ((expanded-dir (expand-dir (looked-at-string input 1))))
-           (setq default-directory expanded-dir)
-           (pwd)))
+	 (let ((expanded-dir (expand-dir (looked-at-string input 1))))
+	   (setq default-directory expanded-dir)
+	   (pwd)))
 	((string-match "^set\\s +chatter\\s +\\([0-9]\\)+" input)
 	 (setq twelf-chatter (string-to-number (looked-at-string input 1))))
 	;;((string-match "^set\\s +trace\\s +\\([0-9]\\)+" input)
@@ -1522,22 +1522,22 @@ The following commands are available:
     (skip-chars-forward *whitespace*)
     (while (not (eobp))                 ; end of buffer?
       (cond ((looking-at "%")           ; comment through end of line
-             (end-of-line))
-            (t (let ((begin-point (point))) ; parse filename starting at point
-                 (skip-chars-forward (concat "^" *whitespace*))
-                 (let* ((file-name (buffer-substring begin-point (point)))
-                        (absolute-file-name
-                         (expand-file-name file-name default-directory)))
-                   (if (file-readable-p absolute-file-name)
-                       (setq filelist (cons absolute-file-name filelist))
-                     (error "File %s not readable." file-name))))))
+	     (end-of-line))
+	    (t (let ((begin-point (point))) ; parse filename starting at point
+		 (skip-chars-forward (concat "^" *whitespace*))
+		 (let* ((file-name (buffer-substring begin-point (point)))
+			(absolute-file-name
+			 (expand-file-name file-name default-directory)))
+		   (if (file-readable-p absolute-file-name)
+		       (setq filelist (cons absolute-file-name filelist))
+		     (error "File %s not readable." file-name))))))
       (skip-chars-forward *whitespace*))
     filelist))
 
 (defun twelf-server-read-config ()
   "Read the configuration and initialize *twelf-config-list*."
   (if (or (not (bufferp *twelf-config-buffer*))
-          (null (buffer-name *twelf-config-buffer*)))
+	  (null (buffer-name *twelf-config-buffer*)))
       (error "No current configuration buffer"))
   (set-buffer *twelf-config-buffer*)
   (goto-char (point-min))
@@ -1546,7 +1546,7 @@ The following commands are available:
 (defun twelf-server-sync-config ()
   "Synchronize the configuration file, buffer, and Twelf server."
   (if (or (not (bufferp *twelf-config-buffer*))
-          (null (buffer-name *twelf-config-buffer*)))
+	  (null (buffer-name *twelf-config-buffer*)))
       (error "No current configuration buffer"))
   (if (and twelf-config-mode
 	   (not (equal *twelf-config-buffer* (current-buffer)))
@@ -1556,38 +1556,38 @@ The following commands are available:
   (save-excursion
     (set-buffer *twelf-config-buffer*)
     (if (buffer-modified-p *twelf-config-buffer*)
-        (progn
-          (display-buffer *twelf-config-buffer*)
-          (if (yes-or-no-p "Config buffer has changed, save new version? ")
-              (save-buffer)
-            (message "Checking old configuration"))))
+	(progn
+	  (display-buffer *twelf-config-buffer*)
+	  (if (yes-or-no-p "Config buffer has changed, save new version? ")
+	      (save-buffer)
+	    (message "Checking old configuration"))))
     (if (not (verify-visited-file-modtime *twelf-config-buffer*))
-        (if (yes-or-no-p "Config file has changed, read new contents? ")
-            (revert-buffer t t)))
+	(if (yes-or-no-p "Config file has changed, read new contents? ")
+	    (revert-buffer t t)))
     (if (not (equal (visited-file-modtime) *twelf-config-time*))
-        (progn 
-          (display-buffer *twelf-config-buffer*)
-          (if (yes-or-no-p "Config file has changed, reconfigure server? ")
-              (twelf-server-configure (buffer-file-name *twelf-config-buffer*)
-                                    "Server OK: Configured")
-            (if (not (yes-or-no-p "Ask next time? "))
-                (setq *twelf-config-time* (visited-file-modtime))))))))
+	(progn
+	  (display-buffer *twelf-config-buffer*)
+	  (if (yes-or-no-p "Config file has changed, reconfigure server? ")
+	      (twelf-server-configure (buffer-file-name *twelf-config-buffer*)
+				    "Server OK: Configured")
+	    (if (not (yes-or-no-p "Ask next time? "))
+		(setq *twelf-config-time* (visited-file-modtime))))))))
 
 (defun twelf-get-server-buffer (&optional createp)
   "Get the current Twelf server buffer.
 Optional argument CREATEP indicates if the buffer should be
 created if it doesn't exist."
   (if (and (bufferp *twelf-server-buffer*)
-           (not (null (buffer-name *twelf-server-buffer*))))
+	   (not (null (buffer-name *twelf-server-buffer*))))
       *twelf-server-buffer*
     (if createp
-        (let ((twelf-server-buffer
-               (get-buffer-create *twelf-server-buffer-name*)))
-          (save-window-excursion
-            (set-buffer twelf-server-buffer)
-            (twelf-server-mode)
-            (setq *twelf-server-buffer* twelf-server-buffer))
-          twelf-server-buffer)
+	(let ((twelf-server-buffer
+	       (get-buffer-create *twelf-server-buffer-name*)))
+	  (save-window-excursion
+	    (set-buffer twelf-server-buffer)
+	    (twelf-server-mode)
+	    (setq *twelf-server-buffer* twelf-server-buffer))
+	  twelf-server-buffer)
       (error "No Twelf server buffer"))))
 
 (defun twelf-init-variables ()
@@ -1605,17 +1605,17 @@ twelf-server-program.
 This locally re-binds `twelf-server-timeout' to 15 secs."
   (interactive)
   (let* ((default-program (if (null program) twelf-server-program program))
-         (default-dir (file-name-directory default-program))
-         (program (expand-file-name
-                   (if (null program)
-                       (read-file-name (concat "Twelf server: (default "
-                                               (file-name-nondirectory
-                                                default-program)
-                                               ") ")
-                                       default-dir
-                                       default-program
-                                       t)
-                     program)))
+	 (default-dir (file-name-directory default-program))
+	 (program (expand-file-name
+		   (if (null program)
+		       (read-file-name (concat "Twelf server: (default "
+					       (file-name-nondirectory
+						default-program)
+					       ") ")
+				       default-dir
+				       default-program
+				       t)
+		     program)))
 	 ;; longer timeout during startup
 	 (twelf-server-timeout 15))
     ;; We save the program name as the default for the next time a server is
@@ -1623,12 +1623,12 @@ This locally re-binds `twelf-server-timeout' to 15 secs."
     (setq twelf-server-program program))
   (save-window-excursion
     (let* ((twelf-server-buffer (twelf-get-server-buffer t))
-           (twelf-server-process (get-buffer-process twelf-server-buffer)))
+	   (twelf-server-process (get-buffer-process twelf-server-buffer)))
       (set-buffer twelf-server-buffer)
       (if (not (null twelf-server-process))
-          (if (yes-or-no-p "Kill current server process? ")
-              (delete-process twelf-server-process)
-            (error "Twelf Server restart aborted")))
+	  (if (yes-or-no-p "Kill current server process? ")
+	      (delete-process twelf-server-process)
+	    (error "Twelf Server restart aborted")))
       (goto-char (point-max))
       (setq *twelf-server-last-process-mark* (point))
       ;; initialize variables
@@ -1642,11 +1642,11 @@ This locally re-binds `twelf-server-timeout' to 15 secs."
 (defun twelf-server-process (&optional buffer)
   "Return the twelf server process, starting one if none exists."
   (let* ((twelf-server-buffer (if (null buffer) (twelf-get-server-buffer t)
-                              buffer))
-         (twelf-server-process (get-buffer-process twelf-server-buffer)))
+			      buffer))
+	 (twelf-server-process (get-buffer-process twelf-server-buffer)))
       (if (not (null twelf-server-process))
-          twelf-server-process
-          (twelf-server))))
+	  twelf-server-process
+	  (twelf-server))))
 
 (defun twelf-server-display (&optional selectp)
   "Display Twelf server buffer, moving to the end of output.
@@ -1658,37 +1658,37 @@ With prefix argument also selects the Twelf server buffer."
 (defun display-server-buffer (&optional buffer)
   "Display the Twelf server buffer so that the end of output is visible."
   (let* ((twelf-server-buffer (if (null buffer) (twelf-get-server-buffer)
-                              buffer))
-         (_ (set-buffer twelf-server-buffer))
-         (twelf-server-process (twelf-server-process twelf-server-buffer))
-         (proc-mark (process-mark twelf-server-process))
-         (_ (display-buffer twelf-server-buffer))
-         (twelf-server-window (get-buffer-window twelf-server-buffer)))
+			      buffer))
+	 (_ (set-buffer twelf-server-buffer))
+	 (twelf-server-process (twelf-server-process twelf-server-buffer))
+	 (proc-mark (process-mark twelf-server-process))
+	 (_ (display-buffer twelf-server-buffer))
+	 (twelf-server-window (get-buffer-window twelf-server-buffer)))
     (if (not (pos-visible-in-window-p proc-mark twelf-server-window))
-        (progn
-          (push-mark proc-mark)
-          (set-window-point twelf-server-window proc-mark)))
+	(progn
+	  (push-mark proc-mark)
+	  (set-window-point twelf-server-window proc-mark)))
     (sit-for 0)))
 
 (defun twelf-server-send-command (command)
   "Send a string COMMAND to the Twelf server."
   (interactive "sCommand: ")
   (let* ((input (concat command "\n"))
-         (twelf-server-buffer (twelf-get-server-buffer))
-         (twelf-server-process (twelf-server-process twelf-server-buffer)))
+	 (twelf-server-buffer (twelf-get-server-buffer))
+	 (twelf-server-process (twelf-server-process twelf-server-buffer)))
     (if twelf-server-echo-commands
-        (let ((previous-buffer (current-buffer)))
-          (if twelf-server-display-commands
-              (display-server-buffer twelf-server-buffer))
-          (set-buffer twelf-server-buffer)
-          (goto-char (point-max))
-          (insert input)
-          (set-marker (process-mark twelf-server-process) (point-max))
-          (setq *twelf-error-pos* (point-max))
-          (set-buffer previous-buffer)))
+	(let ((previous-buffer (current-buffer)))
+	  (if twelf-server-display-commands
+	      (display-server-buffer twelf-server-buffer))
+	  (set-buffer twelf-server-buffer)
+	  (goto-char (point-max))
+	  (insert input)
+	  (set-marker (process-mark twelf-server-process) (point-max))
+	  (setq *twelf-error-pos* (point-max))
+	  (set-buffer previous-buffer)))
     (setq *twelf-last-input-buffer* twelf-server-buffer)
     (setq *twelf-server-last-process-mark*
-          (marker-position (process-mark twelf-server-process)))
+	  (marker-position (process-mark twelf-server-process)))
     (comint-send-string twelf-server-process input)))
 
 (defun twelf-accept-process-output (process timeout)
@@ -1708,37 +1708,37 @@ OK-MESSAGE and ABORT-MESSAGE are the strings to show upon successful
 completion or abort of the server which default to \"Server OK\" and
 \"Server ABORT\"."
   (let* ((chunk-count 0)
-         (last-point *twelf-server-last-process-mark*)
-         (previous-buffer (current-buffer))
-         (previous-match-data (match-data))
-         (twelf-server-buffer (twelf-get-server-buffer))
-         (twelf-server-process (get-buffer-process twelf-server-buffer)))
+	 (last-point *twelf-server-last-process-mark*)
+	 (previous-buffer (current-buffer))
+	 (previous-match-data (match-data))
+	 (twelf-server-buffer (twelf-get-server-buffer))
+	 (twelf-server-process (get-buffer-process twelf-server-buffer)))
     (unwind-protect
-        (catch 'done
-          (set-buffer twelf-server-buffer)
-          (while t
-            (goto-char last-point)
-            (if (re-search-forward "\\(%% OK %%\n\\)\\|\\(%% ABORT %%\n\\)"
-                                   (point-max) 'limit)
-                (cond ((match-beginning 1)
-                       (if displayp
-                           (display-server-buffer twelf-server-buffer))
-                       (message (or ok-message "Server OK"))
-                       (throw 'done nil))
-                      ((match-beginning 2)
-                       (display-server-buffer twelf-server-buffer)
-                       (error (or abort-message "Server ABORT"))
-                       (throw 'done nil)))
-              (cond ((or (not (twelf-accept-process-output
-                               twelf-server-process twelf-server-timeout))
-                         (= last-point (point)))
-                     (display-server-buffer twelf-server-buffer)
-                     (message "Server TIMEOUT, continuing Emacs")
-                     (throw 'done nil))
-                    (t (setq chunk-count (+ chunk-count 1))
-                       (if (= (mod chunk-count 10) 0)
-                           (message (make-string (/ chunk-count 10) ?#)))
-                       (sit-for 0))))))
+	(catch 'done
+	  (set-buffer twelf-server-buffer)
+	  (while t
+	    (goto-char last-point)
+	    (if (re-search-forward "\\(%% OK %%\n\\)\\|\\(%% ABORT %%\n\\)"
+				   (point-max) 'limit)
+		(cond ((match-beginning 1)
+		       (if displayp
+			   (display-server-buffer twelf-server-buffer))
+		       (message (or ok-message "Server OK"))
+		       (throw 'done nil))
+		      ((match-beginning 2)
+		       (display-server-buffer twelf-server-buffer)
+		       (error (or abort-message "Server ABORT"))
+		       (throw 'done nil)))
+	      (cond ((or (not (twelf-accept-process-output
+			       twelf-server-process twelf-server-timeout))
+			 (= last-point (point)))
+		     (display-server-buffer twelf-server-buffer)
+		     (message "Server TIMEOUT, continuing Emacs")
+		     (throw 'done nil))
+		    (t (setq chunk-count (+ chunk-count 1))
+		       (if (= (mod chunk-count 10) 0)
+			   (message (make-string (/ chunk-count 10) ?#)))
+		       (sit-for 0))))))
       (store-match-data previous-match-data)
       (set-buffer previous-buffer))))
 
@@ -1782,27 +1782,27 @@ Starts a Twelf servers if necessary."
 			    nil ; don't require match for now
 			    )))))
   (let* ((config-file (if (file-directory-p config-file)
-                          (concat config-file "sources.cfg")
-                        config-file))
+			  (concat config-file "sources.cfg")
+			config-file))
 	 (config-file-os (twelf-convert-standard-filename config-file))
-         (config-dir (file-name-directory config-file))
+	 (config-dir (file-name-directory config-file))
 	 (config-dir-os (twelf-convert-standard-filename config-dir))
-         (config-buffer (set-buffer (or (get-file-buffer config-file)
-                                        (find-file-noselect config-file))))
-         config-list)
+	 (config-buffer (set-buffer (or (get-file-buffer config-file)
+					(find-file-noselect config-file))))
+	 config-list)
     (setq *twelf-config-buffer* config-buffer)
     (if (and (not (verify-visited-file-modtime (get-file-buffer config-file)))
-             (yes-or-no-p "Config file has changed, read new contents? "))
-        (revert-buffer t t))
+	     (yes-or-no-p "Config file has changed, read new contents? "))
+	(revert-buffer t t))
     (setq config-list (twelf-server-read-config))
     (twelf-server-process)                ; Start process if necessary
     (let* ((_ (set-buffer (twelf-get-server-buffer)))
-           (cd-command
-            (if (equal default-directory config-dir)
-                nil
-              (setq default-directory config-dir)
-              (concat "OS.chDir " config-dir-os)))
-           (_ (set-buffer config-buffer)))
+	   (cd-command
+	    (if (equal default-directory config-dir)
+		nil
+	      (setq default-directory config-dir)
+	      (concat "OS.chDir " config-dir-os)))
+	   (_ (set-buffer config-buffer)))
       (cond ((not (null cd-command))
 	     (twelf-server-send-command cd-command)
 	     (twelf-server-wait nil ""
@@ -1810,7 +1810,7 @@ Starts a Twelf servers if necessary."
       (twelf-server-send-command
        (concat "Config.read " config-file-os))
       (twelf-server-wait nil (or ok-message "Server OK")
-                       "Server ABORT: Could not be configured")
+		       "Server ABORT: Could not be configured")
       ;; *twelf-config-buffer* should still be current buffer here
       (setq *twelf-config-time* (visited-file-modtime))
       (setq *twelf-config-list* config-list))))
@@ -1885,7 +1885,7 @@ Starts a Twelf servers if necessary."
 When called interactively, prompts for parameter and value, supporting
 completion."
   (interactive
-   (let* ((parm (completing-read 
+   (let* ((parm (completing-read
 		 "Parameter: " *twelf-parm-table* nil t))
 	  (argtype (cdr (assoc parm *twelf-parm-table*)))
 	  (value (twelf-read-value argtype)))
@@ -1957,9 +1957,9 @@ if the Twelf server is hopelessly wedged."
   (interactive)
   (twelf-server twelf-server-program)
   (twelf-server-configure (if *twelf-config-buffer*
-                            (buffer-file-name *twelf-config-buffer*)
-                          "sources.cfg")
-                        "Server configured, now checking...")
+			    (buffer-file-name *twelf-config-buffer*)
+			  "sources.cfg")
+			"Server configured, now checking...")
   (twelf-check-config))
 
 ;;;----------------------------------------------------------------------
@@ -2000,12 +2000,12 @@ Optional argument TAGS-FILENAME specifies alternative filename."
   (interactive)
   (twelf-server-sync-config)
   (let* ((error-buffer (twelf-get-server-buffer))
-         (config-filename (buffer-file-name *twelf-config-buffer*))
-         (tags-file
-          (or tags-filename
-              (if (string-equal "sources.cfg"
+	 (config-filename (buffer-file-name *twelf-config-buffer*))
+	 (tags-file
+	  (or tags-filename
+	      (if (string-equal "sources.cfg"
 				(file-name-nondirectory config-filename))
-                  (concat (file-name-directory config-filename "TAGS"))
+		  (concat (file-name-directory config-filename "TAGS"))
 		(concat (file-name-sans-extension config-filename)
 			".tag")))))
     (save-excursion
@@ -2014,10 +2014,10 @@ Optional argument TAGS-FILENAME specifies alternative filename."
       (insert "Tagging configuration " config-filename " in file " tags-file "\n"))
     (set-buffer *twelf-config-buffer*)
     (twelf-tag-files (rev-relativize *twelf-config-list* default-directory)
-                   tags-file error-buffer)
+		   tags-file error-buffer)
     (if (get-buffer-process error-buffer)
-        (set-marker (process-mark (get-buffer-process error-buffer))
-                    (point-max)))))
+	(set-marker (process-mark (get-buffer-process error-buffer))
+		    (point-max)))))
 
 (defun twelf-tag-files (filelist &optional tags-filename error-buffer)
   "Create tags file for FILELIST, routing errors to buffer *tags-errors*.
@@ -2025,17 +2025,17 @@ Optional argument TAGS-FILENAME specifies alternative filename (default: TAGS),
 optional argument ERROR-BUFFER specifies alternative buffer for error message
 (default: *tags-errors*)."
   (let* ((tags-filename (or tags-filename "TAGS"))
-         (tags-buffer (find-file-noselect tags-filename))
-         (error-buffer (or error-buffer (new-temp-buffer "*tags-errors*"))))
+	 (tags-buffer (find-file-noselect tags-filename))
+	 (error-buffer (or error-buffer (new-temp-buffer "*tags-errors*"))))
     (save-excursion
       (set-buffer tags-buffer)
       (if (equal (point-min) (point-max))
-          nil
-        ;;(pop-to-buffer tags-buffer)
-        ;;(if (yes-or-no-p "Delete current tags information? ")
-        (delete-region (point-min) (point-max))
-        ;;)
-        ))
+	  nil
+	;;(pop-to-buffer tags-buffer)
+	;;(if (yes-or-no-p "Delete current tags information? ")
+	(delete-region (point-min) (point-max))
+	;;)
+	))
     (switch-to-buffer-other-window error-buffer)
     (while (not (null filelist))
       (twelf-tag-file (car filelist) tags-buffer error-buffer)
@@ -2047,14 +2047,14 @@ optional argument ERROR-BUFFER specifies alternative buffer for error message
 (defun twelf-tag-file (filename tags-buffer error-buffer)
   "Deposit tag information for FILENAME in TAGS-BUFFER, errors in ERROR-BUFFER."
   (let ((src-buffer (find-file-noselect filename))
-        file-start file-end end-of-id tag-string)
+	file-start file-end end-of-id tag-string)
     (save-excursion
       (set-buffer tags-buffer)
       (goto-char (point-max))
       (insert "\f\n" filename ",0\n")
       (setq file-start (point))
       (save-excursion
-        (set-buffer src-buffer)
+	(set-buffer src-buffer)
 	(goto-char (point-min))
 	(while (twelf-next-decl filename error-buffer)
 	  (setq end-of-id (point))
@@ -2084,23 +2084,23 @@ optional argument ERROR-BUFFER specifies alternative buffer for error message
 Return the declared identifier or `nil' if none was found.
 FILENAME and ERROR-BUFFER are used if something appears wrong."
   (let ((id nil)
-        end-of-id
+	end-of-id
 	beg-of-id)
     (skip-twelf-comments-and-whitespace)
     (while (and (not id) (not (eobp)))
       (setq beg-of-id (point))
       (if (zerop (skip-chars-forward *twelf-id-chars*))
-          ;; Not looking at id: skip ahead
-          (skip-ahead filename (current-line-absolute) "No identifier"
-                      error-buffer)
-        (setq end-of-id (point))
-        (skip-twelf-comments-and-whitespace)
-        (if (not (looking-at ":"))
-            ;; Not looking at valid decl: skip ahead
-            (skip-ahead filename (current-line-absolute end-of-id) "No colon"
-                        error-buffer)
-          (goto-char end-of-id)
-          (setq id (buffer-substring beg-of-id end-of-id))))
+	  ;; Not looking at id: skip ahead
+	  (skip-ahead filename (current-line-absolute) "No identifier"
+		      error-buffer)
+	(setq end-of-id (point))
+	(skip-twelf-comments-and-whitespace)
+	(if (not (looking-at ":"))
+	    ;; Not looking at valid decl: skip ahead
+	    (skip-ahead filename (current-line-absolute end-of-id) "No colon"
+			error-buffer)
+	  (goto-char end-of-id)
+	  (setq id (buffer-substring beg-of-id end-of-id))))
       (skip-twelf-comments-and-whitespace))
     id))
 
@@ -2127,9 +2127,9 @@ Optional argument NAME specified an alternative name."
   (if (not name) (setq name "*temp*"))
   (if (get-buffer name)
       (save-excursion
-        (set-buffer name)
-        (delete-region (point-min) (point-max))
-        (get-buffer name))
+	(set-buffer name)
+	(delete-region (point-min) (point-max))
+	(get-buffer name))
     (get-buffer-create name)))
 
 (defun rev-relativize (filelist dir)
@@ -2137,7 +2137,7 @@ Optional argument NAME specified an alternative name."
   (let ((newlist nil))
     (while (not (null filelist))
       (setq newlist
-            (cons (file-relative-name (car filelist) dir) newlist))
+	    (cons (file-relative-name (car filelist) dir) newlist))
       (setq filelist (cdr filelist)))
     newlist))
 
@@ -2162,7 +2162,7 @@ Optional argument NAME specified an alternative name."
   "Expand argument and check that it is a directory."
   (let ((expanded-dir (file-name-as-directory (expand-file-name dir))))
     (if (not (file-directory-p expanded-dir))
-        (error "%s is not a directory" dir))
+	(error "%s is not a directory" dir))
     expanded-dir))
 
 (defun twelf-sml-cd (dir)
@@ -2190,11 +2190,11 @@ Used as comint-input-sentinel in Twelf-SML buffer."
   (setq *twelf-last-input-buffer* (current-buffer))
   (setq *twelf-error-pos* (marker-position (process-mark (twelf-sml-process))))
   (cond ((string-match twelf-sml-cd-regexp input)
-         (let ((expanded-dir (expand-dir (substring input
-                                                    (match-beginning 1)
-                                                    (match-end 1)))))
-           (setq default-directory expanded-dir)
-           (pwd)))))
+	 (let ((expanded-dir (expand-dir (substring input
+						    (match-beginning 1)
+						    (match-end 1)))))
+	   (setq default-directory expanded-dir)
+	   (pwd)))))
 
 (defun twelf-sml-mode ()
   "Major mode for interacting with an inferior Twelf-SML process.
@@ -2209,7 +2209,7 @@ Customisation: Entry to this mode runs the hooks on twelf-sml-mode-hook.
 You can send queries to the inferior Twelf-SML process from other buffers.
 
 Commands:
-Return after the end of the process' output sends the text from the 
+Return after the end of the process' output sends the text from the
     end of process to point.
 Return before the end of the process' output copies the current line
     to the end of the process' output, and sends it.
@@ -2237,8 +2237,8 @@ to continue it."
   ;; Workaround for problem with Lucid Emacs version of comint.el:
   ;; must exclude double quotes " and must include $ and # in filenames.
   (make-local-variable 'comint-match-partial-pathname-chars)
-  (setq comint-match-partial-pathname-chars 
-        "^][<>{}()!^&*\\|?`'\" \t\n\r\b")
+  (setq comint-match-partial-pathname-chars
+	"^][<>{}()!^&*\\|?`'\" \t\n\r\b")
 
   (setq major-mode 'twelf-sml-mode)
   (setq mode-name "Twelf-SML")
@@ -2275,24 +2275,24 @@ With argument, positions cursor at end of buffer."
       (pop-to-buffer (twelf-sml-process-buffer))
       (error "No current process buffer. "))
   (cond (eob-p
-         (push-mark)
-         (goto-char (point-max)))))
+	 (push-mark)
+	 (goto-char (point-max)))))
 
 (defun display-twelf-sml-buffer (&optional buffer)
   "Display the Twelf-SML buffer so that the end of output is visible."
   ;; Accept output from Twelf-SML process
   (sit-for 1)
   (let* ((twelf-sml-buffer (if (null buffer) (twelf-sml-process-buffer)
-                       buffer))
-         (_ (set-buffer twelf-sml-buffer))
-         (twelf-sml-process (twelf-sml-process))
-         (proc-mark (process-mark twelf-sml-process))
-         (_ (display-buffer twelf-sml-buffer))
-         (twelf-sml-window (get-buffer-window twelf-sml-buffer)))
+		       buffer))
+	 (_ (set-buffer twelf-sml-buffer))
+	 (twelf-sml-process (twelf-sml-process))
+	 (proc-mark (process-mark twelf-sml-process))
+	 (_ (display-buffer twelf-sml-buffer))
+	 (twelf-sml-window (get-buffer-window twelf-sml-buffer)))
     (if (not (pos-visible-in-window-p proc-mark twelf-sml-window))
-        (progn
-          (push-mark proc-mark)
-          (set-window-point twelf-sml-window proc-mark)))))
+	(progn
+	  (push-mark proc-mark)
+	  (set-window-point twelf-sml-window proc-mark)))))
 
 (defun twelf-sml-send-string (string)
   "Send the given string to the Twelf-SML process."
@@ -2308,14 +2308,14 @@ If the region is short, it is sent directly, via COMINT-SEND-REGION."
       (twelf-sml-send-region end start and-go)
     ;; (setq twelf-sml-last-region-sent (list (current-buffer) start end))
     (let ((cur-buffer (current-buffer))
-          (twelf-sml-buffer (twelf-sml-process-buffer)))
+	  (twelf-sml-buffer (twelf-sml-process-buffer)))
       (switch-to-buffer twelf-sml-buffer)
       ;; (setq sml-error-pos (marker-position (process-mark (twelf-sml-process))))
       (setq *twelf-last-input-buffer* twelf-sml-buffer)
       (switch-to-buffer cur-buffer))
     (comint-send-region (twelf-sml-process) start end)
     (if (not (string= (buffer-substring (1- end) end) "\n"))
-        (comint-send-string (twelf-sml-process) "\n"))
+	(comint-send-string (twelf-sml-process) "\n"))
     ;; Next two lines mess up when an Twelf error occurs, since the
     ;; newline is not read and later messes up counting.
     ;; (if (not and-go)
@@ -2328,8 +2328,8 @@ If the region is short, it is sent directly, via COMINT-SEND-REGION."
 Prefix argument means switch-to-twelf-sml afterwards."
   (interactive "P")
   (let* ((par (twelf-current-decl))
-         (query-start (nth 0 par))
-         (query-end (nth 1 par)))
+	 (query-start (nth 0 par))
+	 (query-end (nth 1 par)))
     (twelf-sml-set-mode 'TWELF)
     (twelf-sml-send-region query-start query-end and-go)))
 
@@ -2359,17 +2359,17 @@ Results:
  MORE --- asking whether to find the next solution
  UNKNOWN --- process is running, but can't tell status."
   (let* ((twelf-sml-buffer (or buffer (twelf-sml-process-buffer)))
-         (twelf-sml-process (get-buffer-process twelf-sml-buffer)))
+	 (twelf-sml-process (get-buffer-process twelf-sml-buffer)))
     (if (null twelf-sml-process)
-        'NONE
+	'NONE
       (save-excursion
-        (set-buffer twelf-sml-buffer)
-        (let ((buffer-end (buffer-substring (max (point-min) (- (point-max) 3))
-                                            (point-max))))
-          (cond ((string-match "\\?- " buffer-end) 'TWELF)
-                ((string-match "\n- " buffer-end) 'ML)
-                ((string-match "More\\? " buffer-end) 'MORE)
-                (t 'UNKNOWN)))))))
+	(set-buffer twelf-sml-buffer)
+	(let ((buffer-end (buffer-substring (max (point-min) (- (point-max) 3))
+					    (point-max))))
+	  (cond ((string-match "\\?- " buffer-end) 'TWELF)
+		((string-match "\n- " buffer-end) 'ML)
+		((string-match "More\\? " buffer-end) 'MORE)
+		(t 'UNKNOWN)))))))
 
 (defvar twelf-sml-init "Twelf.Config.load (Twelf.Config.read \"sources.cfg\");\n"
   "Initial command sent to Twelf-SML process when started during twelf-sml-set-mode 'TWELF.")
@@ -2383,21 +2383,21 @@ been achieved.  This allows for asynchronous operation."
     ((eq mode 'ML)
      (let ((status (twelf-sml-status)))
        (cond ((eq status 'NONE) (twelf-sml) 't)
-             ((eq status 'ML) 't)
-             ((eq status 'TWELF) (twelf-sml-send-string "") 't)
-             ((eq status 'MORE) (twelf-sml-send-string "q\n") 't)
-             ((eq status 'UNKNOWN) nil))))
+	     ((eq status 'ML) 't)
+	     ((eq status 'TWELF) (twelf-sml-send-string "") 't)
+	     ((eq status 'MORE) (twelf-sml-send-string "q\n") 't)
+	     ((eq status 'UNKNOWN) nil))))
     ((eq mode 'TWELF)
      (let ((status (twelf-sml-status)))
        (cond ((eq status 'NONE)
-              (twelf-sml)
-              (twelf-sml-send-string twelf-sml-init)
-              (twelf-sml-send-string "Twelf.top ();\n") 't)
-             ((eq status 'ML)
-              (twelf-sml-send-string "Twelf.top ();\n") 't)
-             ((eq status 'TWELF) 't)
-             ((eq status 'MORE) (twelf-sml-send-string "\n") 't)
-             ((eq status 'UNKNOWN) nil))))
+	      (twelf-sml)
+	      (twelf-sml-send-string twelf-sml-init)
+	      (twelf-sml-send-string "Twelf.top ();\n") 't)
+	     ((eq status 'ML)
+	      (twelf-sml-send-string "Twelf.top ();\n") 't)
+	     ((eq status 'TWELF) 't)
+	     ((eq status 'MORE) (twelf-sml-send-string "\n") 't)
+	     ((eq status 'UNKNOWN) nil))))
     (t (error "twelf-sml-set-mode: illegal mode %s" mode))))
 
 (defun twelf-sml-quit ()
@@ -2413,7 +2413,7 @@ been achieved.  This allows for asynchronous operation."
   "Returns the current Twelf-SML process."
   (let ((proc (get-buffer-process (or buffer (twelf-sml-process-buffer)))))
     (or proc
-        (error "No current process."))))
+	(error "No current process."))))
 
 ;;;----------------------------------------------------------------------
 ;;; 2Twelf-SML minor mode for Twelf
@@ -2460,16 +2460,16 @@ Mode map
   (interactive "P")
   (make-local-variable 'twelf-to-twelf-sml-mode)
   (cond ((not (assq 'twelf-to-twelf-sml-mode minor-mode-alist))
-         (setq minor-mode-alist
-               (cons '(twelf-to-twelf-sml-mode " 2Twelf-SML")
-                     minor-mode-alist))))
+	 (setq minor-mode-alist
+	       (cons '(twelf-to-twelf-sml-mode " 2Twelf-SML")
+		     minor-mode-alist))))
   (cond ((or (not twelf-to-twelf-sml-mode) prefix)
-         (setq twelf-to-twelf-sml-mode t)
-         (use-local-map twelf-to-twelf-sml-mode-map)
-         (run-hooks 'twelf-to-twelf-sml-mode-hook))
-        (t
-         (setq twelf-to-twelf-sml-mode nil)
-         (use-local-map twelf-mode-map))))
+	 (setq twelf-to-twelf-sml-mode t)
+	 (use-local-map twelf-to-twelf-sml-mode-map)
+	 (run-hooks 'twelf-to-twelf-sml-mode-hook))
+	(t
+	 (setq twelf-to-twelf-sml-mode nil)
+	 (use-local-map twelf-mode-map))))
 
 ;;;----------------------------------------------------------------------
 ;;; Twelf mode menus
@@ -2658,4 +2658,3 @@ This may be selected from the menubar.  In XEmacs, also bound to Button3."
   (twelf-server-add-menu))
 
 (provide 'twelf-old)
-
diff --git a/twelf/twelf.el b/twelf/twelf.el
index 07590ea9..236846f9 100644
--- a/twelf/twelf.el
+++ b/twelf/twelf.el
@@ -1,6 +1,6 @@
 ;; twelf.el  Proof General instance for Twelf
 ;;
-;; Copyright (C) 2000 LFCS Edinburgh. 
+;; Copyright (C) 2000 LFCS Edinburgh.
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;; Author:    David Aspinall <David.Aspinall@ed.ac.uk>
 ;;
@@ -10,13 +10,13 @@
 ;; TODO:
 ;;   Info doc menu entry
 ;;   X-Symbol upgrade/test?  Mule XE better?
-;; 
+;;
 
 
 (require 'proof-easy-config)            ; easy configure mechanism
 
 (require 'twelf-font)			; font lock configuration
-;; (require 'twelf-old)	
+;; (require 'twelf-old)
 ;; FIXME: put parts of old code into twelf-syntax or similar
 
 ;;
@@ -37,7 +37,7 @@
 ;;
 ;; Instantiation of Proof General
 ;;
-(proof-easy-config 'twelf "Twelf" 
+(proof-easy-config 'twelf "Twelf"
  proof-prog-name		 "twelf-server"
  proof-assistant-home-page       "http://www.cs.cmu.edu/~twelf/"
 
@@ -61,7 +61,7 @@
 
  ;; "Eager annotations" mark messages Proof General should display
  ;; or recognize while the prover is pontificating
- proof-shell-eager-annotation-start   
+ proof-shell-eager-annotation-start
  "^\\[Opening \\|\\[Closing "
  proof-shell-eager-annotation-end "\n"
 
@@ -71,14 +71,14 @@
 
 ;; unset: all of the interactive proof commands
 ;; These don't really apply, I don't think, because Twelf
-;; only has fully automatic prover at the moment. 
+;; only has fully automatic prover at the moment.
 ;; Also, there is no concept of "undo" to remove declarations
 ;; (can simply repeat them, tho.)
 ;; proof-goal-command-regexp       "^%theorem"
 ;; proof-save-command-regexp       "" ;; FIXME: empty?
 ;; proof-goal-with-hole-regexp     "^%theorem\w-+\\(.*\\)\w-+:"
 ;; proof-save-with-hole-regexp     "" ;; FIXME
-;; proof-non-undoables-regexp     
+;; proof-non-undoables-regexp
 ;; proof-goal-command              "%theorem %s."
 ;; proof-save-command              "%prove "
 ;; remaining strings are left over from Isabelle example
@@ -87,12 +87,12 @@
 ;; proof-undo-n-times-cmd          "pg_repeat undo %s;"
 ;; proof-shell-start-goals-regexp  "Level [0-9]"
 ;; proof-shell-end-goals-regexp    "val it"
-;; proof-shell-init-cmd  
+;; proof-shell-init-cmd
 ;; proof-shell-proof-completed-regexp "^No subgoals!"
 
 
 ;;
-;; Twelf server doesn't take declarations directly: 
+;; Twelf server doesn't take declarations directly:
 ;; we need to pre-process script input slightly
 ;;
 
@@ -122,7 +122,7 @@
 
 ;; A-Z and a-z are already word constituents
 ;; For fontification, it would be better if _ and ' were word constituents
-(twelf-map-string 
+(twelf-map-string
  'twelf-set-word "!&$^+/<=>?@~|#*`;,-0123456789\\") ; word constituents
 (twelf-map-string 'twelf-set-symbol "_'")         ; symbol constituents
 ;; Delimited comments are %{ }%, see 1234 below.
@@ -130,7 +130,7 @@
 (twelf-set-syntax ?\t "    ")           ; whitespace
 ; da: this old entry is wrong: it says % always starts a comment
 ;(twelf-set-syntax ?% "< 14")            ; comment begin
-; This next one is much better, 
+; This next one is much better,
 (twelf-set-syntax ?% ". 14")            ; comment begin/second char
 (twelf-set-syntax ?\n ">   ")           ; comment end
 (twelf-set-syntax ?: ".   ")            ; punctuation
@@ -163,7 +163,7 @@
 
 (defun twelf-mode-extra-config ()
   (make-local-hook 'font-lock-after-fontify-buffer-hook)
-  (add-hook 'font-lock-after-fontify-buffer-hook 
+  (add-hook 'font-lock-after-fontify-buffer-hook
 	    'twelf-font-fontify-buffer nil 'local)
   (font-lock-mode))
 
@@ -204,6 +204,6 @@
 
 (defpgdefault menu-entries
   (cdr twelf-syntax-menu))
-  
+
 
 (provide 'twelf)