diff options
-rw-r--r-- | CHANGES | 17 | ||||
-rw-r--r-- | coq/coq.el | 6 | ||||
-rw-r--r-- | generic/proof-config.el | 8 | ||||
-rw-r--r-- | generic/proof-script.el | 6 | ||||
-rw-r--r-- | generic/proof-toolbar.el | 2 | ||||
-rw-r--r-- | isa/isa.el | 6 | ||||
-rw-r--r-- | isar/isar.el | 6 | ||||
-rw-r--r-- | lego/lego.el | 6 | ||||
-rw-r--r-- | plastic/plastic.el | 10 |
9 files changed, 35 insertions, 32 deletions
@@ -8,23 +8,21 @@ Generic Changes New function control-button1 (proof-mouse-track-insert) copies individual commands (highlighted regions) from an open proof. When a proof is closed, it behaves as mouse-track-insert - (default XEmacs behaviour of control-button1). - + (the default XEmacs behaviour of control-button1). * New function C-c C-f (proof-find) to invoke some prover-specific mechanism to search for theories. -* [XEmacs only] Toolbar has five new buttons (State, Context, Info, - Command, Help) which invoke commands previously available on keys/menus. - Also a new "Find" button for proof-find. +* [XEmacs only] Toolbar has six new buttons (State, Context, Info, + Command, Help, Stop) which invoke commands previously available on + keys/menus. Also a new "Find" button for proof-find. * [XEmacs only] Toolbar enablers have been added. Buttons are automatically enabled or disabled as appropriate. This requires XEmacs 20.4 or better for reliable working. - * Menus and keybindings have been reorganized. - Now keybindings invoke same functions as toolbar. + Now keybindings invoke the same functions as the toolbar. * Terminal string now automatically added to command for C-c C-v @@ -76,5 +74,10 @@ Internal changes for developers to note using special character codes is fragile and needs replacing in future versions of Proof General! +* Renamed some configuration variables for uniformity: + proof-ctxt-string -> proof-context-command + proof-help-string -> proof-info-command + proof-prf-string -> proof-showproof-command + * Code cleanups and improvements. @@ -425,13 +425,13 @@ (setq proof-guess-command-line 'coq-guess-command-line) ;; Commands sent to proof engine - (setq proof-prf-string "Show" - proof-ctxt-string "Print All" + (setq proof-proof-command "Show" + proof-context-command "Print All" proof-goal-command "Goal %s." proof-save-command "Save %s." proof-find-theorems-command "Search %s." ;; FIXME da: Does Coq have a help or about command? -;; proof-help-string "Help" +;; proof-info-command "Help" proof-kill-goal-command coq-kill-goal-command) (setq proof-goal-command-p 'coq-goal-command-p diff --git a/generic/proof-config.el b/generic/proof-config.el index aab2e4d6..2a563855 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -437,17 +437,17 @@ command line options. For an example, see coq/coq.el." :type 'string :group 'prover-config) -(defcustom proof-ctxt-string "" +(defcustom proof-context-command "" "Command to display the context in proof assistant." :type 'string :group 'prover-config) -(defcustom proof-help-string "" - "Command to ask for help in proof assistant." +(defcustom proof-info-command "" + "Command to ask for help or information in the proof assistant." :type 'string :group 'prover-config) -(defcustom proof-prf-string "" +(defcustom proof-proof-command "" "Command to display proof state in proof assistant." :type 'string :group 'prover-config) diff --git a/generic/proof-script.el b/generic/proof-script.el index e6938743..a3f0498e 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1510,14 +1510,14 @@ Start up the proof assistant if necessary." (proof-define-assistant-command proof-prf "Show the current proof state." - proof-prf-string) + proof-proof-command) (proof-define-assistant-command proof-ctxt "Show the current context." - proof-ctxt-string) + proof-context-command) (proof-define-assistant-command proof-help "Show a help or information message from the proof assistant. Typically, a list of syntax of commands available." - proof-help-string) + proof-info-command) ;; ;; Commands which require an argument, and maybe affect the script. diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index 3051764d..805c0dfb 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -27,7 +27,7 @@ ;; in proof-toolbar-setup. ;; FIXME: consider automatically disabling buttons which are -;; not configured for the prover, e.g. if proof-help-string is +;; not configured for the prover, e.g. if proof-info-command is ;; not set, then the Info button should not be show. ;; FIXME: In the future, add back the enabler functions. @@ -128,11 +128,11 @@ no regular or easily discernable structure." proof-indent-commands-regexp (proof-ids-to-regexp isa-keywords) ;; proof engine commands - proof-prf-string "pr()" + proof-proof-command "pr()" proof-goal-command "Goal \"%s\";" proof-save-command "qed \"%s\";" - proof-ctxt-string "ProofGeneral.show_context()" - proof-help-string "ProofGeneral.help()" + proof-context-command "ProofGeneral.show_context()" + proof-info-command "ProofGeneral.help()" proof-kill-goal-command "ProofGeneral.kill_goal();" proof-find-theorems-command "ProofGeneral.thms_containing [\"%s\"]" ;; command hooks diff --git a/isar/isar.el b/isar/isar.el index 0b01bd34..1c529bc3 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -158,11 +158,11 @@ proof-save-with-hole-regexp isar-save-with-hole-regexp proof-indent-commands-regexp isar-indent-regexp ;; proof engine commands - proof-prf-string "pr" + proof-proof-command "pr" proof-goal-command "lemma \"%s\";" proof-save-command "qed" - proof-ctxt-string "print_context" - proof-help-string "help" + proof-context-command "print_context" + proof-info-command "help" proof-kill-goal-command "kill_proof;" proof-find-theorems-command "thms_containing %s;" ;; command hooks diff --git a/lego/lego.el b/lego/lego.el index a8b5276e..5930f501 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -349,11 +349,11 @@ Checks the width in the `proof-goals-buffer'" (setq proof-mode-for-script 'lego-mode) - (setq proof-prf-string "Prf" + (setq proof-proof-command "Prf" proof-goal-command "Goal %s;" proof-save-command "Save %s;" - proof-ctxt-string "Ctxt" - proof-help-string "Help") + proof-context-command "Ctxt" + proof-info-command "Help") (setq proof-goal-command-p 'lego-goal-command-p proof-count-undos-fn 'lego-count-undos diff --git a/plastic/plastic.el b/plastic/plastic.el index 14f2b8f3..2c3e44ef 100644 --- a/plastic/plastic.el +++ b/plastic/plastic.el @@ -386,12 +386,12 @@ Given is the first SPAN which needs to be undone." (setq proof-assistant-home-page plastic-www-home-page) (setq proof-mode-for-script 'plastic-mode) - (setq proof-prf-string (concat plastic-lit-string " &S PrfCtxt") - proof-goal-command (concat plastic-lit-string " Claim %s;") - proof-save-command (concat plastic-lit-string " Save %s;") ;; analogue? - proof-ctxt-string (concat plastic-lit-string " &S Ctxt 20") + (setq proof-showproof-command (concat plastic-lit-string " &S PrfCtxt") + proof-goal-command (concat plastic-lit-string " Claim %s;") + proof-save-command (concat plastic-lit-string " Save %s;") ;; analogue? + proof-context-command (concat plastic-lit-string " &S Ctxt 20") ;; show 20 things; see ^c+C... - proof-help-string (concat plastic-lit-string " &S Help")) + proof-info-command (concat plastic-lit-string " &S Help")) (setq proof-goal-command-p 'plastic-goal-command-p proof-count-undos-fn 'plastic-count-undos |