diff options
| -rw-r--r-- | generic/proof-script.el | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index cfce635e..d511f334 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2375,18 +2375,23 @@ sent to the assistant." ;; (defun proof-add-completions () "Add completions from <PA>-completion-table to completion database. -Uses `add-completion' with a negative number of uses to discourage -saving these into the users database." +Uses `add-completion' with a negative number of uses and ancient +last use time, to discourage saving these into the users database." (interactive) (require 'completion) - (mapcar (lambda (cmpl) (add-completion cmpl -1000)) + (mapcar (lambda (cmpl) + ;; completion gives error in this case; trapping + ;; the error here is tricky in FSF Emacs so duplicate + ;; the test. + (if (>= (length cmpl) completion-min-length) + (add-completion cmpl -1000 0))) (proof-ass completion-table))) ;; NB: completion table is expected to be set when proof-script ;; is loaded! Can call proof-script-add-completions if the table ;; is updated. (eval-after-load "completion" - (proof-add-completions)) + '(proof-add-completions)) |