phox is back

1 files changed, 13 insertions, 13 deletions

diff --git a/generic/proof-site.el b/generic/proof-site.el
index df17229d..70a517b2 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -7,7 +7,7 @@
 ;; $Id$
 ;;
 ;;; Commentary:
-;; 
+;;
 ;; Loading stubs and configuration for site and choice of provers.
 ;;
 ;; NB: Normally users do not need to edit this file.  Developers/installers
@@ -25,12 +25,12 @@
 ;;; Code:
 
 ;; Entries in proof-assistant-table-default are lists of the form
-;; 
+;;
 ;;   (SYMBOL NAME FILE-EXTENSION [AUTOMODE-REGEXP] [IGNORED-EXTENSIONS-LIST])
 ;;
 ;; FILE-EXTENSION is without dot ".". AUTOMODE-REGEXP is put into
 ;; auto-mode-alist, if it is not present, a regexp will be made up from
-;; FILE-EXTENSION. IGNORED-EXTENSIONS-LIST, if present, is appended to 
+;; FILE-EXTENSION. IGNORED-EXTENSIONS-LIST, if present, is appended to
 ;; completion-ignored-extensions. See proof-assistant-table for more info.
 ;;
 (defconst proof-assistant-table-default
@@ -40,10 +40,10 @@
       (isar "Isabelle" "thy")
       (coq "Coq" "v" nil (".vo" ".glob"))
       (easycrypt "EasyCrypt" "ec" "\\.eca?\\'")
+      (phox "PhoX" "phx" nil (".phi" ".pho"))
 
       ;; Obscure instances or conflict with other Emacs modes.
 
-      ;; (phox "PhoX" "phx")
       ;; (lego "LEGO" "l")
       ;; (ccc    "CASL Consistency Checker" "ccc")
 
@@ -54,7 +54,7 @@
       (pgshell	 "PG-Shell" "pgsh")
       (pgocaml	 "PG-OCaml" "pgml")
       (pghaskell "PG-Haskell" "pghci")
-      
+
       ;; Incomplete/obsolete:
 
       ;; (hol98	"HOL" "sml")
@@ -296,21 +296,21 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'."
        (run-hooks 'proof-ready-for-assistant-hook))))))
 
 
-(defvar proof-general-configured-provers 
+(defvar proof-general-configured-provers
   (or (mapcar 'intern (split-string (or (getenv "PROOFGENERAL_ASSISTANTS") "")))
       proof-assistants
       (mapcar (lambda (astnt) (car astnt)) proof-assistant-table))
   "A list of the configured proof assistants.
 Set on startup to contents of environment variable PROOFGENERAL_ASSISTANTS,
 the lisp variable `proof-assistants', or the contents of `proof-assistant-table'.")
-  
+
 ;; Add auto-loads and load-path elements to support the
 ;; proof assistants selected, and define stub major mode functions
 (let ((assistants proof-general-configured-provers))
   (while assistants
     (let*
 	((assistant (car assistants))	; compiler bogus warning here
-	 (tableentry 
+	 (tableentry
 	  (or (assoc assistant
 		     proof-assistant-table)
 	      (error "Symbol %s is not in proof-assistant-table (in proof-site)"
@@ -370,16 +370,16 @@ the lisp variable `proof-assistants', or the contents of `proof-assistant-table'
 ;;
 
 (defun proof-chose-prover (prompt)
-  (completing-read prompt 
-		   (mapcar 'symbol-name 
+  (completing-read prompt
+		   (mapcar 'symbol-name
 			   proof-general-configured-provers)))
 
 (defun proofgeneral (prover)
   "Start proof general for prover PROVER."
   (interactive
    (list (proof-chose-prover "Start Proof General for theorem prover: ")))
-  (proof-ready-for-assistant (intern prover) 
-			     (nth 1 (assoc (intern prover) 
+  (proof-ready-for-assistant (intern prover)
+			     (nth 1 (assoc (intern prover)
 					   proof-assistant-table-default)))
   (require (intern prover)))
 
@@ -391,7 +391,7 @@ the lisp variable `proof-assistants', or the contents of `proof-assistant-table'
 		     prover "/example."
 		     (nth 2 (assoc (intern prover) proof-assistant-table-default)))))
 
-		     
+
 
 
 (provide 'proof-site)