Tidy whitespace

8 files changed, 145 insertions, 151 deletions

diff --git a/phox/phox-extraction.el b/phox/phox-extraction.el
index b488d43e..d81acde1 100644
--- a/phox/phox-extraction.el
+++ b/phox/phox-extraction.el
@@ -1,4 +1,4 @@
-;; $State$ $Date$ $Revision$ 
+;; $State$ $Date$ $Revision$
 ;;--------------------------------------------------------------------------;;
 ;;--------------------------------------------------------------------------;;
 ;; program extraction.
@@ -13,11 +13,11 @@
 (defun phox-prog-flags-modify(option)
 "ask for a string that are options to pass to phox binary"
 (interactive "soption :")
-; pas d'analyse de la réponse, 
+; pas d'analyse de la réponse,
 (let ((process))
   (if  (and phox-prog-name
 	    (progn (string-match " \\|$" phox-prog-name)
-		   (setq process 
+		   (setq process
 			 (substring phox-prog-name 0 (match-beginning 0))
 			 )
 		   )
@@ -27,7 +27,7 @@
   )
 (if (string-match "^ *$" option)
     (progn
-      (message 
+      (message
        "no option other than default ones will be passed to phox binary.")
       (setq phox-prog-name phox-prog-orig))
   (progn
@@ -46,7 +46,7 @@ compile theorem_name.
 output."
 (interactive)
 (phox-prog-flags-modify "-f")
-(message 
+(message
 "WARNING : program extraction is experimental and can disturb the prover !")
 )
 
@@ -71,13 +71,13 @@ output."
 
 ; compilation
 (defun phox-compile-theorem(name)
-  "Interactive function : 
+  "Interactive function :
 ask for the name of a theorem and send a compile command to PhoX for it."
   (interactive "stheorem : ")
   (proof-shell-invisible-command (concat "compile " name)))
 
 (defun phox-compile-theorem-on-cursor()
-"Interactive function : 
+"Interactive function :
 send a compile command to PhoX for the theorem which name is under the cursor."
   (interactive)
   (let (start end)
@@ -94,8 +94,8 @@ send a compile command to PhoX for the theorem which name is under the cursor."
 
 (defun phox-output ()
 
-"Interactive function : 
-send output command to phox in order to obtain programs 
+"Interactive function :
+send output command to phox in order to obtain programs
 extracted from proofs of all compiled theorems."
 
 
@@ -103,19 +103,19 @@ extracted from proofs of all compiled theorems."
 (proof-shell-invisible-command  "output"))
 
 (defun phox-output-theorem (name)
-"Interactive function : 
+"Interactive function :
 ask for the name of a theorem and send an output command to PhoX for it
 in order to obtain a programm extracted from the known proof of this theorem."
   (interactive "stheorem : ")
   (proof-shell-invisible-command (concat "output " name)))
 
 (defun phox-output-theorem-on-cursor()
-"Interactive function : 
+"Interactive function :
 send an output command to PhoX for the theorem which name is under the cursor
 in order to obtain a programm extracted from the known proof of this theorem."
   (interactive)
-  (let (start 
-	end 
+  (let (start
+	end
 ;	(syntax (char-to-string (char-syntax ?\.)))
 	)
     (save-excursion
@@ -142,7 +142,7 @@ in order to obtain a programm extracted from the known proof of this theorem."
        ]
       ["------------------------------" nil nil
        ]
-      ["Compile theorem on cursor" phox-compile-theorem-on-cursor 
+      ["Compile theorem on cursor" phox-compile-theorem-on-cursor
        :active(string-match "\-f$" phox-prog-name)
        ]
       ["Extraction for theorem on cursor" phox-output-theorem-on-cursor
diff --git a/phox/phox-font.el b/phox/phox-font.el
index 37a6a910..2eca2c5a 100644
--- a/phox/phox-font.el
+++ b/phox/phox-font.el
@@ -48,8 +48,8 @@
        "prove\\|"
        "r\\(e\\(write\\(_hyp\\)?\\|name\\)\\|mh\\)\\|"
        "s\\(elect\\|how\\|lh\\)\\|"
-       "t\\(hen\\|rivial\\)\\|" 
-       "u\\(se\\|n\\(do\\|fold\\(_hyp\\)?\\|lock\\)\\)\\|" 
+       "t\\(hen\\|rivial\\)\\|"
+       "u\\(se\\|n\\(do\\|fold\\(_hyp\\)?\\|lock\\)\\)\\|"
        "with"
        "\\)[ \t.]")
       '(0 'font-lock-type-face t))))
@@ -86,12 +86,12 @@
 ;  "If non nil: Overrides default Phox-Sym-Lock patterns for PhoX.")
 
 (defun phox-sym-lock-start ()
-        (if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled)
-            (progn
-              (setq phox-sym-lock-color
-                    (face-foreground 'font-lock-function-name-face))
-              (if (not phox-sym-lock-keywords)
-                  (phox-sym-lock phox-sym-lock-keywords-table)))))
+	(if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled)
+	    (progn
+	      (setq phox-sym-lock-color
+		    (face-foreground 'font-lock-function-name-face))
+	      (if (not phox-sym-lock-keywords)
+		  (phox-sym-lock phox-sym-lock-keywords-table)))))
 
 
 (provide 'phox-font)
diff --git a/phox/phox-fun.el b/phox/phox-fun.el
index 82531470..ded13ed0 100644
--- a/phox/phox-fun.el
+++ b/phox/phox-fun.el
@@ -1,5 +1,4 @@
-
-;; $State$ $Date$ $Revision$ 
+;; $State$ $Date$ $Revision$
 ;; syntax
 
 (setq
@@ -16,28 +15,28 @@
  phox-ident-regexp "\\(\\([^() \n\t\r=\\[.]\\|\\(\\.[^() \n\t\r]\\)\\)+\\)"
  phox-inductive-option "\\(\\[[^]]*]\\)?"
  phox-spaces-regexp "[ \n\t\r]*"
- phox-sy-definition-regexp (concat 
+ phox-sy-definition-regexp (concat
    "\\(Cst\\|\\(def\\(rec\\)?\\)\\)"
    phox-comments-regexp
-   "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)") 
- phox-sy-inductive-regexp (concat 
+   "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)")
+ phox-sy-inductive-regexp (concat
    "Inductive"
    phox-comments-regexp
    phox-inductive-option
    phox-comments-regexp
-   "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)") 
- phox-inductive-regexp (concat 
+   "\\(\\(rInfix\\|lInfix\\|Infix\\|Prefix\\|Postfix\\)[^\"]+\"\\([^\"]+\\)\\)")
+ phox-inductive-regexp (concat
    "Inductive"
    phox-comments-regexp
    phox-inductive-option
    phox-comments-regexp
-   phox-ident-regexp) 
- phox-data-regexp (concat 
+   phox-ident-regexp)
+ phox-data-regexp (concat
    "\\(Data\\|type\\)"
    phox-comments-regexp
    phox-inductive-option
    phox-comments-regexp
-   phox-ident-regexp) 
+   phox-ident-regexp)
  phox-definition-regexp (concat
    "\\(Cst\\|def\\(_thlist\\|rec\\)?\\|claim\\|Sort\\)"
    phox-comments-regexp
@@ -66,7 +65,7 @@
 
 
 (defun phox-init-syntax-table (&optional TABLE)
-  "Set appropriate values for syntax table in current buffer, 
+  "Set appropriate values for syntax table in current buffer,
 or for optional argument TABLE."
 ;; useful for using forward-word
   (modify-syntax-entry ?_  "w" TABLE)
@@ -172,72 +171,72 @@ or for optional argument TABLE."
 
 (defun phox-find-and-forget (span)
   (let (str ans tmp (lsp -1) name sname) ;; da: added name,sname.  are tmp/lsp not used?
-    (while span 
+    (while span
       (setq str (span-property span 'cmd))
 
       (cond
 
-       ((eq (span-property span 'type) 'comment))       
+       ((eq (span-property span 'type) 'comment))
 
        ((eq (span-property span 'type) 'proverproc))
 
        ((eq (span-property span 'type) 'goalsave)
 	(if (proof-string-match phox-prove-claim-regexp str)
-	    (setq ans (concat (format phox-forget-proof-command 
+	    (setq ans (concat (format phox-forget-proof-command
 				      (match-string 4 str)) ans))
 	  (setq ans (concat (format phox-forget-id-command
 				    (span-property span 'name)) ans))))
 
        ((proof-string-match phox-new-elim-regexp str)
-	(setq ans 
-	      (concat (format phox-forget-new-elim-command 
+	(setq ans
+	      (concat (format phox-forget-new-elim-command
 				  (match-string 3 str)) ans)))
 
        ((proof-string-match phox-new-intro-regexp str)
-	(setq ans 
-	      (concat (format phox-forget-new-intro-command 
+	(setq ans
+	      (concat (format phox-forget-new-intro-command
 				  (match-string 3 str)) ans)))
 
        ((proof-string-match phox-new-rewrite-regexp str) ; deprecated
-	(setq ans 
-	      (concat (format phox-forget-new-equation-command 
+	(setq ans
+	      (concat (format phox-forget-new-equation-command
 				  (match-string 3 str)) ans)))
 
        ((proof-string-match phox-new-equation-regexp str)
-	(setq ans 
-	      (concat (format phox-forget-new-equation-command 
+	(setq ans
+	      (concat (format phox-forget-new-equation-command
 				  (match-string 3 str)) ans)))
 
        ((proof-string-match phox-close-def-regexp str)
-	(setq ans 
-	      (concat (format phox-forget-close-def-command 
+	(setq ans
+	      (concat (format phox-forget-close-def-command
 				  (match-string 4 str)) ans)))
 
        ((proof-string-match phox-sy-definition-regexp str)
-	(setq ans 
-	      (concat (format phox-forget-id-command 
+	(setq ans
+	      (concat (format phox-forget-id-command
 				  (concat "$" (match-string 7 str))) ans)))
 
        ((proof-string-match phox-sy-inductive-regexp str)
-	(setq ans 
-	      (concat (format phox-forget-id-command 
+	(setq ans
+	      (concat (format phox-forget-id-command
 				  (concat "$" (match-string 10 str))) ans)))
 
        ((proof-string-match phox-inductive-regexp str)
-	(setq ans 
-	      (concat (format phox-forget-id-command 
+	(setq ans
+	      (concat (format phox-forget-id-command
 				  (match-string 8 str)) ans)))
 
        ((proof-string-match phox-data-regexp str)
 	(setq
 	  name (match-string 8 str)
-          sname (concat (downcase (substring name 0 1)) 
+	  sname (concat (downcase (substring name 0 1))
 			(substring name 1 nil))
-	  ans (concat (format phox-forget-id-command 
+	  ans (concat (format phox-forget-id-command
 			      sname) ans)))
 
        ((proof-string-match phox-definition-regexp str)
-	(setq ans (concat (format phox-forget-id-command 
+	(setq ans (concat (format phox-forget-id-command
 				      (match-string 6 str)) ans))))
 
       (setq lsp (span-start span))
@@ -268,7 +267,7 @@ If inside a comment, just process until the start of the comment."
 ;; function, and appear in the submenu  "State" [pr].
 
 (defun phox-depend-theorem(theorem)
-  "Interactive function : 
+  "Interactive function :
 ask for a string and  and send a depend command to PhoX for it.
 
 Gives the list of all axioms which have been used to prove the theorem."
@@ -277,8 +276,8 @@ Gives the list of all axioms which have been used to prove the theorem."
 (proof-shell-invisible-command (concat "depend " theorem)))
 
 (defun phox-eshow-extlist(extlist)
-  "Interactive function : 
-ask for a string and send an eshow command to PhoX for it. 
+  "Interactive function :
+ask for a string and send an eshow command to PhoX for it.
 
 Shows the given extension-list.  Possible extension lists are : equation
 (the list of equations added to unification introduced by the new_equation
@@ -291,7 +290,7 @@ introduced by the new_elim and new_intro {-t} commands), closed
 (proof-shell-invisible-command (concat "eshow " extlist)))
 
 (defun phox-flag-name(name)
-"Interactive function : 
+"Interactive function :
 ask for a string and send a flag command  to PhoX for it.
 
   Print the value of an internal flag of the
@@ -302,7 +301,7 @@ ask for a string and send a flag command  to PhoX for it.
 
 
 (defun phox-path()
-"Interactive function : 
+"Interactive function :
  send a path command to PhoX.
 
   Prints the list of all paths. This path list is used to find
@@ -313,20 +312,20 @@ ask for a string and send a flag command  to PhoX for it.
 (proof-shell-invisible-command  "path"))
 
 (defun phox-print-expression(expr)
-"Interactive function : 
+"Interactive function :
 ask for a string and send a print command  to PhoX for it.
 
   In case argument expr
   is a closed expression of the language in use, prints it and gives its
   sort, gives an (occasionally) informative error message otherwise. In
-  case expr is a defined expression (constant, theorem ...) 
+  case expr is a defined expression (constant, theorem ...)
   gives  the definition."
 
 (interactive "sexpr: ")
 (proof-shell-invisible-command (concat "print " expr)))
 
 (defun phox-print-sort-expression(expr)
-"Interactive function : 
+"Interactive function :
 ask for a string and send a print_sort command  to PhoX for it.
 
   Similar to print, but gives more information on sorts of bounded
@@ -337,7 +336,7 @@ ask for a string and send a print_sort command  to PhoX for it.
 
 
 (defun phox-priority-symbols-list(symblist)
-"Interactive function : 
+"Interactive function :
 ask for a string and send a priority command  to PhoX for it.
 
   Print the priority of the given symbols. If no symbol are
@@ -349,22 +348,22 @@ ask for a string and send a priority command  to PhoX for it.
 
 
 (defun phox-search-string(string type)
-  "Interactive function: 
+  "Interactive function:
 ask for a string and possibly a type and send a search command to PhoX for it.
 
  Prints the list of all loaded symbols which have type and whose name
  contains the string. If no type is given, it prints all symbols whose
  name contains string."
 
-(interactive 
-"sstring : 
+(interactive
+"sstring :
 stype (nothing for any type, 'a as type parameter) :")
 (proof-shell-invisible-command (concat "search \"" string "\" " type)))
 
 ;; The followings are proof commands (doc in cmd_proof.tex) :
 
 (defun phox-constraints()
-"Interactive function : 
+"Interactive function :
  send a constraints command to PhoX.
 
   Prints the  constraints which should be fulfilled by unification variables,
@@ -375,7 +374,7 @@ stype (nothing for any type, 'a as type parameter) :")
 (proof-shell-invisible-command  "constraints"))
 
 (defun phox-goals()
-"Interactive function : 
+"Interactive function :
  send a goals command to PhoX.
 
   Prints the list of all remaining goals, only works in proofs."
@@ -412,13 +411,13 @@ stype (nothing for any type, 'a as type parameter) :")
 ;; obsolète probablement, sinon à modifier pour en étendre la portée.
 
 (defun phox-delete-symbol(symbol)
-  "Interactive function : 
+  "Interactive function :
 ask for a symbol and send a delete command to PhoX for it."
   (interactive "ssymbol : ")
   (proof-shell-invisible-command (concat "del " symbol)))
 
 (defun phox-delete-symbol-on-cursor()
-"Interactive function : 
+"Interactive function :
 send a delete command to PhoX for the symbol whose name is under the cursor."
   (interactive)
   (let (start end)
@@ -434,6 +433,3 @@ send a delete command to PhoX for the symbol whose name is under the cursor."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 (provide 'phox-fun)
-
-
-    
diff --git a/phox/phox-lang.el b/phox/phox-lang.el
index a67941e4..a83328b8 100644
--- a/phox/phox-lang.el
+++ b/phox/phox-lang.el
@@ -1,9 +1,10 @@
-;; $State$ $Date$ $Revision$ 
+;; $State$ $Date$ $Revision$
 ;;--------------------------------------------------------------------------;;
 ;;--------------------------------------------------------------------------;;
 ;; messages in various languages
 
 (provide 'phox-lang)
+(require 'cl)				; for case
 
 (defvar phox-lang
   (let* ((s1 (getenv "LANG")) (s2 (getenv "LC_LANG")) (s (substring (if s1 s1 (if s2 s2 "en")) 0 2)))
@@ -12,9 +13,9 @@
       ((string= s "fr") 'fr)
       (t 'en))))
 
- 
+
 (defun phox-lang-absurd ()
-  (case phox-lang 
+  (case phox-lang
     (en "By absurd")
     (fr "Par l'absurde")))
 
@@ -24,7 +25,7 @@
     (fr (concat  "Supprimer l'hypothèse " s " (si elle est devenue inutile)"))))
 
 (defun phox-lang-opendef ()
-  (case phox-lang 
+  (case phox-lang
     (en "Expand the definition: ")
     (fr "Ouvre la définition : ")))
 
@@ -49,11 +50,11 @@
     (fr (concat  "Dévérouille la variable " s))))
 
 (defun phox-lang-prove (s)
-  (case phox-lang 
+  (case phox-lang
     (en (concat "Let us prove \\[" s "\\]"))
     (fr (concat "Prouvons \\[" s "\\]"))))
 
 (defun phox-lang-let (s)
-  (case phox-lang 
+  (case phox-lang
     (en (concat "Let \\[ \\] = \\[" s "\\]"))
     (fr (concat "Définissons \\[ \\] = \\[" s "\\]"))))
diff --git a/phox/phox-outline.el b/phox/phox-outline.el
index 766bddb3..329e2421 100644
--- a/phox/phox-outline.el
+++ b/phox/phox-outline.el
@@ -7,20 +7,20 @@
 (setq phox-outline-title-regexp "\\((\\*[ \t\n]*title =\\)")
 (setq phox-outline-section-regexp "\\((\\*\\*+\\)")
 (setq phox-outline-save-regexp "\\((\\*#\\)")
-(setq 
- phox-outline-theo-regexp 
+(setq
+ phox-outline-theo-regexp
  "\\((\\*lem\\)\\|\\((\\*prop\\)\\|\\((\\*fact\\)\\|\\((\\*theo\\)\\|\\((\\*def\\)\\|\\((\\*cst\\)")
-(setq 
- phox-outline-theo2-regexp 
+(setq
+ phox-outline-theo2-regexp
  "\\(lem\\)\\|\\(prop\\)\\|\\(fact\\)\\|\\(theo\\)\\|\\(def\\)\\|\\(cst\\)\\|\\(claim\\)\\|\\(new_\\)")
 
-(setq 
-  phox-outline-regexp 
-  (concat 
-   phox-outline-title-regexp "\\|" 
-   phox-outline-section-regexp "\\|" 
-   phox-outline-save-regexp "\\|" 
-   phox-outline-theo-regexp "\\|" 
+(setq
+  phox-outline-regexp
+  (concat
+   phox-outline-title-regexp "\\|"
+   phox-outline-section-regexp "\\|"
+   phox-outline-save-regexp "\\|"
+   phox-outline-theo-regexp "\\|"
    phox-outline-theo2-regexp))
 
 (setq phox-outline-heading-end-regexp "\\(\\*)[ \t]*\n\\)\\|\\(\\.[ \t]*\n\\)")
diff --git a/phox/phox-pbrpm.el b/phox/phox-pbrpm.el
index 9c7411f3..5e831938 100644
--- a/phox/phox-pbrpm.el
+++ b/phox/phox-pbrpm.el
@@ -1,4 +1,4 @@
-;; $State$ $Date$ $Revision$ 
+;; $State$ $Date$ $Revision$
 ;;--------------------------------------------------------------------------;;
 ;;--------------------------------------------------------------------------;;
 ;; the proof by rules popup menu part
@@ -43,15 +43,15 @@
   "build a menu from a string send by phox"
   (setq str (proof-shell-invisible-cmd-get-result str))
   (if (string= str "") nil
-    (mapcar 
-     (lambda (s) (append (list order) (split-string s "\\\\-") 
+    (mapcar
+     (lambda (s) (append (list order) (split-string s "\\\\-")
 			      (list 'phox-pbrpm-rename-in-cmd)))
      (split-string str "\\\\\\\\"))))
 
 (defun phox-pbrpm-rename-in-cmd (cmd spans)
   (let ((modified nil) (prev 0))
-    (mapc (lambda (span) 
-	    (if (not (string=  (span-property span 'original-text) 
+    (mapc (lambda (span)
+	    (if (not (string=  (span-property span 'original-text)
 			       (span-string span)))
 		(setq modified (cons span modified)))) spans)
     (setq modified (reverse modified))
@@ -61,8 +61,8 @@
 	      (progn
 		(while (and modified (= 0 (span-property (car modified) 'goalnum)))
 		  (let ((span (pop modified)))
-		    (setq cmd (concat cmd ";; rename " 
-				      (span-property span 'original-text) " " 
+		    (setq cmd (concat cmd ";; rename "
+				      (span-property span 'original-text) " "
 				      (span-string span)))))
 		(if modified (setq cmd (concat "(" cmd ")")))))
 	  (if modified (setq cmd (concat cmd ";; ")))
@@ -72,7 +72,7 @@
 	      (while (< (+ prev 1) goalnum)
 		(setq cmd (concat cmd "idt @+@ "))
 		(setq prev (+ prev 1)))
-	      (setq cmd (concat cmd "(rename " (span-property span 'original-text) " " 
+	      (setq cmd (concat cmd "(rename " (span-property span 'original-text) " "
 				      (span-string span)))
 	      (setq prev goalnum)
 	      (if (or (not modified) (< goalnum (span-property (car modified) 'goalnum)))
@@ -80,7 +80,7 @@
 		(setq cmd (concat cmd ";; ")))))
 	  (if (> prev 0) (setq cmd (concat cmd "idt"))))))
   cmd)
-	
+
 (defun phox-pbrpm-get-region-name (region-info)
       (if (= (nth 0 region-info) 1) (nth 1 region-info) (nth 2 region-info)))
 
@@ -96,11 +96,11 @@
    (let
      ((pbrpm-rules-list nil)
       (goal-prefix
-       (if (= (nth 0 click-infos) 1) "" 
+       (if (= (nth 0 click-infos) 1) ""
 	 (concat "["
 		 (int-to-string (nth 0 click-infos))
 		 "] "))))
- 
+
 
    ; the first goal is the selected one by default, so we prefer not to display it.
 
@@ -123,13 +123,13 @@
    ; if clicking a conclusion with a selection
    (if (and (string= (nth 1 click-infos) "none") region-infos)
        (setq pbrpm-rules-list
-         (append pbrpm-rules-list
+	 (append pbrpm-rules-list
 		 (phox-pbrpm-menu-from-string 0
 			 (concat "menu_intro "
-				 (int-to-string (nth 0 click-infos))	
+				 (int-to-string (nth 0 click-infos))
 				 (let ((tmp ""))
 				   (mapc (lambda (region-info)
-					   (setq tmp 
+					   (setq tmp
 						 (concat tmp " " (phox-pbrpm-escape-string (nth 2 region-info)))))
 					 region-infos)
 				   tmp)))
@@ -138,7 +138,7 @@
 			       (int-to-string (nth 0 click-infos)) " "
 			       (let ((tmp ""))
 				 (mapc (lambda (region-info)
-					 (setq tmp 
+					 (setq tmp
 					       (concat tmp " " (phox-pbrpm-escape-string (phox-pbrpm-get-region-name region-info)))))
 				       region-infos)
 				 tmp))))))
@@ -158,7 +158,7 @@
 			 (if (char= (string-to-char r) ?t)
 			     (list
 			      (list 9 (phox-lang-suppress (nth 1 click-infos))
-				    (concat "[" (int-to-string (nth 0 click-infos)) "] " 
+				    (concat "[" (int-to-string (nth 0 click-infos)) "] "
 					    "rmh " (nth 1 click-infos))))
 			   nil)
 			 (phox-pbrpm-menu-from-string 1
@@ -176,19 +176,19 @@
 							       (nth 1 click-infos)))))))
 
    ; if clicking on an hypothesis with a selection
-   (if (and         
+   (if (and
 	(not (or (string= (nth 1 click-infos) "none")
 		 (string= (nth 1 click-infos) "whole")))
 	region-infos)
        (setq pbrpm-rules-list
-         (append pbrpm-rules-list
+	 (append pbrpm-rules-list
 		 (phox-pbrpm-menu-from-string 1
 		       (concat "menu_apply "
 			       (int-to-string (nth 0 click-infos)) " "
 			       (nth 1 click-infos)
 			       (let ((tmp ""))
 				 (mapc (lambda (region-info)
-					 (setq tmp 
+					 (setq tmp
 					       (concat tmp " " (phox-pbrpm-escape-string (nth 2 region-info)))))
 				       region-infos)
 				 tmp)))
@@ -198,7 +198,7 @@
 			       (nth 1 click-infos)
 			       (let ((tmp ""))
 				 (mapc (lambda (region-info)
-					 (setq tmp 
+					 (setq tmp
 					       (concat tmp " " (phox-pbrpm-escape-string (phox-pbrpm-get-region-name region-info)))))
 				       region-infos)
 				 tmp))))))
@@ -207,12 +207,12 @@
 	    region-infos (not (cdr region-infos)))
        (setq pbrpm-rules-list
 	     (append pbrpm-rules-list
-		     (list (list 0 (concat 
+		     (list (list 0 (concat
 				    (phox-lang-instance (nth 2 click-infos))
 				    (nth 2 (car region-infos)))
-				 (concat 
+				 (concat
 				  "instance "
-				  (nth 2 click-infos) 
+				  (nth 2 click-infos)
 				  " "
 				  (nth 2 (car region-infos))))))))
 
@@ -220,13 +220,13 @@
 	    (not region-infos))
        (setq pbrpm-rules-list
 	     (append pbrpm-rules-list
-		     (list (list 0 (concat 
+		     (list (list 0 (concat
 				    (phox-lang-open-instance (nth 2 click-infos)))
-				 (concat 
+				 (concat
 				  "instance "
-				  (nth 2 click-infos) 
+				  (nth 2 click-infos)
 				  " ")
-			  (lambda (cmd spans) 
+			  (lambda (cmd spans)
 			    (let ((span (pop spans)))
 			      (concat cmd " " (span-string span)))))))))
 
@@ -234,8 +234,8 @@
    (if (and (not region-infos) (not (string= (nth 2 click-infos) "")))
        (let ((r (proof-shell-invisible-cmd-get-result (concat "is_definition "
 							      (int-to-string (nth 0 click-infos))
-							      " " 
-                                                              (phox-pbrpm-escape-string (nth 2 click-infos)))))
+							      " "
+							      (phox-pbrpm-escape-string (nth 2 click-infos)))))
 	     (ri (proof-shell-invisible-cmd-get-result (concat "is_definition "
 							      (int-to-string (nth 0 click-infos))
 							      " "
@@ -243,14 +243,14 @@
 	 (if (or (char= (string-to-char r) ?t) (char= (string-to-char ri) ?t))
 	     (setq pbrpm-rules-list
 		   (append pbrpm-rules-list
-			   (list (list 1 (concat 
+			   (list (list 1 (concat
 					(phox-lang-opendef)
 					(nth 2 click-infos))
-				       (concat 
+				       (concat
 					goal-prefix
-					(if (or (string= (nth 1 click-infos) "none") 
+					(if (or (string= (nth 1 click-infos) "none")
 						(string= (nth 1 click-infos) "whole"))
-					    "unfold -ortho " 
+					    "unfold -ortho "
 					  (concat "unfold_hyp " (nth 1 click-infos) " -ortho "))
 					"$"
 					(nth 2 click-infos))))))
@@ -261,14 +261,14 @@
 		     (setq pbrpm-rules-list
 			   (append pbrpm-rules-list
 				   (list (list 0 (phox-lang-unlock (nth 2 click-infos))
-					 (concat 
+					 (concat
 					  goal-prefix
 					  "unlock "
 					  (nth 2 click-infos))))))
 		     (setq pbrpm-rules-list
 			   (append pbrpm-rules-list
 				   (list (list 0 (phox-lang-lock (nth 2 click-infos))
-					 (concat 
+					 (concat
 					  goal-prefix
 					  "lock "
 					  (nth 2 click-infos))))))))))))
@@ -278,12 +278,12 @@
 	   (append pbrpm-rules-list
 		   (list
 		    (list 10 "Trivial ?" (concat goal-prefix "trivial"))
-		    (list 10 (phox-lang-prove arg) (concat goal-prefix "prove") 
-			  (lambda (cmd spans) 
+		    (list 10 (phox-lang-prove arg) (concat goal-prefix "prove")
+			  (lambda (cmd spans)
 			    (let ((span (pop spans)))
 			      (concat cmd " " (span-string span)))))
-		    (list 10 (phox-lang-let arg) (concat goal-prefix "local") 
-			  (lambda (cmd spans) 
+		    (list 10 (phox-lang-let arg) (concat goal-prefix "local")
+			  (lambda (cmd spans)
 			    (let ((span1 (pop spans)) (span2 (pop spans)))
 			      (concat cmd " " (span-string span1) " = "(span-string span2)))))))))
 
diff --git a/phox/phox-sym-lock.el b/phox/phox-sym-lock.el
index e13f56a8..38d93441 100644
--- a/phox/phox-sym-lock.el
+++ b/phox/phox-sym-lock.el
@@ -16,14 +16,14 @@
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;                                 History
-;; 
+;;
 ;; first prototype by wg <wg@cs.tu-berlin.de> 5-96
 ;; tweaked by Steve Dunham <dunham@gdl.msu.edu> 5-96
 ;; rewritten and enhanced by Albert Cohen <Albert.Cohen@prism.uvsq.fr> 3-97
 ;; new symbol-face format and ergonomy improvement by Albert Cohen 2-98
 ;; major step towards portability and customization by Albert Cohen 5-98
 ;; removed bug with multiple appends in hook by Albert Cohen 3-99
-;; removed phox-sym-lock-face&atom which where not working by C Raffalli 4-2000 
+;; removed phox-sym-lock-face&atom which where not working by C Raffalli 4-2000
 
 ;; more about symbol font ? check out: xfd -fn '-adobe-symbol-*--12-*'
 
@@ -76,14 +76,14 @@
   "Generate a new internal symbol."
   ;; where is the standard function to do this ?
   (setq phox-sym-lock-sym-count (+ phox-sym-lock-sym-count 1))
-  (intern (concat "phox-sym-lock-gen-" (or prefix "") 
+  (intern (concat "phox-sym-lock-gen-" (or prefix "")
 		  (int-to-string phox-sym-lock-sym-count))))
 
 
 (defun phox-sym-lock-make-symbols-atomic (&optional begin end)
   "Function to make symbol faces atomic."
   (if phox-sym-lock-enabled
-      (map-extents 
+      (map-extents
        (lambda (extent maparg)
 	 (let ((face (extent-face extent)) (ext))
 	   (if (and face (setq ext (face-property face 'phox-sym-lock-remap)))
@@ -128,7 +128,7 @@
 	  (lf (and (fboundp 'list-fonts) ; da: what is this function? not defined
 		   (list-fonts font-pat))))
     (while (and lf maxsize)
-      (if 
+      (if
 	  (string-match font-reg
 		    (car lf))
 	  (let ((str-size (substring (car lf) (match-beginning 1)
@@ -171,8 +171,8 @@
 ;;			  'final 53
 ;; DA PG 3.7: above line doesn't work on XEmacs 21.5b28, gives
 ;; Character set already defined for this DIMENSION/CHARS/FINAL/DIRECTION combo (indian-is13194)
-;; DA: Will 55 work?  
-			  'final 55 
+;; DA: Will 55 work?
+			  'final 55
 			  'graphic 0))
       (make-charset 'phox-sym-lock-cset-right "Char set for symbol font"
 		    (list 'registry "adobe-fontspecific"
@@ -180,10 +180,10 @@
 			  'chars 94
 			  'final 54
 			  'graphic 1))
-      (set-face-property 'phox-sym-lock-adobe-symbol-face 
+      (set-face-property 'phox-sym-lock-adobe-symbol-face
 			 'font phox-sym-lock-font-name nil
 			 ;; DA: removed next line, it breaks "make magic" in doc
-			 ;; '(mule-fonts) 'prepend,   
+			 ;; '(mule-fonts) 'prepend,
 			 ))
   (set-face-font 'phox-sym-lock-adobe-symbol-face phox-sym-lock-font-name 'global))
 
@@ -243,7 +243,7 @@ the empty string. OBJ may either be a string or a character."
     (fillarray table "")
     (set-face-property tface 'display-table table)
     (set-face-property tface 'phox-sym-lock-remap 1) ; mark it
-    tface 
+    tface
     ;; return face value and not face name
     ;; the temporary face would be otherwise GCed
     ))
@@ -259,7 +259,7 @@ face's extent will become atomic."
 
 (defun phox-sym-lock-rec (fl)
   (let ((f (car fl)))
-    (if f 	      
+    (if f
 	(cons (apply 'phox-sym-lock-atom-face f)
 	      (phox-sym-lock-rec (cdr fl))))))
 
@@ -333,7 +333,7 @@ OBJ under `phox-sym-lock-adobe-symbol-face'. The face extent will become atomic.
 		   ["Phox-Sym-Lock"
 		    (if phox-sym-lock-enabled (phox-sym-lock-disable) (phox-sym-lock-enable))
 		    :style toggle :selected phox-sym-lock-enabled
-		    :active phox-sym-lock-keywords] "Automatic")  
+		    :active phox-sym-lock-keywords] "Automatic")
   (if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled
 	   font-lock-defaults (boundp 'phox-sym-lock-keywords))
       (progn
@@ -345,8 +345,8 @@ OBJ under `phox-sym-lock-adobe-symbol-face'. The face extent will become atomic.
       (and
        (featurep 'font-lock)
        (if font-lock-auto-fontify
-           (not (memq major-mode font-lock-mode-disable-list))
-         (memq major-mode font-lock-mode-enable-list))
+	   (not (memq major-mode font-lock-mode-disable-list))
+	 (memq major-mode font-lock-mode-enable-list))
        (font-lock-set-defaults-1 explicit-defaults)
        (phox-sym-lock-patch-keywords))
     (turn-on-font-lock)))
diff --git a/phox/phox-tags.el b/phox/phox-tags.el
index 70a4fb2a..8ff2848d 100644
--- a/phox/phox-tags.el
+++ b/phox/phox-tags.el
@@ -1,4 +1,4 @@
-;; $State$ $Date$ $Revision$ 
+;; $State$ $Date$ $Revision$
 ;;--------------------------------------------------------------------------;;
 ;;--------------------------------------------------------------------------;;
 ;;                         gestion des TAGS
@@ -43,7 +43,7 @@
   (interactive)
   (phox-tags-add-table (concat phox-lib-dir "/TAGS"))
   )
- 
+
 (defun phox-tags-add-local-table()
   "Add the tags table created with function phox-create-local-table."
   (interactive)
@@ -53,8 +53,8 @@
 (defun phox-tags-create-local-table()
   "create table on local buffer"
   (interactive)
-  (shell-command (concat phox-etags 
-			 " -o " 
+  (shell-command (concat phox-etags
+			 " -o "
 			 (file-name-nondirectory (buffer-file-name))
 			 "TAGS "
 			 (file-name-nondirectory (buffer-file-name))))
@@ -85,6 +85,3 @@
 )
 
 (provide 'phox-tags)
-
-
-