diff options
author | Erik Martin-Dorel <erik@martin-dorel.org> | 2018-08-22 23:29:35 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-22 23:29:35 +0200 |
commit | 26b3bf9f070e9aee45c6e3d19bca475d4ae8ed37 (patch) | |
tree | 64b5b138c91b75c464e66eecd5dc19542ad68276 /generic | |
parent | 3b9e1e4742a2dafce6ac2ef4bfa95d22e43c3c59 (diff) | |
parent | 7ee9486a616b12ea99490b134c1417792ef78459 (diff) |
Merge pull request #200 from craff/master
Update phox support
Diffstat (limited to 'generic')
-rw-r--r-- | generic/proof-site.el | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/generic/proof-site.el b/generic/proof-site.el index c7d721cd..dccc32a9 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -14,7 +14,7 @@ ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;;; Commentary: -;; +;; ;; Loading stubs and configuration for site and choice of provers. ;; ;; NB: Normally users do not need to edit this file. Developers/installers @@ -32,12 +32,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 @@ -47,10 +47,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") @@ -61,7 +61,7 @@ (pgshell "PG-Shell" "pgsh") (pgocaml "PG-OCaml" "pgml") (pghaskell "PG-Haskell" "pghci") - + ;; Incomplete/obsolete: ;; (hol98 "HOL" "sml") @@ -303,21 +303,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)" @@ -377,16 +377,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))) @@ -398,7 +398,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) |