Fixes for completion support.

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))