diff options
| -rw-r--r-- | coq/coq.el | 2 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 4 | ||||
| -rw-r--r-- | etc/ProofGeneral.patch | 6 | ||||
| -rw-r--r-- | generic/proof-config.el | 37 | ||||
| -rw-r--r-- | generic/proof-script.el | 11 | ||||
| -rw-r--r-- | generic/proof-site.el | 52 | ||||
| -rw-r--r-- | generic/proof-splash.el | 12 | ||||
| -rw-r--r-- | generic/proof-toolbar.el | 4 | ||||
| -rw-r--r-- | isa/isa.el | 4 | ||||
| -rw-r--r-- | lego/lego.el | 2 |
10 files changed, 64 insertions, 70 deletions
@@ -330,7 +330,7 @@ (setq proof-comment-start "(*") (setq proof-comment-end "*)") - (setq proof-www-home-page coq-www-home-page) + (setq proof-assistant-home-page coq-www-home-page) (setq proof-mode-for-script 'coq-mode) diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 6c0dcc6e..66ca6936 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -1256,7 +1256,7 @@ called myassistant. directory, to put the specific customization and associated files in. @item Add a file myassistant.el to the new directory. @item Edit proof-site.el to add a new entry to the - @var{proof-internal-assistants-table} variable. The new entry should + @var{proof-assistants-table} variable. The new entry should look like this: (myassistant "My New Assistant" "\\.myasst$") @@ -1266,7 +1266,7 @@ for the new mode as well as the directory and file where it loads from. The second is a string, naming the proof assistant. The third item is a regular expression to match names of proof script files for this assistant. See the documentation -of @var{proof-internal-assistants-table} for more details. +of @var{proof-assistants-table} for more details. @item Define the new modes in myassistant.el, by looking at the files for the currently supported assistants for example. Basically you need to define some modes using @code{define-derived-mode} diff --git a/etc/ProofGeneral.patch b/etc/ProofGeneral.patch index 0e7043d9..b0be5c97 100644 --- a/etc/ProofGeneral.patch +++ b/etc/ProofGeneral.patch @@ -19,15 +19,15 @@ diff -cr ProofGeneral.old/generic/proof-site.el ProofGeneral/generic/proof-site. *** 76,82 **** :group 'proof-internal) - (defcustom proof-internal-info-directory -! (concat proof-internal-home-directory "doc/") + (defcustom proof-info-directory +! (concat proof-home-directory "doc/") "*Where Proof General Info files are installed." :type 'directory :group 'proof-internal) --- 76,82 ---- :group 'proof-internal) - (defcustom proof-internal-info-directory + (defcustom proof-info-directory ! "/usr/info/" "*Where Proof General Info files are installed." :type 'directory diff --git a/generic/proof-config.el b/generic/proof-config.el index 1d501da1..51b11fbc 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -46,18 +46,18 @@ (defcustom proof-prog-name-ask-p nil "*If non-nil, query user which program to run for the inferior process." :type 'boolean - :group 'proof) + :group 'proof-general) (defcustom proof-one-command-per-line nil "*If non-nil, format for newlines after each proof command in a script." :type 'boolean - :group 'proof) + :group 'proof-general) (and (featurep 'toolbar) (defcustom proof-toolbar-wanted t "*Whether to use toolbar in proof mode." :type 'boolean - :group 'proof)) + :group 'proof-general)) (defcustom proof-toolbar-follow-mode 'follow "*Choice of how point moves with toolbar commands. @@ -69,7 +69,7 @@ If ignore, point is never moved after toolbar movement commands." (const :tag "Follow locked region" locked) (const :tag "Keep locked region displayed" follow) (const :tag "Never move" ignore)) - :group 'proof) + :group 'proof-general) ;; @@ -181,7 +181,7 @@ Could come either from proof assistant or Proof General itself." (defgroup prover-config nil "Configuration of Proof General for the prover in use." - :group 'proof-internal + :group 'proof-general-internals :prefix "proof-") ;; The variables in the "prover-config" (NB: not "proof config"!!) @@ -196,24 +196,17 @@ Could come either from proof assistant or Proof General itself." ;; not liable to work, because the prover specific elisp usually ;; overrides with a series of setq's in <assistant>-mode-config type ;; functions. This is why prover-config appears under the -;; proof-internal group. - -;; Note: The XEmacs customization menus would be nicer if the -;; variables in prover-config group were uniformly renamed -;; prover-config-* (and similarly for other variables/groups). -;; But it's somewhat of a horror in the code! - +;; proof-general-internal group. (defcustom proof-assistant "" "Name of the proof assistant Proof General is using. This is set automatically by the mode stub defined in proof-site, -from the name given in proof-internal-assistant-table." +from the name given in proof-assistant-table." :type 'string :group 'prover-config) - ;; ;; 2. The major modes used by Proof General. @@ -251,7 +244,7 @@ Suggestion: this can be set in the script mode configuration." ;; 3. Configuration for menus, user-level commands, etc. ;; -(defcustom proof-www-home-page "" +(defcustom proof-asssistant-home-page "" "Web address for information on proof assistant" :type 'string :group 'prover-config) @@ -439,7 +432,7 @@ This is used to handle nested goals allowed by some provers." (defgroup proof-shell nil "Settings for output from the proof assistant in the proof shell." :group 'prover-config - :prefix "proof-") + :prefix "proof-shell-") ;; @@ -661,13 +654,13 @@ data triggered by `proof-shell-retract-files-regexp'." "Root name for proof script mode. Used internally and in menu titles." :type 'string - :group 'proof-internal) + :group 'proof-general-internals) -(defcustom proof-general-home-page +(defcustom proof-proof-general-home-page "http://www.dcs.ed.ac.uk/home/proofgen" "*Web address for Proof General" :type 'string - :group 'proof-internal) + :group 'proof-general-internals) ;; FIXME: da: could we put these into another keymap already? ;; FIXME: da: it's offensive to experienced users to rebind global stuff @@ -683,7 +676,7 @@ Used internally and in menu titles." Elements of the list are tuples (k . f) where `k' is a keybinding (vector) and `f' the designated function." :type 'sexp - :group 'proof-internal) + :group 'proof-general-internals) @@ -712,7 +705,7 @@ return a non-nil value. Then (actf cmd string) is invoked. See the documentation of `proof-shell-process-output' for the required output format." :type '(cons (function function)) - :group 'prover-config) + :group 'proof-shell) (defcustom proof-activate-scripting-hook nil "Hook run when a buffer is switched into scripting mode. @@ -721,7 +714,7 @@ The current buffer will be the newly active scripting buffer. This hook may be useful for synchronizing with the proof assistant, for example, to switch to a new theory." :type '(repeat function) - :group 'prover-config) + :group 'proof-script) diff --git a/generic/proof-script.el b/generic/proof-script.el index 8fabb2b8..a45b45a2 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1285,9 +1285,9 @@ Start up the proof assistant if necessary." (defvar proof-help-menu `("Help" [,(concat proof-assistant " web page") - (browse-url proof-www-home-page) t] + (browse-url proof-assistant-home-page) t] ["Proof General home page" - (browse-url proof-general-home-page) t] + (browse-url proof-proof-general-home-page) t] ["Proof General Info" proof-info-mode t] ) "The Help Menu in Script Management.") @@ -1506,9 +1506,10 @@ finish setup which depends on specific proof assistant configuration." ;; older/non-existent customize doesn't have ;; this function. (if (fboundp 'customize-menu-create) - (list (customize-menu-create 'proof) - (customize-menu-create 'proof-internal - "Internals")) + (list (customize-menu-create 'proof-general) + (customize-menu-create + 'proof-general-internals + "Internals")) nil) ;; end UGLY COMPATIBILTY HACK ))) diff --git a/generic/proof-site.el b/generic/proof-site.el index 0b4eb909..8e775c70 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -18,7 +18,7 @@ ;; end UGLY COMPATIBILITY HACK -(defgroup proof nil +(defgroup proof-general nil "Customization of Proof General." :group 'external :group 'processes @@ -30,14 +30,14 @@ ;; configuration to different proof assistants. ;; This is for development purposes rather than ;; user-level customization, so this group does -;; not belong to 'proof (or any other group). -(defgroup proof-internal nil +;; not belong to 'proof-general (or any other group). +(defgroup proof-general-internals nil "Customization of Proof General internals." :prefix "proof-") ;; Master table of supported assistants. -(defcustom proof-internal-assistant-table +(defcustom proof-assistant-table '((isa "Isabelle" "\\.ML$\\|\\.thy$") (lego "LEGO" "\\.l$") (coq "Coq" "\\.v$")) @@ -58,12 +58,12 @@ directory and elisp file for the mode, which will be where `<proof-directory-home>/' is the value of the variable proof-directory-home." :type '(repeat (list symbol string string)) - :group 'proof-internal) + :group 'proof-general-internals) ;; Directories -(defcustom proof-internal-home-directory +(defcustom proof-home-directory ;; FIXME: make sure compiling does not evaluate next expression. (or (getenv "PROOFGENERAL_HOME") (let ((curdir @@ -76,19 +76,19 @@ Default value taken from environment variable PROOFGENERAL_HOME if set, otherwise based on where the file proof-site was loaded from. You can use customize to set this variable." :type 'directory - :group 'proof-internal) + :group 'proof-general-internals) -(defcustom proof-internal-images-directory - (concat proof-internal-home-directory "images/") +(defcustom proof-images-directory + (concat proof-home-directory "images/") "*Where Proof General image files are installed. Ends with slash." :type 'directory - :group 'proof-internal) + :group 'proof-general-internals) -(defcustom proof-internal-info-directory - (concat proof-internal-home-directory "doc/") +(defcustom proof-info-directory + (concat proof-home-directory "doc/") "*Where Proof General Info files are installed." :type 'directory - :group 'proof-internal) + :group 'proof-general-internals) ;; Add the info directory to the end of Emacs Info path if need be. ;; It's easier to do this after Info has loaded because of the @@ -96,10 +96,10 @@ You can use customize to set this variable." (eval-after-load "info" - '(or (member proof-internal-info-directory Info-directory-list) + '(or (member proof-info-directory Info-directory-list) (progn (setq Info-directory-list - (cons proof-internal-info-directory + (cons proof-info-directory Info-directory-list)) ;; Clear cache of info dir (setq Info-dir-contents nil)))) @@ -108,13 +108,13 @@ You can use customize to set this variable." ;; Might be nicer to have a boolean for each supported assistant. (defcustom proof-assistants (mapcar (lambda (astnt) (car astnt)) - proof-internal-assistant-table) + proof-assistant-table) (concat "*Choice of proof assitants to use with Proof General. A list of symbols chosen from:" (apply 'concat (mapcar (lambda (astnt) (concat " '" (symbol-name (car astnt)))) - proof-internal-assistant-table)) + proof-assistant-table)) ".\nEach proof assistant defines its own instance of Proof General, providing session control, script management, etc. Proof General will be started automatically for the assistants chosen here. @@ -124,12 +124,12 @@ NOTE: to change proof assistant, you must start a new Emacs session.") :type (cons 'set (mapcar (lambda (astnt) (list 'const ':tag (car (cdr astnt)) (car astnt))) - proof-internal-assistant-table)) - :group 'proof) + proof-assistant-table)) + :group 'proof-general) ;; Extend load path for the generic files. (let ((proof-lisp-path - (concat proof-internal-home-directory "generic/"))) + (concat proof-home-directory "generic/"))) (or (member proof-lisp-path load-path) (setq load-path (cons proof-lisp-path load-path)))) @@ -139,8 +139,8 @@ NOTE: to change proof assistant, you must start a new Emacs session.") ;; FIXME: this doesn't work quite right. We want to test ;; whether we are running during a compilation. How? ; (eval-when-compile -; (dolist (assistant proof-internal-assistant-table) -; (let ((path (concat proof-internal-home-directory +; (dolist (assistant proof-assistant-table) +; (let ((path (concat proof-home-directory ; (concat (symbol-name (car assistant)) "/")))) ; (or (member path load-path) ; (setq load-path @@ -156,9 +156,9 @@ NOTE: to change proof assistant, you must start a new Emacs session.") (or (cdr-safe (assoc assistant - proof-internal-assistant-table)) + proof-assistant-table)) (error "proof-site: symbol " (symbol-name assistant) - "is not in proof-internal-assistant-table"))) + "is not in proof-assistant-table"))) (assistant-name (car nameregexp)) (regexp (car (cdr nameregexp))) (sname (symbol-name assistant)) @@ -184,12 +184,12 @@ NOTE: to change proof assistant, you must start a new Emacs session.") (defgroup ,cusgrp nil ,(concat "Customization of " assistant-name " specific settings for Proof General.") - :group 'proof) + :group 'proof-general) ;; Set the proof-assistant configuration variable (setq proof-assistant ,assistant-name) ;; Extend the load path, load the real mode and invoke it. (setq load-path - (cons (concat proof-internal-home-directory ,elisp-dir "/") + (cons (concat proof-home-directory ,elisp-dir "/") load-path)) (load-library ,elisp-file) (,proofgen-mode)))) diff --git a/generic/proof-splash.el b/generic/proof-splash.el index 85a349e6..025431d6 100644 --- a/generic/proof-splash.el +++ b/generic/proof-splash.el @@ -25,10 +25,10 @@ Gif filename depends on colour depth of display." (cond ((and window-system (featurep 'jpeg) (not nojpeg)) (vector 'jpeg :file - (concat proof-internal-images-directory name ".jpg"))) + (concat proof-images-directory name ".jpg"))) ((and window-system (featurep 'gif)) (vector 'gif :file - (concat proof-internal-images-directory + (concat proof-images-directory (concat name (or (and (fboundp 'device-pixel-depth) @@ -64,12 +64,12 @@ inserted." :type 'sexp :group 'proof-config) -(defcustom proof-internal-display-splash-time 1.5 +(defcustom proof-splash-time 1.5 "Minimum number of seconds to display splash screen for. The splash screen may be displayed for a couple of seconds longer than this, depending on how long it takes the machine to initialise proof mode." :type 'number - :group 'proof-internal) + :group 'proof-general-internals) ;; Would be nice to get rid of this variable, but it's tricky ;; to construct a hook function, with a higher order function, @@ -148,7 +148,7 @@ Only do it if proof-splash-display is nil." (sit-for 0)) (setq proof-splash-timeout-conf (cons - (add-timeout proof-internal-display-splash-time + (add-timeout proof-splash-time 'proof-splash-remove-screen winconf) winconf)))))) @@ -161,7 +161,7 @@ Only do it if proof-splash-display is nil." ;; To approximate the best behaviour, we assume that this file is ;; loaded by a call to proof-mode. We display the screen now and add ;; a wait procedure temporarily to proof-mode-hook which prevents -;; redisplay until proof-internal-display-splash-time has elapsed. +;; redisplay until proof-splash-time has elapsed. ;; Display the screen ASAP... (proof-splash-display-screen) diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index 84a09dad..2686ccb3 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -36,7 +36,7 @@ prover specific buttons, see proof-toolbar.el.") (proof-toolbar-restart-icon "restart")) "List of icon variable names and their associated image files. A list of lists of the form (VAR IMAGE). IMAGE is the root name -for an image file in proof-internal-images-directory. The toolbar +for an image file in proof-images-directory. The toolbar code expects to find files IMAGE.xbm, IMAGE.xpm, IMAGE.8bit.xpm and chooses the best one for the display properites.") @@ -82,7 +82,7 @@ to the default toolbar." (lambda (buttons) (let ((var (car buttons)) (iconfiles (mapcar (lambda (name) - (concat proof-internal-images-directory + (concat proof-images-directory name icontype)) (cdr buttons)))) (set var (toolbar-make-button-list iconfiles)))) @@ -91,7 +91,7 @@ to set outline heading regexp.") (defun isa-mode-config-set-variables () "Configure generic proof scripting mode variables for Isabelle." (setq - proof-www-home-page isabelle-web-page + proof-assistant-home-page isabelle-web-page proof-mode-for-script 'isa-proofscript-mode ;; proof script syntax proof-terminal-char ?\; ; ends a proof @@ -159,7 +159,7 @@ to set outline heading regexp.") ;; /home/da/devel/lego/elisp/ or $PROOFGENERIC_HOME ? proof-shell-init-cmd (concat "use \"" - proof-internal-home-directory + proof-home-directory "isa/ProofGeneral.ML\";") proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading\\|^Proof General\\|^Not reading" ; "^---\\|^\\[opening " ;; could be last bracket on end of line, or with ### and ***. diff --git a/lego/lego.el b/lego/lego.el index 3a6fe5d4..869cf50a 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -378,7 +378,7 @@ (setq proof-comment-start "(*") (setq proof-comment-end "*)") - (setq proof-www-home-page lego-www-home-page) + (setq proof-assistant-home-page lego-www-home-page) (setq proof-mode-for-script 'lego-mode) |