From 95d8a7f7364fde5af433ffa0e6c9f5bf664c5ebc Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sun, 8 Aug 2010 13:42:31 +0000 Subject: Checkdoc cleanups --- generic/pg-user.el | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'generic/pg-user.el') 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? -- cgit v1.2.3