From 06d72fb68fd9dd57632650f1a79de01317a6069f Mon Sep 17 00:00:00 2001 From: Christophe Raffalli Date: Fri, 22 Sep 2017 00:28:27 +0200 Subject: phox is back --- generic/proof-site.el | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'generic') 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) -- cgit v1.2.3