diff options
| author | David Aspinall | 1999-11-17 13:54:49 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-11-17 13:54:49 +0000 |
| commit | f69af9a107a9c0124831a766279475f8a2d96fb2 (patch) | |
| tree | 79f8db24d69c03afc0d9a71f5e6d3bba7e4433cf /generic/proof-script.el | |
| parent | dbe60d432254dd18dc83c178ea827ee65436ae55 (diff) | |
Add Function Menu to menu. Fix a few bugs/probs shown up by byte-compiling.
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index c7d98503..2f84648d 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -35,10 +35,12 @@ ;; More autoloads for proof-shell (added to nuke warnings, ;; maybe some should be 'official' exported functions in proof.el) ;; This helps see interface between proof-script / proof-shell. -(eval-when-compile +(eval-and-compile (mapcar (lambda (f) (autoload f "proof-shell")) '(proof-shell-ready-prover + proof-extend-queue + proof-shell-wait proof-start-queue proof-shell-live-buffer proof-shell-invisible-command))) @@ -457,7 +459,7 @@ proof assistant and Emacs is has a modified buffer visiting the file." 'wait))))) (defun proof-inform-prover-file-retracted (rfile) - (if (and informprover proof-shell-inform-file-retracted-cmd) + (if proof-shell-inform-file-retracted-cmd (proof-shell-invisible-command (format proof-shell-inform-file-retracted-cmd rfile) 'wait))) @@ -2284,6 +2286,8 @@ This is intended as a value for proof-activate-scripting-hook" :active (proof-x-symbol-support-maybe-available) :style toggle :selected proof-x-symbol-enable] + ["Function menu" function-menu + :active (foundp 'function-menu)] "----") proof-shared-menu) "The menu for the proof assistant.") |