diff options
| author | Hendrik Tews | 2011-04-15 11:47:51 +0000 |
|---|---|---|
| committer | Hendrik Tews | 2011-04-15 11:47:51 +0000 |
| commit | 3b5d51c37781b16e74fe7bab2e12c80dc86aa86a (patch) | |
| tree | ed01668c3829dc695bdc2773e7c8359f88dc1f47 | |
| parent | 73617c15286def069e3b0a49c37805c42ccb6e56 (diff) | |
* fix overwriting setq coq-prog-name before loading Proof General
* more complete callback listing in proof-action list doc
| -rw-r--r-- | coq/coq-syntax.el | 5 | ||||
| -rw-r--r-- | coq/coq.el | 2 | ||||
| -rw-r--r-- | generic/proof-shell.el | 4 |
3 files changed, 4 insertions, 7 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 5b15cb3a..b95d0345 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -27,11 +27,6 @@ See also `coq-prog-env' to adjust the environment." :type 'string :group 'coq) -;; da: please take care that the compiled version of this file works! -;; Top-level forms need to be delayed during compile. - -(eval-when (load eval) - (custom-reevaluate-setting 'coq-prog-name)) ;;; keyword databases @@ -37,8 +37,8 @@ (declare-function smie-rule-parent-p "smie") (require 'proof) -(require 'coq-local-vars) ; (require 'coq-syntax) ; sets coq-prog-name +(require 'coq-local-vars) ; (require 'coq-abbrev) ; coq specific menu diff --git a/generic/proof-shell.el b/generic/proof-shell.el index be127b8a..dee2298e 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -56,7 +56,9 @@ is a space. ACTION is the callback to be invoked when this item has been processed by the prover. For normal scripting items it is `proof-done-advancing', for retract items -`proof-done-retracting', but there are more possibilities. +`proof-done-retracting', but there are more possibilities (e.g. +`proof-done-invisible', `proof-shell-set-silent' and +`proof-shell-clear-silent'). The DISPLAYFLAGS are set for non-scripting commands or for when scripting should not |