diff options
Diffstat (limited to 'generic/proof-site.el')
| -rw-r--r-- | generic/proof-site.el | 59 |
1 files changed, 33 insertions, 26 deletions
diff --git a/generic/proof-site.el b/generic/proof-site.el index 671c3c82..e339d022 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -1,13 +1,20 @@ -;; proof-site.el -- Loading stubs for Proof General. -;; -;; Copyright (C) 1998-2003 LFCS Edinburgh. +;;; proof-site.el --- Loading stubs for Proof General. + +;; This file is part of Proof General. + +;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh +;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $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 +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 @@ -39,11 +46,11 @@ (isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) - (easycrypt "EasyCrypt" "ec" ".*\\.eca?") + (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 +61,7 @@ (pgshell "PG-Shell" "pgsh") (pgocaml "PG-OCaml" "pgml") (pghaskell "PG-Haskell" "pghci") - + ;; Incomplete/obsolete: ;; (hol98 "HOL" "sml") @@ -73,7 +80,7 @@ (eval-and-compile ;; WARNING: do not edit next line (constant is edited in Makefile.devel) - (defconst proof-general-version "Proof General Version 4.4.1~pre." + (defconst proof-general-version "Proof General Version 4.5-git." "Version string identifying Proof General release.")) (defconst proof-general-short-version @@ -149,7 +156,7 @@ You can use customize to set this variable." ;; (defun proof-add-to-load-path (dir) - "Add DIR to `load-path' if not contained already" + "Add DIR to `load-path' if not contained already." (add-to-list 'load-path dir)) (proof-add-to-load-path (concat proof-home-directory "generic/")) @@ -163,7 +170,7 @@ You can use customize to set this variable." (require 'proof-autoloads) (eval-when-compile - (defvar Info-dir-contents nil)) + (defvar Info-dir-contents)) ;; Add the info directory to the Info path (if (file-exists-p proof-info-directory) ; for safety @@ -199,10 +206,10 @@ Each entry is a list of the form The NAME is a string, naming the proof assistant. The SYMBOL is used to form the name of the mode for the assistant, `SYMBOL-mode', run when files with AUTOMODE-REGEXP -\(or with extension FILE-EXTENSION) are visited. If present, +\(or with extension FILE-EXTENSION) are visited. If present, IGNORED-EXTENSIONS-LIST is a list of file-name extensions to be ignored when doing file-name completion (IGNORED-EXTENSIONS-LIST -is added to completion-ignored-extensions). +is added to ‘completion-ignored-extensions’). SYMBOL is also used to form the name of the directory and elisp file for the mode, which will be @@ -296,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'.") - +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 +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))) @@ -391,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) |