diff options
| author | David Aspinall | 1998-10-12 15:58:59 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-10-12 15:58:59 +0000 |
| commit | d399afff6fbf157550a1144c14e90ecfdbb8b005 (patch) | |
| tree | 94fcbc5032b65d34cfde4e03c7c01db17044fb51 | |
| parent | a9fd410a36676d296d81cc17e168e750749b24d3 (diff) | |
Added todo for proof-issue-goal, proof-issue-save.
| -rw-r--r-- | generic/proof-site.el | 12 | ||||
| -rw-r--r-- | todo | 3 |
2 files changed, 10 insertions, 5 deletions
diff --git a/generic/proof-site.el b/generic/proof-site.el index eda5261c..b33748b9 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -7,6 +7,7 @@ ;; $Id$ ;; +;; begin UGLY COMPATIBILITY HACK (or (featurep 'custom) ;; Quick hack to support defcustom for Emacs 19 ;; FIXME da: Remove this soon. @@ -14,6 +15,7 @@ (defmacro defcustom (sym val doc &rest args) (defvar sym val doc)) (defmacro group (sym mems doc &rest args))) +;; end UGLY COMPATIBILITY HACK (defgroup proof nil @@ -125,20 +127,20 @@ NOTE: to change proof assistant, you must start a new Emacs session.") ;; Now add auto-loads and load-path elements to support the ;; proof assistants selected, and define a stub -(let ((assistants proof-assistants) proof-assistant) +(let ((assistants proof-assistants) assistant) (while assistants (let* - ((proof-assistant (car assistants)) + ((assistant (car assistants)) (nameregexp (or (cdr-safe - (assoc proof-assistant + (assoc assistant proof-internal-assistant-table)) - (error "proof-site: symbol " (symbol-name proof-assistant) + (error "proof-site: symbol " (symbol-name assistant) "is not in proof-internal-assistant-table"))) (assistant-name (car nameregexp)) (regexp (car (cdr nameregexp))) - (sname (symbol-name proof-assistant)) + (sname (symbol-name assistant)) ;; NB: File name for each prover is the same as its symbol name! (elisp-file sname) ;; NB: Dir name for each prover is the same as its symbol name! @@ -14,6 +14,9 @@ X (Low) probably not worth wasting time on * This is a list of things which need doing in the generic interface ==================================================================== +B proof-issue-goal should refuse to work when a proof is in progress. + Similarly proof-issue-save should refuse to work when a proof + hasn't been completed! B Bug in proof-retract-until-point when called twice in succession: calls backward-char at beginning of buffer. (Should say no |