diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-08 13:42:31 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-08 13:42:31 +0000 |
| commit | 95d8a7f7364fde5af433ffa0e6c9f5bf664c5ebc (patch) | |
| tree | 9be997d4d9af9c12882d53434d8dbbcb49cbdcb6 /generic/pg-user.el | |
| parent | 0877b91645ec1a824eba51cf0ad46eb4d76a138f (diff) | |
Checkdoc cleanups
Diffstat (limited to 'generic/pg-user.el')
| -rw-r--r-- | generic/pg-user.el | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index 49c40675..fca238f8 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -966,6 +966,7 @@ The function `substitute-command-keys' is called on the argument." (global-set-key [f5] 'pg-identifier-near-point-query) (defun pg-identifier-under-mouse-query (event) + "Query the prover about the identifier near mouse click EVENT." (interactive "e") (if proof-query-identifier-command (save-selected-window @@ -975,6 +976,7 @@ The function `substitute-command-keys' is called on the argument." (pg-identifier-near-point-query)))))) (defun pg-identifier-near-point-query () + "Query the prover about the identifier near point." (interactive) (let* ((stend (if (region-active-p) (cons (region-beginning) (region-end)) @@ -1005,6 +1007,7 @@ The function `substitute-command-keys' is called on the argument." (defvar proof-query-identifier-history nil) (defun proof-query-identifier (string) + "Query the prover about the identifier STRING." (interactive (list (completing-read "Query identifier: " @@ -1015,8 +1018,10 @@ The function `substitute-command-keys' is called on the argument." (if string (pg-identifier-query string))) (defun pg-identifier-query (identifier &optional ctxt callback) - "Query the proof assisstant about the given identifier (or string). + "Query the proof assisstant about the given IDENTIFIER. This uses `proof-query-identifier-command'. +Parameter CTXT allows to give a context for the identifier (which +allows for multiple name spaces). If CALLBACK is set, we invoke that when the command completes." (unless (or (null identifier) (string-equal identifier "")) ;; or whitespace? |