diff options
author | 1998-10-22 16:01:38 +0000 | |
---|---|---|
committer | 1998-10-22 16:01:38 +0000 | |
commit | 2d6b4150e681dfb09a75eab05c052a0fa04c621c (patch) | |
tree | 5b7556743eea8921f5715c497c41e9f7c63a7888 /generic/proof-config.el | |
parent | e7b001fc03220b8c386bedfb480b2ce963560521 (diff) |
Added todo for clean byte compile
Diffstat (limited to 'generic/proof-config.el')
-rw-r--r-- | generic/proof-config.el | 79 |
1 files changed, 62 insertions, 17 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index f5fb761d..5c82946e 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -9,22 +9,65 @@ ;; $Id$ ;; ;; -;; This file declares all prover-specific configuration variables. -;; These are used variously by the proof script mode and the proof -;; shell mode. +;; This file declares all user options and prover-specific +;; configuration variables for Proof General. The variables +;; are used variously by the proof script mode and the +;; proof shell mode, menus, and toolbar. ;; ;; To customize Proof General for a new proof assistant, you ;; should read this file carefully! ;; -;; 0. Major modes -;; 1. Menus, user-level commands. -;; 2. Script mode configuration -;; 3. Shell mode configuration -;; 3a. commands -;; 3b. regexps -;; 3c. hooks +;; 1. User options +;; 2. Major modes +;; 3. Menus, user-level commands. +;; 4. Script mode configuration +;; 5. Shell mode configuration +;; 5a. commands +;; 5b. regexps +;; 5c. hooks ;; +;; The user options don't need to be set on a per-prover basis. +;; The remaining variables in sections 2-5 do. +;; + +;; A global constant that's convenient to keep here. +(defconst proof-mode-name "Proof-General" + "Root name for proof script mode. +Used internally and in menu titles.") + + + +;; +;; 1. User options for proof mode +;; +;; The following variables are user options for Proof General. +;; They appear in the 'proof' customize group and should +;; *not* normally be touched by prover specific code. +;; + +(defcustom proof-prog-name-ask-p nil + "*If non-nil, query user which program to run for the inferior process." + :type 'boolean + :group 'proof) + +(defcustom proof-one-command-per-line nil + "*If non-nil, format for newlines after each proof command in a script." + :type 'boolean + :group 'proof) + +(defcustom proof-general-home-page + "http://www.dcs.ed.ac.uk/home/proofgen" + "*Web address for Proof General" + :type 'string + :group 'proof-internal) + + + +;; +;; CONFIGURATION VARIABLES +;; +;; (defgroup prover-config nil "Configuration of Proof General for the prover in use." @@ -59,9 +102,10 @@ from the name given in proof-internal-assistant-table." + ;; -;; 0. The major modes used by Proof General. +;; 2. The major modes used by Proof General. ;; (defcustom proof-mode-for-shell nil @@ -85,8 +129,9 @@ Suggestion: this can be set in proof-pre-shell-start-hook." + ;; -;; 1. Configuration for menus, user-level commands, etc. +;; 3. Configuration for menus, user-level commands, etc. ;; (defcustom proof-www-home-page "" @@ -136,7 +181,7 @@ This variable should be set before requiring proof.el" ;; -;; 2. Configuration for proof script mode +;; 4. Configuration for proof script mode ;; ;; @@ -289,7 +334,7 @@ assistant, for example, to switch to a new theory." ;; -;; 3. Configuration for proof shell +;; 5. Configuration for proof shell ;; ;; The variables in this section concern the proof shell mode. ;; The first group of variables are hooks invoked at various points. @@ -308,7 +353,7 @@ assistant, for example, to switch to a new theory." ;; -;; 3a. commands +;; 5a. commands ;; (defcustom proof-prog-name nil @@ -329,7 +374,7 @@ Suggestion: this can be set in proof-pre-shell-start-hook." ;; -;; 3b. Regexp variables for matching output from proof process. +;; 5b. Regexp variables for matching output from proof process. ;; (defcustom proof-shell-prompt-pattern nil @@ -406,7 +451,7 @@ In particular, after a `pbp-goal-command' or a `pbp-hyp-command'." :group 'proof-shell) ;; -;; 3c. hooks +;; 5c. hooks ;; (defcustom proof-shell-insert-hook nil |