Fix most doc issues raised by (checkdoc)

25 files changed, 398 insertions, 376 deletions

diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el
index 714429b7..b06b4ec5 100644
--- a/generic/pg-assoc.el
+++ b/generic/pg-assoc.el
@@ -48,7 +48,7 @@ Some may be dead/nil."
 ;;;###autoload
 (defun proof-associated-windows (&optional all-frames)
   "Return a list of the associated buffers windows.
-Dead or nil buffers are not represented in the list. Optional
+Dead or nil buffers are not represented in the list.  Optional
 argument ALL-FRAMES has the same meaning than for
 `get-buffer-window'."
   (let ((bufs (proof-associated-buffers))
diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index bc3ab9c5..e7cb19a9 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-autotest.el
@@ -104,7 +104,7 @@
 				 (format-time-string "%D %H:%M")))))
 
 (defun pg-autotest-message (msg &rest args)
-  "Give message MSG in log file output and on display."
+  "Give message MSG (formatted using ARGS) in log file output and on display."
   (let ((fmsg   (if args (apply 'format msg args) msg)))
     (proof-with-current-buffer-if-exists
      pg-autotest-log
@@ -217,7 +217,7 @@ completely processing the buffer as the last step."
 	(proof-shell-wait)
 	(decf jumps))
 
-	((and (eq random-thing 1) 
+	((and (eq random-thing 1)
 	      (not (proof-locked-region-empty-p)))
 	 (pg-autotest-message
 	  " random jump: retracting whole buffer")
@@ -280,7 +280,7 @@ completely processing the buffer as the last step."
 (defun pg-autotest-test-quit-prover ()
   "Exit prover process."
   (if (buffer-live-p proof-shell-buffer)
-      (let ((kill-buffer-query-functions nil)) 
+      (let ((kill-buffer-query-functions nil))
 	(kill-buffer proof-shell-buffer))
     (error "No proof shell buffer to kill")))
 
diff --git a/generic/pg-custom.el b/generic/pg-custom.el
index 8a7bb793..0c67c7a2 100644
--- a/generic/pg-custom.el
+++ b/generic/pg-custom.el
@@ -115,7 +115,7 @@ For example for coq on Windows you might need something like:
   :type '(repeat string)
   :group 'proof-shell)
 
-(defpgcustom quit-timeout 
+(defpgcustom quit-timeout
   (cond
    ((eq proof-assistant-symbol 'isar)    45)
    (t					 5))
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index c35f0f29..baab5561 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -89,7 +89,7 @@ function tries to do that by calling `pg-response-maybe-erase'.
 
 If KEEPRESPONSE is non-nil, we assume that a response message
 corresponding to this goals message has already been displayed
-before this goals message (see `proof-shell-handle-delayed-output'),  
+before this goals message (see `proof-shell-handle-delayed-output'),
 so the response buffer should not be cleared."
   (save-excursion
     ;; Response buffer may be out of date. It may contain (error)
diff --git a/generic/pg-movie.el b/generic/pg-movie.el
index ba641c20..9be95972 100644
--- a/generic/pg-movie.el
+++ b/generic/pg-movie.el
@@ -52,15 +52,15 @@
   (let* ((tokens   (proof-ass unicode-tokens-enable))
 	 (cmd      (buffer-substring-no-properties
 		      (span-start span) (span-end span)))
-	 (tcmd     (if tokens 
+	 (tcmd     (if tokens
 		       ;; no subscripts of course
 		       (unicode-tokens-encode-str cmd)
 		     cmd))
 	 (helpspan (span-property span 'pg-helpspan))
-	 (resp     (when helpspan 
+	 (resp     (when helpspan
 		     (span-property helpspan 'response)))
 	 (tresp    (if resp
-		       (if tokens 
+		       (if tokens
 			   (unicode-tokens-encode-str resp)
 			 resp)
 		     ""))
@@ -99,7 +99,7 @@ If FORCE, overwrite existing file without asking."
 		(point-min)
 		(point-max)))
 	(movie-file-name
-	 (concat 
+	 (concat
 	  (file-name-sans-extension
 		  (buffer-file-name)) ".xml")))
 
@@ -114,7 +114,7 @@ If FORCE, overwrite existing file without asking."
 ;;;###autoload
 (defun pg-movie-export-from (script &optional force)
   "Export the movie file that results from processing SCRIPT."
-  (interactive "fFile: 
+  (interactive "fFile:
 P")
   (let ((proof-full-annotation t) ; dynamic
 	(proof-fast-process-buffer t))
@@ -126,10 +126,10 @@ P")
 (defun pg-movie-export-directory (dir extn)
   "Export movie files from directory DIR with extension EXTN.
 Existing XML files are overwritten."
-  (interactive "DDirectory: 
+  (interactive "DDirectory:
 sFile extension: ")
-  (let ((files (directory-files 
-		dir t 
+  (let ((files (directory-files
+		dir t
 		(concat "\\." extn "$"))))
     (dolist (f files)
       (pg-movie-export-from f 'force))
diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el
index 9792dfd0..1492e0ca 100644
--- a/generic/pg-pamacs.el
+++ b/generic/pg-pamacs.el
@@ -39,10 +39,10 @@
 (require 'proof-compat)			; pg-custom-undeclare-variable
 (require 'proof-autoloads)		; proof-debug
 
-(defmacro deflocal (var value &optional docstring)
-  "Define a buffer local variable VAR with default value VALUE."
+(defmacro deflocal (var value &optional doc)
+  "Define a buffer local variable VAR with default value VALUE and docstring DOC."
  `(progn
-    (defvar ,var nil ,docstring)
+    (defvar ,var nil ,doc)
     (make-variable-buffer-local (quote ,var))
     (setq-default ,var ,value)))
 
@@ -79,13 +79,13 @@ This macro should only be invoked once a specific prover is engaged."
 		(symbol-value pasym)))))
 
 (defun proof-defpgcustom-fn (sym args)
-  "Define a new customization variable <PA>-sym for current proof assistant.
+  "Define a new customization variable <PA>-SYM for current proof assistant.
 Helper for macro `defpgcustom'."
   (let ((specific-var (proof-ass-symv sym))
 	 (generic-var  (intern (concat "proof-assistant-" (symbol-name sym))))
-	 (newargs     (if (member :group args) 
-			  args 
-			(append (list :group 
+	 (newargs     (if (member :group args)
+			  args
+			(append (list :group
 				      proof-assistant-internals-cusgrp)
 				args))))
     (eval
@@ -116,7 +116,7 @@ but which the user may require different values of across provers.
 The function proof-assistant-<SYM> is also defined, which can be used in the
 generic portion of Proof General to access the value for the current prover.
 
-Arguments are as for `defcustom', which see.  If a :group argument is
+Arguments ARGS are as for `defcustom', which see.  If a :group argument is
 not supplied, the setting will be added to the internal settings for the
 current prover (named <PA>-config)."
   `(proof-defpgcustom-fn (quote ,sym) (quote ,args)))
@@ -183,7 +183,7 @@ Usage: (defpgdefault SYM VALUE)"
 	(setq name (intern (concat (downcase (cadr args)) ":" (symbol-name name))))
 	(put name 'pggroup (cadr args))
 	(setq args (cdr args)))
-       ((eq (car args) :pgdynamic) 
+       ((eq (car args) :pgdynamic)
 	(put name 'pgdynamic (cadr args))
 	(setq args (cdr args)))
        ((eq (car args) :type)
@@ -202,11 +202,11 @@ Usage: (defpgdefault SYM VALUE)"
 		      (eq (eval type) 'integer)
 		      (eq (eval type) 'number)
 		      (eq (eval type) 'string)))
-      (error "defpacustom: missing :type keyword or wrong :type value"))
+      (error "Macro defpacustom: missing :type keyword or wrong :type value"))
 
     ;; Error in case a defpacustom is repeated.
     (when (assq name proof-assistant-settings)
-      (error "defpacustom: Proof assistant setting %s re-defined!"
+      (error "Macro defpacustom: Proof assistant setting %s re-defined!"
 	     name))
 
     (eval
@@ -237,8 +237,8 @@ which can be changed by sending commands.
 In this case, NAME stands for the internal setting, flag, etc,
 for the proof assistant, and a :setting and :type value should be
 provided.  The :type of NAME should be one of 'integer, 'float,
-'boolean, 'string. Other types are not supported (see
-`proof-menu-entry-for-setting'). They will yield an error when
+'boolean, 'string.  Other types are not supported (see
+`proof-menu-entry-for-setting').  They will yield an error when
 constructing the proof assistant menu.
 
 The function `proof-assistant-format' is used to format VAL.
@@ -262,7 +262,7 @@ Additional properties in the ARGS prop list may include:
 
  pgdynamic flag      If flag is non-nil, this setting is a dynamic one
 		     that is particular to the running instance of the prover.
-		     Automatically set by preferences configured from PGIP 
+		     Automatically set by preferences configured from PGIP
 		     askprefs message.
 
 This macro also extends the `proof-assistant-settings' list."
diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el
index 6436871f..619a5d6c 100644
--- a/generic/pg-pbrpm.el
+++ b/generic/pg-pbrpm.el
@@ -125,22 +125,22 @@ Matches the region to be returned.")
   (set-buffer pg-pbrpm-buffer-menu))
 
 (defun pg-pbrpm-analyse-goal-buffer ()
-  "This function analyses the goal buffer and produces a table to find goals and hypothesis.
-If stores, in the variable pg-pbrpm-goal-description, a list with shape
-
-   (start-goal end-goal goal-name start-concl hyps ...) with 5 elements for each goal:
-
-     start-goal: the position of the first char of the goal
-     end-goal: the position of the last char of the goal
-     goal-name: the goal name (or number)
-     start-concl: the position of first char of the conclusion of the goal
-     hyps: the list of hypothesis with the shape:
-
-  (start-hyp start-hyp-text end-hyp hyp-name ...) with 4 elemets per hypothesis:
-     start-hyp: the position of the first char of the hypothesis (including its name)
-     start-hyp-text: the position of the first char of the hypothesis formula (no name)
-     end-hyp: the position of the last char of the hypothesis
-     hyp-name: then name of the hypothesis."
+  "Analyse the goal buffer and produce a table to find goals and hypothesis.
+
+It stores, in the variable ‘pg-pbrpm-goal-description’, a list with shape
+
+(start-goal end-goal goal-name start-concl hyps ...) with 5 elements per goal:
+  start-goal: the position of the first char of the goal
+  end-goal: the position of the last char of the goal
+  goal-name: the goal name (or number)
+  start-concl: the position of first char of the conclusion of the goal
+  hyps: the list of hypothesis with the shape:
+
+(start-hyp start-hyp-text end-hyp hyp-name ...) with 4 elements per hypothesis:
+  start-hyp: the position of the first char of the hyp (including its name)
+  start-hyp-text: the position of the first char of the hyp formula (no name)
+  end-hyp: the position of the last char of the hypothesis
+  hyp-name: then name of the hypothesis."
   (with-current-buffer proof-goals-buffer
   (save-excursion
     (goto-char 0)
@@ -204,7 +204,9 @@ If stores, in the variable pg-pbrpm-goal-description, a list with shape
       (pg-pbrpm-eliminate-id (cons (car l) acc) (cdr l)))))
 
 (defun pg-pbrpm-build-menu (event start end)
-"Build a Proof By Rules pop-up menu according to the state of the proof, the event and a selected region (between the start and end markers).
+  "Build a Proof By Rules pop-up menu.
+Depends on the state of the proof, the event and a selected region
+(between the start and end markers).
 The prover command is processed via pg-pbrpm-run-command."
 ;; first, run the prover specific (name, rule)'s list generator
    (let ((click-info (pg-pbrpm-process-click event start end))) ; retrieve click informations
@@ -327,8 +329,9 @@ The prover command is processed via pg-pbrpm-run-command."
 				     (span-property sp1 'goalnum))))))))
 
 (defun pg-pbrpm-run-command (args)
-"Insert COMMAND into the proof queue and then run it.
--- adapted from proof-insert-pbp-command --"
+"Insert command into the proof queue and then run it.
+
+\(adapted from ‘proof-insert-pbp-command’)"
    (let* ((command (pop args)) (act (pop args)) (spans (pop args)) (allspan (pop spans)))
      (if act (setq command (apply act command spans nil)))
      (if allspan (setq command (concat "(* " (span-string allspan) " *)\n" command ".")))
@@ -428,15 +431,15 @@ If no match found, return the empty string."
 	(return-from 'loop "")))))
 
 (defun pg-pbrpm-translate-position (buffer pos)
-  "return pos if buffer is goals-buffer otherwise, return the point position in
-the goal buffer"
+  "If BUFFER is goals-buffer, return POS, otherwise the point in the goal buffer."
   (if (eq proof-goals-buffer buffer)
       pos
     (with-current-buffer proof-goals-buffer
       (point))))
 
 (defun pg-pbrpm-process-click (event start end)
-"Returns the list of informations about the click needed to call generate-menu. EVENT is an event."
+  "Return the list of infos about the click needed to call ‘generate-menu’.
+EVENT is an event."
   (save-excursion
     (save-window-excursion
       (mouse-set-point event)
@@ -521,8 +524,8 @@ the goal buffer"
   t)
 
 (defun pg-pbrpm-remember-region (event &optional delete)
-  "Allow multiple selection as a list of spam stored in ???. The current (standard)
-   selection in the same buffer is also stored"
+  "Allow multiple selection as a list of span stored in ???.
+The current (standard) selection in the same buffer is also stored."
   (interactive "*e")
   (setq pg-pbrpm-remember-region-selected-region nil)
   (let ((mouse-track-drag-up-hook 'pg-pbrpm-remember-region-drag-up-hook)
@@ -535,7 +538,8 @@ the goal buffer"
 		     (pg-pbrpm-do-remember-region (car pair) (cdr pair))))))
 
 (defun pg-pbrpm-process-region (span)
-"Returns the list of informations about the the selected region needed to call generate-menu. span is a span covering the selected region"
+"Return the list of infos on the selected region needed to call ‘generate-menu’.
+SPAN is a span covering the selected region."
    (let ((start (span-start span))
 	 (end (span-end span))
 	 (buffer (span-buffer span))
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el
index 997f8bb1..0f427ecb 100644
--- a/generic/pg-pgip.el
+++ b/generic/pg-pgip.el
@@ -38,7 +38,7 @@
 
 (declare-function pg-response-warning "pg-response")
 (declare-function pg-response-message "pg-response")
-(declare-function proof-segment-up-to "proof-script") 
+(declare-function proof-segment-up-to "proof-script")
 (declare-function proof-insert-pbp-command "proof-script")
 
 (defalias 'pg-pgip-debug   'proof-debug)
@@ -111,7 +111,7 @@ Return a symbol representing the PGIP command processed, or nil."
   (let ((ppfn  (cdr-safe (assoc cmdname pg-pgip-post-process-functions))))
     (if (fboundp ppfn)
 	(progn
-	  (pg-pgip-debug 
+	  (pg-pgip-debug
 	   "Post-processing for PGIP message type `%s' with function `%s'" cmdname ppfn)
 	  (funcall ppfn))
       (pg-pgip-debug "[No post-processing defined for PGIP message type `%s']" cmdname))))
diff --git a/generic/pg-response.el b/generic/pg-response.el
index d89d3c0b..43e0e279 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -92,8 +92,7 @@
 ;;
 
 (defvar pg-response-special-display-regexp nil
-  "Regexp for `special-display-regexps' (now display-buffer-alist)
-for multiple frame use.
+  "Regexp for ‘display-buffer-alist’ for multiple frame use.
 Internal variable, setting this will have no effect!")
 
 (defconst proof-multiframe-parameters
@@ -129,8 +128,10 @@ Internal variable, setting this will have no effect!")
 
 (defun proof-guess-3win-display-policy (&optional policy)
   "Return the 3 windows mode layout policy from user choice POLICY.
-If POLIY is smart then guess the good policy from the current
-frame geometry, otherwise follow POLICY."
+If POLICY is ’smart then guess the good policy from the current
+frame geometry, otherwise follow POLICY.
+
+See ‘proof-layout-windows’ for more details about POLICY."
   (if (eq policy 'smart)
       (cond
        ((>= (frame-width) (* 1.5 split-width-threshold)) 'horizontal)
@@ -139,9 +140,10 @@ frame geometry, otherwise follow POLICY."
     policy))
 
 (defun proof-select-three-b (b1 b2 b3 &optional policy)
-  "Put the given three buffers into three windows.
-Following POLICY, which can be one of 'smart, 'horizontal,
-'vertical or 'hybrid."
+  "Put the three buffers B1, B2, and B3 into three windows.
+Following POLICY, which can be 'smart, 'horizontal, 'vertical, or 'hybrid.
+
+See ‘proof-layout-windows’ for more details about POLICY."
   (interactive "bBuffer1:\nbBuffer2:\nbBuffer3:")
   (delete-other-windows)
   (switch-to-buffer b1)
@@ -181,7 +183,8 @@ Following POLICY, which can be one of 'smart, 'horizontal,
 
 
 (defun proof-display-three-b (&optional policy)
-  "Layout three buffers in a single frame.  Only do this if buffers exist."
+  "Layout three buffers in a single frame.  Only do this if buffers exist.
+In this case, call ‘proof-select-three-b’ with argument POLICY."
   (interactive)
   (when (and (buffer-live-p proof-goals-buffer)
 	     (buffer-live-p proof-response-buffer))
@@ -220,9 +223,9 @@ For multiple frame mode, this function obeys the setting of
 For single frame mode:
 
 - In two panes mode, this uses a canonical layout made by splitting
-Emacs windows in equal proportions. The splitting is vertical if
-emacs width is smaller than `split-width-threshold' and
-horizontal otherwise. You can then adjust the proportions by
+Emacs windows in equal proportions.  The splitting is vertical if
+Emacs width is smaller than `split-width-threshold' and
+horizontal otherwise.  You can then adjust the proportions by
 dragging the separating bars.
 
 - In three pane mode, there are three display modes, depending
@@ -238,7 +241,7 @@ dragging the separating bars.
     response).
 
   By default, the display mode is automatically chosen by
-  considering the current emacs frame width: if it is smaller
+  considering the current Emacs frame width: if it is smaller
   than `split-width-threshold' then vertical mode is chosen,
   otherwise if it is smaller than 1.5 * `split-width-threshold'
   then hybrid mode is chosen, finally if the frame is larger than
@@ -249,7 +252,7 @@ dragging the separating bars.
 
   If you want to force one of the layouts, you can set variable
   `proof-three-window-mode-policy' to 'vertical, 'horizontal or
-  'hybrid. The default value is 'smart which sets the automatic
+  'hybrid.  The default value is 'smart which sets the automatic
   behaviour described above."
   (interactive)
   (cond
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 21d9479d..126901cb 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -31,8 +31,8 @@
   (require 'completion))                ; Loaded dynamically at runtime.
 (defvar which-func-modes)               ; Defined by which-func.
 
-(declare-function proof-segment-up-to "proof-script") 
-(declare-function proof-interrupt-process "proof-shell") 
+(declare-function proof-segment-up-to "proof-script")
+(declare-function proof-interrupt-process "proof-shell")
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -46,12 +46,12 @@
 ;;;###autoload
 (defun proof-script-new-command-advance ()
   "Move point to a nice position for a new command, possibly inserting spaces.
-Assumes that point is at the end of a command.  
+Assumes that point is at the end of a command.
 No effect if `proof-next-command-insert-space' is nil."
   (interactive)
   (when proof-next-command-insert-space
     (let (sps)
-      (if (and (proof-next-command-new-line) 
+      (if (and (proof-next-command-new-line)
 	       (setq sps (skip-chars-forward " \t"))
 	       ;; don't break existing lines
 	       (eolp))
@@ -93,7 +93,7 @@ Assumes script buffer is current."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-;; Further movement commands 
+;; Further movement commands
 ;;
 
 (defun proof-goto-command-start ()
@@ -135,7 +135,8 @@ Assumes script buffer is current."
 		(backward-char))))))))
 
 (defun proof-forward-command (&optional num)
-  "Move forward to the start of the next proof region."
+  "Move forward to the start of the next proof region.
+If called interactively, NUM is given by the prefix argument."
   (interactive "p")
   (skip-chars-forward " \t\n")
   (let* ((span  (or (span-at (point) 'type)
@@ -387,7 +388,7 @@ a proof command."
 
 ;;;###autoload
 (defmacro proof-define-assistant-command (fn doc cmdvar &optional body)
-  "Define FN (docstring DOC) to send BODY to prover, based on CMDVAR.
+  "Define FN (docstring DOC): check if CMDVAR is set, then send BODY to prover.
 BODY defaults to CMDVAR, a variable."
   `(defun ,fn ()
      ,(concat doc
@@ -400,7 +401,8 @@ BODY defaults to CMDVAR, a variable."
 
 ;;;###autoload
 (defmacro proof-define-assistant-command-witharg (fn doc cmdvar prompt &rest body)
-  "Define command FN to prompt for string CMDVAR to proof assistant.
+  "Define FN (arg) with DOC: check CMDVAR is set, PROMPT a string and eval BODY.
+The BODY can contain occurrences of arg.
 CMDVAR is a variable holding a function or string.  Automatically has history."
   `(progn
      (defvar ,(intern (concat (symbol-name fn) "-history")) nil
@@ -482,14 +484,14 @@ This is intended as a value for `proof-activate-scripting-hook'"
  "Write a goal command in the script, prompting for the goal."
  proof-goal-command
  "Goal" ; Goals always start at a new line
- (let ((proof-next-command-on-new-line t)) 
+ (let ((proof-next-command-on-new-line t))
    (proof-issue-new-command arg)))
 
 (proof-define-assistant-command-witharg proof-issue-save
  "Write a save/qed command in the script, prompting for the theorem name."
  proof-save-command
  "Save as" ; Saves always start at a new line
- (let ((proof-next-command-on-new-line t)) 
+ (let ((proof-next-command-on-new-line t))
    (proof-issue-new-command arg)))
 
 
@@ -524,13 +526,13 @@ It can also be used as a minor mode function: with ARG, turn on iff ARG>0"
 (defun proof-electric-terminator (&optional count)
   "Insert terminator char, maybe sending the command to the assistant.
 If we are inside a comment or string, insert the terminator.
-Otherwise, if the variable `proof-electric-terminator-enable' 
+Otherwise, if the variable `proof-electric-terminator-enable'
 is non-nil, the command will be sent to the assistant.
 
-To side-step the electric action and possibly insert multiple 
-characters, use a numeric prefix arg, like M-3 <terminator>."
+To side-step the electric action and possibly insert multiple characters,
+pass a non-nil COUNT arg, e.g. a numeric prefix such as M-3 <terminator>."
   (interactive "P")
-  (if (and 
+  (if (and
        (not count)
        proof-electric-terminator-enable
        (not (proof-inside-comment (point)))
@@ -749,7 +751,7 @@ If NUM is negative, move upwards.  Return new span."
 	  ((idiom (and span (span-property span 'idiom)))
 	   (id    (and span (span-property span 'id))))
 	(popup-menu (pg-create-in-span-context-menu
-		     span idiom 
+		     span idiom
 		     (if id (symbol-name id))))))))
 
 (defun pg-toggle-visibility ()
@@ -766,7 +768,7 @@ If NUM is negative, move upwards.  Return new span."
   (append
    (list (pg-span-name span))
    (list (vector
-	  "Show/hide"  
+	  "Show/hide"
 	  (if idiom (list 'pg-toggle-element-visibility (quote idiom) name))
 	  (not (not idiom))))
    (list (vector
@@ -812,7 +814,7 @@ If NUM is negative, move upwards.  Return new span."
     (pg-hint
      (format
       "\\[proof-prf] for goals;%s \\[proof-layout-windows] refreshes"
-      (if (or proof-three-window-enable 
+      (if (or proof-three-window-enable
 	      proof-multiple-frames-enable)
 	  ""
 	(format " \\[proof-display-some-buffers] rotates output%s;"
@@ -956,7 +958,7 @@ If CALLBACK is set, we invoke that when the command completes."
       (imenu-add-to-menubar "Index")
     (progn
       (when (listp which-func-modes)
-        (setq which-func-modes 
+        (setq which-func-modes
               (remove proof-mode-for-script which-func-modes)))
       (let ((oldkeymap (keymap-parent (current-local-map))))
 	(if ;; sanity checks in case someone else set local keymap
@@ -994,7 +996,8 @@ If CALLBACK is set, we invoke that when the command completes."
   "Stored incomplete input: string between point and locked.")
 
 (defun pg-previous-input (arg)
-  "Cycle backwards through input history, saving input."
+  "Cycle backwards through input history, saving input.
+If called interactively, ARG is given by the prefix argument."
   (interactive "*p")
   (if (and pg-input-ring-index
 	   (or			       ; leaving the "end" of the ring
@@ -1008,7 +1011,8 @@ If CALLBACK is set, we invoke that when the command completes."
     (pg-previous-matching-input "." arg)))
 
 (defun pg-next-input (arg)
-  "Cycle forwards through input history."
+  "Cycle forwards through input history.
+If called interactively, ARG is given by the prefix argument."
   (interactive "*p")
   (pg-previous-input (- arg)))
 
@@ -1198,7 +1202,7 @@ removed if it matches the last item in the ring."
 
 
 ;;;###autoload
-(defun  pg-clear-input-ring ()
+(defun pg-clear-input-ring ()
   (setq pg-input-ring nil))
 
 
@@ -1221,6 +1225,10 @@ removed if it matches the last item in the ring."
 (defun pg-protected-undo (&optional arg)
   "As `undo' but avoids breaking the locked region.
 
+A numeric ARG serves as a repeat count.
+If called interactively, ARG is given by the prefix argument.
+If ARG is omitted, nil, or not numeric, it takes the value 1.
+
 It performs each of the desired undos checking that these operations will
 not affect the locked region, obeying `proof-strict-read-only' if required.
 If strict read only behaviour is enforced, the user is queried whether to
@@ -1268,7 +1276,7 @@ behavior is expected."
 		 (> (proof-queue-or-locked-end) beg)
 		 proof-strict-read-only ; edit freely doesn't retract
 		 (not (and		; neither does edit in comments
-		       (proof-inside-comment beg) 
+		       (proof-inside-comment beg)
 		       (proof-inside-comment end))))
 	(if (or (eq proof-strict-read-only 'retract)
 		(y-or-n-p "Next undo will modify read-only region, retract? "))
@@ -1276,12 +1284,12 @@ behavior is expected."
 	  (when (eq last-command 'undo) (setq this-command 'undo))
 	  ;; now we can stop the function without breaking possible undo chains
 	  (error
-	   "Cannot undo without retracting to the appropriate position.")))
+	   "Cannot undo without retracting to the appropriate position")))
       (undo arg))))
 
 (defun next-undo-elt (arg)
-  "Returns the undo element that will be processed on next undo/redo,
-assuming the undo-in-region behavior will apply if ARG is non-nil."
+  "Return the undo element that will be processed on next undo/redo.
+Assume the undo-in-region behavior will apply if ARG is non-nil."
   (let ((undo-list (if arg		; handle "undo in region"
 		       (undo-make-selective-list
 			(region-beginning) (region-end)) ; can be '(nil)
@@ -1318,11 +1326,11 @@ assuming the undo-in-region behavior will apply if ARG is non-nil."
 ;;;###autoload
 (defun proof-autosend-enable (&optional nomsg)
   "Enable or disable autosend behaviour."
-  (if proof-autosend-timer 
+  (if proof-autosend-timer
       (cancel-timer proof-autosend-timer))
   (when proof-autosend-enable
     (setq proof-autosend-timer
-	  (run-with-idle-timer proof-autosend-delay 
+	  (run-with-idle-timer proof-autosend-delay
 			       t 'proof-autosend-loop))
     (setq proof-autosend-modified-tick nil)
     (unless nomsg (message "Automatic sending turned on.")))
@@ -1355,10 +1363,10 @@ assuming the undo-in-region behavior will apply if ARG is non-nil."
       (progn
 	(save-excursion
 	  (goto-char (point-max))
-	  (proof-assert-until-point 
-	   (if proof-multiple-frames-enable 
+	  (proof-assert-until-point
+	   (if proof-multiple-frames-enable
 	       'no-minibuffer-messages ; nb: not API
-	     '(no-response-display 
+	     '(no-response-display
 	       no-error-display
 	       no-goals-display))))
 	(proof-shell-wait t) ; interruptible
@@ -1381,9 +1389,9 @@ assuming the undo-in-region behavior will apply if ARG is non-nil."
 	  ;(skip-chars-forward " \t\n")
 	  (message "Trying next commands in prover...")
 	  (proof-assert-until-point
-	   (if proof-multiple-frames-enable 
+	   (if proof-multiple-frames-enable
 	       'no-minibuffer-messages ; nb: not API
-	     '(no-response-display 
+	     '(no-response-display
 	       no-error-display
 	       no-goals-display))))
 	(let ((proof-sticky-errors t))
@@ -1401,16 +1409,16 @@ assuming the undo-in-region behavior will apply if ARG is non-nil."
 	(unless (eq qol (proof-queue-or-locked-end)) ; no progress
 	  (save-excursion
 	    (goto-char qol)
-	    (proof-retract-until-point 
+	    (proof-retract-until-point
 	     (lambda (beg end)
-	       (span-make-self-removing-span 
+	       (span-make-self-removing-span
 		(save-excursion
 		  (goto-char beg)
 		  (skip-chars-forward " \t\n")
-		  (point)) 
+		  (point))
 		end
 		'face 'highlight))
-	     '(no-response-display 
+	     '(no-response-display
 	       no-error-display
 	       no-goals-display)))))))
   
diff --git a/generic/pg-vars.el b/generic/pg-vars.el
index 546c955e..d1e5dfa9 100644
--- a/generic/pg-vars.el
+++ b/generic/pg-vars.el
@@ -27,16 +27,16 @@
 ;;;
 
 (defvar proof-assistant-cusgrp nil
-  "Symbol for the customization group of the user options for the proof assistant.
+  "Symbol for the customization group of user options for the proof assistant.
 Do not change this variable! It is set automatically by the mode
 stub defined in proof-site, from the name given in
-proof-assistant-table.")
+‘proof-assistant-table’.")
 
 (defvar proof-assistant-internals-cusgrp nil
-  "Symbol for the customization group of the PG internal settings proof assistant.
+  "Symbol for the customization group of PG internal settings.
 Do not change this variable! It is set automatically by the mode
 stub defined in proof-site, from the name given in
-proof-assistant-table.")
+‘proof-assistant-table’.")
 
 (defvar proof-assistant ""
   "Name of the proof assistant Proof General is using.
@@ -217,7 +217,7 @@ the form of the menu entry for the setting (this is an Emacs widget type)
 and the DESCR description string is used as a help tooltip in the settings menu.
 
 As TYPE's only the simple types boolean, integer, number and
-string are supported (see `proof-menu-entry-for-setting'). Other
+string are supported (see `proof-menu-entry-for-setting').  Other
 types will yield an error when constructing the proof assistant
 menu from this list.
 
diff --git a/generic/pg-xml.el b/generic/pg-xml.el
index 5de8095d..18285572 100644
--- a/generic/pg-xml.el
+++ b/generic/pg-xml.el
@@ -61,6 +61,7 @@
 
 (defun pg-xml-parse-buffer (&optional buffer nomsg start end)
   "Parse an XML documment in BUFFER (defaulting to current buffer).
+Display progress message unless NOMSG is non-nil.
 Parsing according to `xml-parse-file' of xml.el.
 Optional START and END bound the parse."
   (unless nomsg
@@ -83,7 +84,7 @@ Optional START and END bound the parse."
     (or val
 	(if optional
 	    defaultval
-	  (pg-xml-error "pg-xml-get-attr: Didn't find required %s attribute in %s element"
+	  (pg-xml-error "Function pg-xml-get-attr: Didn't find required %s attribute in %s element"
 		 attribute (xml-node-name node))))))
 
 (defun pg-xml-child-elts (node)
@@ -100,7 +101,7 @@ Optional START and END bound the parse."
 			    (xml-node-name node)))))
 
 (defun pg-xml-get-child (child node)
-  "Return single element CHILD of node, give error if more than one."
+  "Return single element CHILD of NODE, give error if more than one."
   (let ((children (xml-get-children node child)))
     (if (> (length children) 1)
 	 (progn
@@ -141,8 +142,9 @@ Optional START and END bound the parse."
 ;; based on xml-debug-print from xml.el
 
 (defun pg-xml-output-internal (xml indent-string outputfn)
-  "Outputs the XML tree using OUTPUTFN, which should accept a list of args.
-Output with indentation INDENT-STRING (or none if nil)."
+  "Output the XML tree.
+Use indentation INDENT-STRING (or none if nil).
+Cal OUTPUTFN, which should accept a list of args."
   (let ((tree xml)
 	attlist)
     (funcall outputfn (or indent-string "") "<" (symbol-name (xml-node-name tree)))
@@ -167,7 +169,7 @@ Output with indentation INDENT-STRING (or none if nil)."
 	      (pg-xml-output-internal node (if indent-string (concat indent-string "  ")) outputfn))
 	     ((stringp node) (funcall outputfn node))
 	     (t
-	      (error "pg-xml-output-internal: Invalid XML tree"))))
+	      (error "Function pg-xml-output-internal: Invalid XML tree"))))
 
 	  (funcall outputfn (if indent-string (concat "\n" indent-string) "")
 		   "</" (symbol-name (xml-node-name xml)) ">"))
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 5cd83ddd..e93c4da2 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -292,7 +292,7 @@ Additional properties in the ARGS prop list may include:
 
  pgdynamic flag      If flag is non-nil, this setting is a dynamic one
 		     that is particular to the running instance of the prover.
-		     Automatically set by preferences configured from PGIP 
+		     Automatically set by preferences configured from PGIP
 		     askprefs message.
 
 This macro also extends the `proof-assistant-settings' list.
@@ -654,7 +654,7 @@ also as the 'response property on the span.
 
 Optional argument MOUSEFACE means use the given face as a mouse highlight
 face, if it is a face, otherwise, if it is non-nil but not a face,
-do not add a mouse highlight.  
+do not add a mouse highlight.
 
 In any case, a mouse highlight and tooltip are only set if
 `proof-output-tooltips' is non-nil.
@@ -783,7 +783,7 @@ Busy wait for `proof-shell-busy' to become nil, reading from prover.
 
 Needed between sequences of commands to maintain synchronization,
 because Proof General does not allow for the action list to be extended
-in some cases.   Also is considerably faster than leaving the Emacs 
+in some cases.   Also is considerably faster than leaving the Emacs
 top-level command loop to read from the prover.
 
 Called by `proof-shell-invisible-command' and `proof-process-buffer'
diff --git a/generic/proof-config.el b/generic/proof-config.el
index bd5ca611..ea7fda8f 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -259,7 +259,7 @@ or `proof-script-parse-function'."
   :group 'prover-config)
 
 (defcustom proof-script-sexp-commands nil
-  "Non-nil if script has LISP-like syntax: commands are top-level sexps.
+  "Non-nil if script has Lisp-like syntax: commands are top-level sexps.
 You should set this variable in script mode configuration.
 
 To configure command recognition properly, you must set at least one
@@ -411,11 +411,11 @@ It's safe to leave this setting as nil."
   :group 'proof-script)
 
 (defcustom proof-save-with-hole-result 2
-  "How to get theorem name after `proof-save-with-hole-regexp' match.
+  "How to get theorem name after ‘proof-save-with-hole-regexp’ match.
 String or Int.
-If an int N use match-string to recover the value of the Nth parenthesis matched.
-If it is a string use replace-match. In this case, `proof-save-with-hole-regexp'
-should match the entire command"
+If an int N, use ‘match-string’ to get the value of the Nth parenthesis matched.
+If a string, use ‘replace-match’.  In this case, ‘proof-save-with-hole-regexp’
+should match the entire command."
   :type '(choice string integer)
   :group 'proof-script)
 
@@ -441,11 +441,11 @@ It's safe to leave this setting as nil."
   :group 'proof-script)
 
 (defcustom proof-goal-with-hole-result 2
-  "How to get theorem name after `proof-goal-with-hole-regexp' match.
+  "How to get theorem name after ‘proof-goal-with-hole-regexp’ match.
 String or Int.
-If an int N use match-string to recover the value of the Nth parenthesis matched.
-If it is a string use replace-match. In this case, proof-save-with-hole-regexp
-should match the entire command"
+If an int N, use ‘match-string’ to get the value of the Nth parenthesis matched.
+If a string, use ‘replace-match’.  In this case, ‘proof-goal-with-hole-regexp’
+should match the entire command."
   :type '(choice string integer)
   :group 'proof-script)
 
@@ -683,10 +683,10 @@ assistant, for example, to compile a completed file."
 (defcustom proof-no-fully-processed-buffer nil
   "Set to t if buffers should always retract before scripting elsewhere.
 Leave at nil if fully processed buffers make sense for the current
-proof assistant. If nil the user can choose to fully assert a
-buffer when starting scripting in a different buffer. If t there
+proof assistant.  If nil the user can choose to fully assert a
+buffer when starting scripting in a different buffer.  If t there
 is only the choice to fully retract the active buffer before
-starting scripting in a different buffer. This last behavior is
+starting scripting in a different buffer.  This last behavior is
 needed for Coq."
   :type 'boolean
   :group 'proof-script)
@@ -760,12 +760,12 @@ Elisp errors will be trapped when evaluating; set
   :group 'proof-script)
 
 (defcustom proof-script-insert-newlines t
-  "if non-nil inserts a newline between each message in response buffer."
+  "If non-nil, insert a newline between each message in response buffer."
   :type 'boolean
   :group 'proof-script)
 
 (defcustom proof-script-color-error-messages t
-  "if non-nil error messages will be globally colored with corresponding face.
+  "If non-nil, error messages will be globally colored with corresponding face.
 If prover mode has a better coloring mechanism for errors, set this to nil."
   :type 'boolean
   :group 'proof-script)
@@ -1195,18 +1195,18 @@ If nil, use the whole of the output from the match on
   :group 'proof-shell)
 
 (defcustom proof-shell-empty-action-list-command nil
-  "A function returning a list of commands (strings) to be sent
-to the prover when the last command in the queue has been
-performed. Typically to ask for some informational
-display (goals, etc).
+  "A function returning a list of commands (strings).
+These commands are sent to the prover when the last command in the queue
+has been performed.
+Typically to ask for some informational display (goals, etc.)
 
 The function takes as argument the last command in the queue.
 
-NOTE 1: The commands will be tagged invisible, i.e. not related
+NOTE 1: The commands will be tagged invisible, i.e., not related
 to a place in the buffer.
 
 NOTE 2: The commands should NOT have any effect on the state of
-the prover. Otherwise running the script outside pg would be
+the prover.  Otherwise running the script outside pg would be
 inconsistent."
   :type 'function
   :group 'proof-shell)
@@ -1563,7 +1563,7 @@ This setting is used inside the function `proof-format-filename'."
   "The value of `process-connection-type' for the proof shell.
 Set non-nil for ptys, nil for pipes.
 
-NOTE: In emacs >= 24 (checked for 24 and 25.0.50.1), t is not a
+NOTE: In Emacs >= 24 (checked for 24 and 25.0.50.1), t is not a
 good choice: input is cut after 4095 chars, which hangs pg."
   :type 'boolean
   :group 'proof-shell)
@@ -1589,14 +1589,14 @@ if you don't need it (slight speed penalty)."
   :group 'proof-shell)
 
 (defcustom proof-shell-extend-queue-hook nil
-  "Hooks run by proof-extend-queue before extending `proof-action-list'.
+  "Hooks run by ‘proof-extend-queue’ before extending `proof-action-list'.
 Can be used to run additional actions before items are added to
 the queue \(such as compiling required modules for Coq) or to
 modify the items that are going to be added to
-`proof-action-list'. The items that are about to be added are
+`proof-action-list'.  The items that are about to be added are
 bound to `queueitems'."
   :type '(repeat function)
-  :group 'proof-shell)  
+  :group 'proof-shell)
 
 (defcustom proof-shell-insert-hook nil
   "Hooks run by `proof-shell-insert' before inserting a command.
@@ -1644,12 +1644,12 @@ it is added to the queue of commands."
 (defcustom proof-assert-command-hook nil
   "Hooks run before asserting a command (or a set of commands).
 Can be used to insert commands before any (set of) input sent
-by the user. It is run by `proof-assert-until-point'.
+by the user.  It is run by `proof-assert-until-point'.
 
 WARNING: don't call `proof-assert-until-point' in this hook, you
 would loop forever.
 
-Example of use: Insert a command to adapt printing width. Note
+Example of use: Insert a command to adapt printing width.  Note
 that `proof-shell-insert-hook' may be use instead (see lego mode)
 if no more prompt will be displayed (see
 `proof-shell-insert-hook' for details)."
@@ -1658,13 +1658,13 @@ if no more prompt will be displayed (see
 
 (defcustom proof-retract-command-hook nil
   "Hooks run before retracting a command (or a set of commands).
-Can be used to insert commands. It is run by
+Can be used to insert commands.  It is run by
 `proof-retract-until-point'.
 
 WARNING: don't call `proof-retract-until-point' in this hook, you
 would loop forever.
 
-Example of use: Insert a command to adapt printing width. Note
+Example of use: Insert a command to adapt printing width.  Note
 that `proof-shell-insert-hook' may be use instead (see lego mode)
 if no more prompt will be displayed (see
 `proof-shell-insert-hook' for details)."
@@ -1704,14 +1704,14 @@ something in scripting buffer, `save-excursion' and/or `set-buffer'."
 (defcustom proof-shell-signal-interrupt-hook nil
   "Run when the user tries to interrupt the prover.
 This hook is run inside `proof-interrupt-process' when the user
-tries to interrupt the proof process. It is therefore run earlier
+tries to interrupt the proof process.  It is therefore run earlier
 than `proof-shell-handle-error-or-interrupt-hook', which runs
 when the interrupt is acknowledged inside `proof-shell-exec-loop'.
 
 This hook also runs when the proof assistent is killed.
 
 Hook functions should set the dynamic variable `prover-was-busy'
-to t if there might have been a reason to interrupt. Otherwise
+to t if there might have been a reason to interrupt.  Otherwise
 the generic interrupt handler might issue a prover-not-busy
 error."
   :type '(repeat function)
diff --git a/generic/proof-depends.el b/generic/proof-depends.el
index 74332c71..72beb1d2 100644
--- a/generic/proof-depends.el
+++ b/generic/proof-depends.el
@@ -181,7 +181,7 @@ Called from `proof-done-advancing' when a save is processed and
       (vector menuname nil nil))))
 
 (defun proof-dep-split-deps (deps)
-  "Split dependencies into named nested lists according to dotted prefixes."
+  "Split dependencies DEPS into named nested lists according to dotted prefixes."
   ;; NB: could handle deeper nesting here, but just do one level for now.
   (let (nested toplevel)
     ;; Add each name into a nested list or toplevel list
@@ -223,6 +223,7 @@ NAMEFN is applied to each element of LIST to make the names."
 
 (defun proof-goto-dependency (name span)
   "Go to the start of SPAN."
+  ;; FIXME(EMD): seems buggy as NAME is not used
   ;; FIXME: check buffer is right one.  Later we'll allow switching buffer
   ;; here and jumping to different files.
   (goto-char (span-start span))
diff --git a/generic/proof-easy-config.el b/generic/proof-easy-config.el
index 59fa03e5..4dc2e1d4 100644
--- a/generic/proof-easy-config.el
+++ b/generic/proof-easy-config.el
@@ -62,7 +62,8 @@
        `(define-derived-mode ,mode ,parent ,modename nil ,@fullbody)))))
 
 (defun proof-easy-config-check-setup (sym name)
-  "A number of simple checks."
+  "Perform a number of simple checks.
+The proof assistant is denoted by symbol SYM and string NAME."
   (let ((msg ""))
     ;; At the moment we just check that the symbol/name used
     ;; in the macro matches that in `proof-assistant-table'
@@ -84,7 +85,7 @@
 	    (not (eq proof-assistant-symbol sym))
 	    (setq msg (format "\nproof-assistant symbol: '%s doesn't match expected '%s"
 			      proof-assistant-symbol sym))))
-      (error "proof-easy-config: PG already in use or name/symbol mismatch %s"
+      (error "Macro proof-easy-config: PG already in use or name/symbol mismatch %s"
 	     msg))
      (t
       ;; Setting these here is nice for testing: no need to get
@@ -94,9 +95,10 @@
 
 ;;;###autoload
 (defmacro proof-easy-config (sym name &rest body)
-  "Configure Proof General for proof-assistant using BODY as a setq body.
+  "Configure Proof General for a given proof assistant.
 The symbol SYM and string name NAME must match those given in
-the `proof-assistant-table', which see."
+  the `proof-assistant-table', which see.
+Additional arguments are taken into account as a setq BODY."
   `(progn
      (proof-easy-config-check-setup ,sym ,name)
      (setq
@@ -105,3 +107,7 @@ the `proof-assistant-table', which see."
 
 ;;
 (provide 'proof-easy-config)
+
+(provide 'proof-easy-config)
+
+;;; proof-easy-config.el ends here
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index f893a9f6..fc18d504 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -318,7 +318,7 @@ without adjusting window layout."
 (proof-deftoggle proof-delete-empty-windows)
 (proof-deftoggle proof-shrink-windows-tofit)
 (proof-deftoggle proof-multiple-frames-enable proof-multiple-frames-toggle)
-(proof-deftoggle proof-layout-windows-on-visit-file 
+(proof-deftoggle proof-layout-windows-on-visit-file
 		 proof-layout-windows-eagerly-toggle)
 (proof-deftoggle proof-three-window-enable proof-three-window-toggle)
 (proof-deftoggle proof-auto-raise-buffers proof-auto-raise-toggle)
@@ -342,7 +342,7 @@ without adjusting window layout."
    (proof-ass-sym maths-menu-enable) 'proof-maths-menu-toggle))
 
 (defun proof-keep-response-history ()
-  "Enable associated buffer histories following `proof-keep-response-history'."
+  "Enable associated buffer histories following option `proof-keep-response-history'."
   (if proof-keep-response-history
       (proof-map-buffers (proof-associated-buffers) (bufhist-init))
     (proof-map-buffers (proof-associated-buffers) (bufhist-exit))))
@@ -371,7 +371,7 @@ without adjusting window layout."
       ["Beep on Errors" proof-shell-quiet-errors-toggle
        :style toggle
        :selected (not proof-shell-quiet-errors)
-       :help "Beep on errors or interrupts"]      
+       :help "Beep on errors or interrupts"]
       ["Fly Past Comments" proof-script-fly-past-comments-toggle
        :style toggle
        :selected proof-script-fly-past-comments
@@ -613,7 +613,7 @@ without adjusting window layout."
 ;;
 
 (defun proof-set-document-centred ()
-  "Select options for document-centred working"
+  "Select options for document-centred working."
   (interactive)
   (proof-full-annotation-toggle 1)
   (proof-auto-raise-toggle 0)
@@ -626,9 +626,9 @@ without adjusting window layout."
 
 
 (defun proof-set-non-document-centred ()
-  "Set options for classic Proof General interaction"
+  "Set options for classic Proof General interaction."
   (interactive)
-  ;; default: (proof-full-annotation-toggle 1) 
+  ;; default: (proof-full-annotation-toggle 1)
   (proof-auto-raise-toggle 1)
   (proof-colour-locked-toggle 1)
   (proof-sticky-errors-toggle 0)
@@ -744,7 +744,7 @@ without adjusting window layout."
 ;;; Define stuff from favourites
 
 (defun proof-def-favourite (command inscript menuname &optional key new)
-  "Define and a \"favourite\" proof assisant function.
+  "Define and a \"favourite\" proof assistant function.
 See doc of `proof-add-favourite' for first four arguments.
 Extra NEW flag means that this should be a new favourite, so check
 that function defined is not already bound.
@@ -987,7 +987,7 @@ We first clear the dynamic settings from `proof-assistant-settings'."
   (let (cmds)
     (dolist (setting proof-assistant-settings)
       (let ((sym       (car setting))
-	    (pacmd     (cadr setting))) 
+	    (pacmd     (cadr setting)))
 	(if (and pacmd
 		 (or (not (get sym 'pgdynamic))
 		     (proof-ass-differs-from-default sym)))
@@ -1038,7 +1038,7 @@ value) and the second for false."
 	  ((consp string)     ;; true/false options
 	   (if curvalue (car string) (cdr string)))
 	  (t ;; no idea what to do
-	   (error "proof-assistant-format: called with invalid string arg %s" string)))))
+	   (error "Function proof-assistant-format: called with invalid string arg %s" string)))))
     (if proof-assistant-setting-format
 	(funcall proof-assistant-setting-format setting)
       setting)))
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 0baf3d5f..3a663a3a 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -287,8 +287,8 @@ next time an error is processed."
 (defun proof-restart-buffers (buffers)
   "Remove all extents in BUFFERS and maybe reset `proof-script-buffer'.
 The high-level effect is that all members of BUFFERS are
-completely unlocked, including all the necessary cleanup. No
-effect on a buffer which is nil or killed. If one of the buffers
+completely unlocked, including all the necessary cleanup.  No
+effect on a buffer which is nil or killed.  If one of the buffers
 is the current scripting buffer, then `proof-script-buffer' will
 deactivated."
   (mapcar
@@ -416,7 +416,7 @@ Works on any buffer."
   (eq (proof-unprocessed-begin) (point-min)))
 
 (defun proof-only-whitespace-to-locked-region-p ()
-  "Non-nil if only whitespace from char-after point and end of locked region.
+  "Non-nil if only whitespace from char after point to end of locked region.
 Point must be after the locked region or this will signal an error."
   (save-excursion
     (or (eq (point) (point-max))
@@ -510,7 +510,7 @@ Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'."
     (clrhash (cdr idtbl))))
 
 (defun pg-remove-element (idiom id)
-  "Remove the identifier ID from the script portion IDIOM."
+  "From the script portion IDIOM, remove the identifier ID."
   (let* ((elts (cdr-safe (assq idiom pg-script-portions)))
 	 (span (and elts (gethash idiom elts))))
     (when span
@@ -518,8 +518,8 @@ Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'."
       (remhash id elts))))
 
 (defun pg-get-element (idiomsym id)
-  "Return proof script element of type IDIOM identifier ID.
-IDIOM is a symbol, ID is a string."
+  "Return proof script element of type IDIOMSYM with identifier ID.
+IDIOMSYM is a symbol, ID is a string."
   (assert (symbolp idiomsym))
   (assert (stringp id))
   (let ((idsym  (intern id))
@@ -581,15 +581,15 @@ This is a value for the overlay 'invisible property."
   (intern (concat "pg-" (symbol-name (or idiom 'other)))))
 
 (defun pg-set-element-span-invisible (span invisiblep)
-  "Function to adjust visibility of span to INVISIBLEP.
+  "Function to adjust visibility of SPAN to INVISIBLEP.
 We use list values of the 'invisible property which contain
 private symbols, that should play well with other conforming modes
 and `buffer-invisibility-spec'."
   (let* ((invisible-prop  (pg-invisible-prop (span-property span 'idiom)))
 	 (invisible-rest  (remq invisible-prop
 				(span-property span 'invisible))))
-    (span-set-property span 'invisible 
-		       (if invisiblep 
+    (span-set-property span 'invisible
+		       (if invisiblep
 			   (cons invisible-prop invisible-rest)
 			 invisible-rest))))
 		       
@@ -604,12 +604,12 @@ and `buffer-invisibility-spec'."
   (pg-set-element-span-invisible span invisible))
 
 (defun pg-make-element-invisible (idiomsym id)
-  "Make element ID of type IDIOMSYM invisible, with ellipsis."
+  "Make element of type IDIOMSYM and identifier ID invisible, with ellipsis."
   (let ((span (pg-get-element idiomsym id)))
     (if span (pg-set-element-span-invisible span t))))
 
 (defun pg-make-element-visible (idiomsym id)
-  "Make element ID of type IDIOMSYM visible."
+  "Make element of type IDIOMSYM and identifier ID visible."
   (let ((span (pg-get-element idiomsym id)))
     (if span (pg-set-element-span-invisible span nil))))
 
@@ -625,8 +625,8 @@ IDIOMSYM is a symbol and ID is a strings."
    (list
     (intern
      (completing-read
-      (concat "Make " 
-	      (if current-prefix-arg "in" "") 
+      (concat "Make "
+	      (if current-prefix-arg "in" "")
 	      "visible all regions of: ")
       (apply 'vector pg-idioms) nil t))
     current-prefix-arg))
@@ -641,7 +641,7 @@ IDIOMSYM is a symbol and ID is a strings."
        (maphash alterfn elts)))))
 
 (defun pg-add-proof-element (name span controlspan)
-  "Add a span proof element to SPAN with name NAME and parent CONTROLSPAN."
+  "Add a span proof element (named NAME) to SPAN with parent CONTROLSPAN."
   (let ((proofid   (proof-next-element-id 'proof)))
     (pg-add-element 'proof proofid span name)
     ;; Set id in controlspan [NB: intern here means symbol-name elsewhere]
@@ -665,8 +665,7 @@ Each span has a 'type property, one of:
     'vanilla      Initialised in proof-semis-to-vanillas, for
     'comment      A comment outside a command.
     'proverproc   A region closed by the prover, processed outwith PG
-    'pbp	  A PBP command inserted automatically into the script
-"
+    'pbp	  A PBP command inserted automatically into the script."
   (let ((type    (span-property span 'type))
 	(idiom   (span-property span 'idiom))
 	(name    (span-property span 'name))
@@ -995,7 +994,7 @@ Gives a message in the minibuffer and busy-waits for the retraction
 or processing to complete.  If it fails for some reason,
 an error is signalled here."
   (unless (or (eq action 'process) (eq action 'retract))
-    (error "proof-protected-process-or-retract: invalid argument"))
+    (error "Invalid argument (in proof-protected-process-or-retract)"))
   (let ((buf (or buffer (current-buffer))))
     (with-current-buffer buf
       (unless (proof-action-completed action)
@@ -1093,7 +1092,7 @@ retract or assert, or automatically take the action indicated in the
 user option `proof-auto-action-when-deactivating-scripting'.
 
 If `proof-no-fully-processed-buffer' is t there is only the choice
-to fully retract the active scripting buffer. In this case the
+to fully retract the active scripting buffer.  In this case the
 active scripting buffer is retracted even if it was fully processed.
 Setting `proof-auto-action-when-deactivating-scripting' to 'process
 is ignored in this case.
@@ -1117,7 +1116,7 @@ questioning the user.  It is used to make a value for
 the `kill-buffer-hook' for scripting buffers, so that when
 a scripting buffer is killed it is always retracted."
   (interactive)
-  (proof-with-current-buffer-if-exists 
+  (proof-with-current-buffer-if-exists
    proof-script-buffer
    ;; Examine buffer.
 
@@ -1277,7 +1276,7 @@ activation is considered to have failed and an error is given."
 		      (eq 'interrupt proof-shell-last-output-kind))
 	      (proof-deactivate-scripting) ;; turn off again!
 	      ;; Give an error to prevent further actions.
-	      (error 
+	      (error
 	       "Scripting not activated because of error or interrupt")))))))
 
 
@@ -1405,7 +1404,7 @@ Argument SPAN has just been processed."
     (pg-add-element 'comment id bodyspan)
     (span-set-property span 'id (intern id))
     (span-set-property span 'idiom 'comment)
-    (let ((proof-shell-last-output "")) ; comments not sent, no last output 
+    (let ((proof-shell-last-output "")) ; comments not sent, no last output
       (pg-set-span-helphighlights bodyspan))
 
     ;; possibly evaluate some arbitrary Elisp.  SECURITY RISK!
@@ -1512,8 +1511,9 @@ Argument SPAN has just been processed."
 
 (defun proof-make-goalsave
   (gspan goalend savestart saveend nam &optional nestedundos)
-  "Make new goal-save span, using GSPAN. Subroutine of `proof-done-advancing-save'.
-Argument GOALEND is the end of the goal;."
+  "Make new goal-save span, using GSPAN.
+Subroutine of `proof-done-advancing-save'.
+Argument GOALEND is the end of the goal."
   (unless proof-arbitrary-undo-positions
     (span-set-end gspan saveend)
     (span-set-property gspan 'type 'goalsave))
@@ -1646,7 +1646,7 @@ Subroutine of `proof-done-advancing-save'."
 This partitions the script buffer into contiguous regions, classifying
 them by type.  Return a list of lists of the form
   
-   (TYPE TEXT ENDPOS)
+  \(TYPE TEXT ENDPOS)
 
 where:
 
@@ -1860,8 +1860,8 @@ The optional QUEUEFLAGS are added to each queue item."
 		(span-set-property span 'cmd cmd)
 		(setq alist (cons qitem alist))))
 	  ;; ignored text
-	  (let ((qitem  
-		 (list span nil cb queueflags))) ; nil was `proof-no-command' 
+	  (let ((qitem
+		 (list span nil cb queueflags))) ; nil was `proof-no-command'
 	  (span-set-property span 'type 'comment)
 	    (setq alist (cons qitem alist))))
 	(setq start end)))
@@ -1923,7 +1923,7 @@ try to avoid duplicating them in the buffer.
 When used in the locked region (and so with strict read only off), it
 always defaults to inserting a semi (nicer might be to parse for a
 comment, and insert or skip to the next semi)."
-  (let ((mrk         (point)) 
+  (let ((mrk         (point))
 	(termregexp  (regexp-quote proof-terminal-string))
 	ins incomment nwsp)
     (if (< mrk (proof-unprocessed-begin))
@@ -2045,9 +2045,8 @@ We update display after proof process has reset its state.
 See also the documentation for `proof-retract-until-point'.
 Optionally delete the region corresponding to the proof sequence.
 After an undo, we clear the proof completed flag.  The rationale
-is that undoing never leaves prover in a \"proof just completed\"
-state, which is true for some proof assistants (but probably not
-others)."
+is that undoing never leaves prover in a \"proof just completed\" state,
+which is true for some proof assistants (but probably not others)."
   ;; TODO: need to fixup proof-nesting-depth
   (setq proof-shell-proof-completed nil)
   (if (span-live-p span)
@@ -2074,7 +2073,7 @@ others)."
   ;; State of scripting may have changed now
   (run-hooks 'proof-state-change-hook))
 
-(defun proof-setup-retract-action (start end proof-commands remove-action &optional 
+(defun proof-setup-retract-action (start end proof-commands remove-action &optional
 					 displayflags)
   "Make span from START to END which corresponds to retraction.
 Returns retraction action destined for proof shell queue, and make span.
@@ -2186,7 +2185,7 @@ DISPLAYFLAGS control output shown to user, see `proof-action-list'."
 			      undo-action
 			      displayflags))))
 
-    (proof-start-queue (min start end) (proof-unprocessed-begin) 
+    (proof-start-queue (min start end) (proof-unprocessed-begin)
 		       actions 'retracting)))
 
 (defun proof-retract-until-point-interactive (&optional delete-region)
@@ -2195,7 +2194,7 @@ If invoked outside a locked region, undo the last successfully processed
 command.  If called with a prefix argument (DELETE-REGION non-nil), also
 delete the retracted region from the proof-script."
   (interactive "P")
-  (proof-retract-until-point 
+  (proof-retract-until-point
    (if delete-region 'kill-region)))
 
 (defun proof-retract-until-point (&optional undo-action displayflags)
@@ -2205,8 +2204,8 @@ the locked region.  If invoked outside the locked region, undo
 the last successfully processed command.  See `proof-retract-target'.
 
 After retraction has succeeded in the prover, the filter will call
-`proof-done-retracting'.  If UNDO-ACTION is non-nil, it will 
-then be invoked on the region in the proof script corresponding to 
+`proof-done-retracting'.  If UNDO-ACTION is non-nil, it will
+then be invoked on the region in the proof script corresponding to
 the proof command sequence.
 DISPLAYFLAGS control output shown to user, see `proof-action-list'.
 
@@ -2218,7 +2217,7 @@ of effects:
 for scripting again which may involve retracting
 other (dependent) files.
 
-2. We may query the user whether to save some buffers.  
+2. We may query the user whether to save some buffers.
 
 Step 2 may seem odd -- we're undoing (in) the buffer, after all
 -- but what may happen is that when scripting starts going
@@ -2371,9 +2370,9 @@ mode features, but are only ever processed atomically by the proof
 assistant."
   (setq proof-script-buffer-file-name buffer-file-name)
 
-  (setq font-lock-defaults 
+  (setq font-lock-defaults
 	(list '(proof-script-font-lock-keywords)
-	      ;; see defadvice in proof-syntax 
+	      ;; see defadvice in proof-syntax
 	      (fboundp (proof-ass-sym font-lock-fontify-syntactically-region))))
 
   ;; Has buffer already been processed?
@@ -2593,7 +2592,7 @@ finish setup which depends on specific proof assistant configuration."
 
   ;; Invisibility management: show ellipsis
   (mapc (lambda (p)
-	    (add-to-invisibility-spec 
+	    (add-to-invisibility-spec
 	     (cons (pg-invisible-prop p) t)))
 	  pg-all-idioms)
 
@@ -2686,7 +2685,7 @@ Stores recent results of `proof-segment-up-to' in reverse order.")
     (if (and
 	 proof-use-parser-cache      ;; safety off valve
 	 proof-segment-up-to-cache
-	 (>= (proof-queue-or-locked-end) 
+	 (>= (proof-queue-or-locked-end)
 	     proof-segment-up-to-cache-start)
 	 (setq res (proof-segment-cache-contents-for pos))
 	 ;; only use result if last edit point is >1 segment below
@@ -2710,7 +2709,7 @@ Stores recent results of `proof-segment-up-to' in reverse order.")
 
 (defun proof-segment-cache-contents-for (pos)
   ;; only return result if we have cache for complete region
-  (when (<= pos proof-segment-up-to-cache-end) 
+  (when (<= pos proof-segment-up-to-cache-end)
     (let ((semis   proof-segment-up-to-cache)
 	  (start  (proof-queue-or-locked-end))
 	  usedsemis semiend)
@@ -2719,7 +2718,7 @@ Stores recent results of `proof-segment-up-to' in reverse order.")
 	(if (> semiend start)
 	    (setq usedsemis (cons (car semis) usedsemis)))
 	(setq semis
-	      (if (or (< semiend pos) 
+	      (if (or (< semiend pos)
 		      ;; matches parsing-until-find-something behaviour
 		      (and (= semiend pos) (not usedsemis)))
 		  (cdr semis))))
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 00d8b1d7..b5bbcd9f 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -59,12 +59,12 @@ The value is a list of lists of the form
 
 which is the queue of things to do.
 
-SPAN is a region in the sources, where COMMANDS come from. Often,
+SPAN is a region in the sources, where COMMANDS come from.  Often,
 additional properties are recorded as properties of SPAN.
 
 COMMANDS is a list of strings, holding the text to be send to the
-prover. It might be the empty list if nothing needs to be sent to
-the prover, such as, for comments. Usually COMMANDS
+prover.  It might be the empty list if nothing needs to be sent to
+the prover, such as, for comments.  Usually COMMANDS
 contains just 1 string, but it might also contains more elements.
 The text should be obtained with
 `(mapconcat 'identity COMMANDS \" \")', where the last argument
@@ -105,14 +105,13 @@ See the functions `proof-start-queue' and `proof-shell-exec-loop'.")
   "Signals that some items are waiting outside of `proof-action-list'.
 If this is t it means that some items from the queue region are
 waiting for being processed in a place different from
-`proof-action-list'. In this case Proof General must behave as if
-`proof-action-list' would be non-empty, when it is, in fact,
-empty.
+`proof-action-list'.  In this case Proof General must behave as if
+`proof-action-list' would be non-empty, when it is, in fact, empty.
 
 This is used, for instance, for parallel background compilation
 for Coq: The Require command and the following items are not put
 into `proof-action-list' and are stored somewhere else until the
-background compilation finishes. Then those items are put into
+background compilation finishes.  Then those items are put into
 `proof-action-list' for getting processed.")
 
 
@@ -158,8 +157,8 @@ from calling `proof-shell-exit'.")
 ;;
 
 (defcustom proof-shell-active-scripting-indicator
-  '(:eval (propertize 
-   " Scripting " 'face 
+  '(:eval (propertize
+   " Scripting " 'face
    (cond
     (proof-shell-busy			       'proof-queue-face)
     ((eq proof-shell-last-output-kind 'error)  'proof-script-sticky-error-face)
@@ -224,7 +223,7 @@ No change to current buffer or point."
 
 ;;;###autoload
 (defsubst proof-shell-live-buffer ()
-  "Return non-nil if proof-shell-buffer is live."
+  "Return non-nil if ‘proof-shell-buffer’ is live."
   (and proof-shell-buffer
        (buffer-live-p proof-shell-buffer)
        (scomint-check-proc proof-shell-buffer)))
@@ -262,10 +261,10 @@ If QUEUEMODE is supplied, set the lock to that value."
   :group 'proof-shell)
 
 (defvar proof-shell-filter-active nil
-  "t when `proof-shell-filter' is running.")
+  "Variable equal to t if `proof-shell-filter' is running.")
 
 (defvar proof-shell-filter-was-blocked nil
-  "t when a recursive call of `proof-shell-filter' was blocked.
+  "Variable equal to t if a recursive call of `proof-shell-filter' was blocked.
 In this case `proof-shell-filter' must be called again after it finished.")
 
 (defun proof-shell-set-text-representation ()
@@ -358,7 +357,7 @@ process command."
 	     
 	    
 	     ;; The next few settings control the proof assistant encoding.
-	     ;; See Elisp manual for recommendations for coding systems.  
+	     ;; See Elisp manual for recommendations for coding systems.
 	     
 	     ;; Modern versions of proof systems should be Unicode
 	     ;; clean, i.e., outputing only ASCII characters or using a
@@ -376,7 +375,7 @@ process command."
 			(cons
 			 (if (getenv "LANG")
 			     (format "LANG=%s"
-				     (replace-regexp-in-string 
+				     (replace-regexp-in-string
 				      "\\.UTF-8" ""
 				      (getenv "LANG")))
 			   "LANG=C")
@@ -487,7 +486,7 @@ shell buffer, called by `proof-shell-bail-out' if process exits."
     (when (and alive proc)
       (catch 'exited
 	(setq proof-shell-exit-in-progress t)
-	(set-process-sentinel 
+	(set-process-sentinel
 	 proc
 	 (lambda (p m) (throw 'exited t)))
 	
@@ -520,7 +519,7 @@ shell buffer, called by `proof-shell-bail-out' if process exits."
     (proof-shell-clear-state)
     (run-hooks 'proof-shell-kill-function-hooks)
 
-    ;; Remove auxiliary windows, trying to stop proliferation of 
+    ;; Remove auxiliary windows, trying to stop proliferation of
     ;; frames (NB: loses if user has switched buffer in special frame)
     (if (and proof-multiple-frames-enable
 	     proof-shell-fiddle-frames)
@@ -558,7 +557,7 @@ shell buffer, called by `proof-shell-bail-out' if process exits."
 
 This simply kills the `proof-shell-buffer' relying on the hook function
 
-`proof-shell-kill-function' to do the hard work. If optional
+`proof-shell-kill-function' to do the hard work.  If optional
 argument DONT-ASK is non-nil, the proof process is terminated
 without confirmation.
 
@@ -680,7 +679,7 @@ In both cases we then sound a beep, clear the queue and spans and
 finally we call `proof-shell-handle-error-or-interrupt-hook'.
 
 Commands which are not part of regular script management (with
-non-empty flags='no-error-display) will not cause any display action.
+FLAGS containing 'no-error-display) will not cause any display action.
 
 This is called in two places: (1) from the output processing
 functions, in case we find an error or interrupt message output,
@@ -697,7 +696,7 @@ didn't cause prover output."
        "Interrupt: script management may be in an inconsistent state
 	   (but it's probably okay)"))
      (t ; error
-      (if proof-shell-delayed-output-start 
+      (if proof-shell-delayed-output-start
 	  (save-excursion
 	    (proof-shell-handle-delayed-output)))
       (proof-shell-handle-error-output
@@ -724,11 +723,11 @@ unless the FLAGS for the command are non-nil (see `proof-action-list')."
 
     (proof-with-current-buffer-if-exists proof-script-buffer
       (save-excursion
-	(proof-script-clear-queue-spans-on-error badspan 
+	(proof-script-clear-queue-spans-on-error badspan
 						 (eq err-or-int 'interrupt))))
     ;; Note: coq-par-emergency-cleanup, which might be called via
     ;; proof-shell-handle-error-or-interrupt-hook below, assumes that
-    ;; proof-action-list is empty on error. 
+    ;; proof-action-list is empty on error.
     (setq proof-action-list nil)
     (proof-release-lock)
     (unless flags
@@ -739,7 +738,7 @@ unless the FLAGS for the command are non-nil (see `proof-action-list')."
       (run-hooks 'proof-shell-handle-error-or-interrupt-hook))))
 
 (defun proof-goals-pos (span maparg)
-  "Given a span, return the start of it if corresponds to a goal, nil otherwise."
+  "Given a SPAN, return the start of it if corresponds to a goal, nil otherwise."
   (and (eq 'goal (car (span-property span 'proof-top-element)))
        (span-start span)))
 
@@ -756,7 +755,7 @@ This is a hook function for proof-shell-handle-delayed-output-hook."
 
 
 (defsubst proof-shell-string-match-safe (regexp string)
-  "Like string-match except returns nil if REGEXP is nil."
+  "Like (string-match REGEXP STRING), but return nil if REGEXP is nil."
   (and regexp (string-match regexp string)))
 
 (defun proof-shell-handle-immediate-output (cmd start end flags)
@@ -787,7 +786,7 @@ after a completed proof."
   (cond
    ;; TODO: Isabelle has changed (since 2009) and is now amalgamating
    ;; output between prompts, and does e.g.,
-   ;;   GOALS 
+   ;;   GOALS
    ;;   ERROR
    ;; we need to override delayed output from the previous
    ;; command with delayed output from this command to handle that!
@@ -878,9 +877,9 @@ single string.
 The ACTION argument is a symbol which is typically the name of a
 callback for when each string has been processed.
 
-This calls `proof-shell-insert-hook'.  The arguments `action' and
-`scriptspan' may be examined by the hook to determine how to modify
-the `string' variable (exploiting dynamic scoping) which will be
+This calls `proof-shell-insert-hook'.  The arguments ACTION and
+SCRIPTSPAN may be examined by the hook to determine how to modify
+the string variable (exploiting dynamic scoping) which will be
 the command actually sent to the shell.
 
 Note that the hook is not called for the empty (null) string
@@ -959,7 +958,7 @@ track what happens in the proof queue."
   "Non-nil if we should switch to silent mode based on size of queue."
   (if (and proof-shell-start-silent-cmd ; configured
 	   (not proof-full-annotation)  ; always noisy
-	   (not proof-tree-external-display) ; no proof-tree display 
+	   (not proof-tree-external-display) ; no proof-tree display
 	   (not proof-shell-silent))	; already silent
 	  ;; NB: to be more accurate we should only count number
 	  ;; of scripting items in the list (not e.g. invisibles).
@@ -1044,7 +1043,7 @@ being processed."
 			      proof-action-list)
 		      (cons (car proof-action-list) ; after current
 			    (cons (proof-shell-stop-silent-item)
-				  (cdr proof-action-list))))))	  
+				  (cdr proof-action-list))))))
 	  (when nothingthere  ; start sending commands
 	    (proof-grab-lock queuemode)
 	    (setq proof-shell-last-output-kind nil)
@@ -1059,11 +1058,11 @@ being processed."
 
 ;;;###autoload
 (defun proof-start-queue (start end queueitems &optional queuemode)
-  "Begin processing a queue of commands in QUEUEITEMS.
+  "Begin processing a queue of commands.
 If START is non-nil, START and END are buffer positions in the
 active scripting buffer for the queue region.
 
-This function calls `proof-add-to-queue'."
+This function calls ‘proof-add-to-queue’ with args QUEUEITEMS and QUEUEMODE."
   (if start
       (proof-set-queue-endpoints start end))
   (proof-add-to-queue queueitems queuemode))
@@ -1173,7 +1172,7 @@ contains only invisible elements for Prooftree synchronization."
 	    (proof-shell-insert-action-item (car proof-action-list)))
 
 	;; process the delayed callbacks now
-	(mapc 'proof-shell-invoke-callback cbitems)	
+	(mapc 'proof-shell-invoke-callback cbitems)
 
 	(unless (or proof-action-list proof-second-action-list-active)
 					; release lock, cleanup
@@ -1218,8 +1217,8 @@ and indentation.  Assumes `proof-script-buffer' is active."
 (defun proof-shell-process-urgent-message (start end)
   "Analyse urgent message between START and END for various cases.
 
-Cases are: *trace* output, included/retracted files, cleared 
-goals/response buffer, variable setting, xml-encoded PGIP response, 
+Cases are: *trace* output, included/retracted files, cleared
+goals/response buffer, variable setting, xml-encoded PGIP response,
 theorem dependency message or interactive output indicator.
 
 If none of these apply, display the text between START and END.
@@ -1301,11 +1300,10 @@ A subroutine of `proof-shell-process-urgent-message'."
 
 (defun proof-shell-process-urgent-message-retract (start end)
   "A subroutine of `proof-shell-process-urgent-message'.
-Takes files off `proof-included-files-list' and calls
-`proof-restart-buffers' to do the necessary clean-up on those
-buffers visting a file that disappears from
-`proof-included-files-list'. So in some respect this function is
-inverse to `proof-register-possibly-new-processed-file'."
+Take files off `proof-included-files-list' and call `proof-restart-buffers'
+to do the necessary clean-up on those buffers visiting a file that disappears
+from `proof-included-files-list'.  So in some respect, this function is inverse
+to `proof-register-possibly-new-processed-file'."
   (let ((current-included proof-included-files-list))
     (setq proof-included-files-list
 	  (funcall proof-shell-compute-new-files-list))
@@ -1363,7 +1361,7 @@ inverse to `proof-register-possibly-new-processed-file'."
 ;;
 
 (defun proof-shell-strip-eager-annotations (start end)
-  "Strip `proof-shell-eager-annotation-{start,end}' from region."
+  "Strip `proof-shell-eager-annotation-{START,END}' from region."
   (goto-char start)
   (if (re-search-forward proof-shell-eager-annotation-start end nil)
       (setq start (point)))
@@ -1407,20 +1405,20 @@ calls."
 	   (setq proof-shell-filter-active nil
 		 proof-shell-filter-was-blocked nil)
 	   (signal (car err) (cdr err))))
-	(setq call-proof-shell-filter proof-shell-filter-was-blocked)))))  
+	(setq call-proof-shell-filter proof-shell-filter-was-blocked)))))
 
 
 (defun proof-shell-filter ()
   "Master filter for the proof assistant shell-process.
 A function for `scomint-output-filter-functions'.
 
-Deal with output and issue new input from the queue. This is an
-important internal function. The output must be collected from
-`proof-shell-buffer' for the following reason. This function
+Deal with output and issue new input from the queue.  This is an
+important internal function.  The output must be collected from
+`proof-shell-buffer' for the following reason.  This function
 might block inside `process-send-string' when sending input to
-the proof assistant or to prooftree. In this case Emacs might
+the proof assistant or to prooftree.  In this case Emacs might
 call the process filter again while the previous instance is
-still running. `proof-shell-filter-wrapper' detects and delays
+still running.  `proof-shell-filter-wrapper' detects and delays
 such calls but does not buffer the output.
 
 Handle urgent messages first.  As many as possible are processed,
@@ -1702,7 +1700,7 @@ i.e., 'goals or 'response."
        (setq both
 	     (> (- gmark rstart) 4))
        (if both
-	   (proof-shell-display-output-as-response 
+	   (proof-shell-display-output-as-response
 	    flags
 	    (buffer-substring-no-properties rstart gmark)))
        ;; display goals output second so it persists in 2-pane mode
@@ -1763,10 +1761,10 @@ Only works when system timer has microsecond count available."
 	    (> (- tm pg-last-tracing-output-time) pg-slow-mode-duration)
 	  (setq dontprint nil))
       (when ;; time since last tracing output less than threshold
-	  (and 
-	   (< (- tm pg-last-tracing-output-time) 
+	  (and
+	   (< (- tm pg-last-tracing-output-time)
 	      (/ pg-fast-tracing-mode-threshold 1000000.0))
-	   (>= (incf pg-last-trace-output-count) 
+	   (>= (incf pg-last-trace-output-count)
 	       pg-slow-mode-trigger-count))
 	;; quickly consecutive tracing outputs: go into slow mode
 	(setq dontprint t)
@@ -1779,7 +1777,7 @@ Only works when system timer has microsecond count available."
   "Handle the end of possibly voluminous tracing-style output.
 If the output update was slowed down, show it now."
   (proof-trace-buffer-finish)
-  (when pg-tracing-slow-mode 
+  (when pg-tracing-slow-mode
     (proof-display-and-keep-buffer proof-trace-buffer)
     (setq pg-tracing-slow-mode nil))
   (setq pg-last-trace-output-count 0))
@@ -1800,7 +1798,7 @@ If the output update was slowed down, show it now."
 
 Needed between sequences of commands to maintain synchronization,
 because Proof General does not allow for the action list to be extended
-in some cases.   Also is considerably faster than leaving the Emacs 
+in some cases.   Also is considerably faster than leaving the Emacs
 top-level command loop to read from the prover.
 
 Called by `proof-shell-invisible-command' and `proof-process-buffer'
@@ -1815,7 +1813,7 @@ If TIMEOUTSECS is a number, time out after that many seconds."
 			  (/ timeoutsecs accepttime))))
     (when proverproc
       (while (and proof-shell-busy (not quit-flag)
-		  (if timecount 
+		  (if timecount
 		      (> (setq timecount (1- timecount)) 0)
 		    t)
 		  (not (and interrupt-on-input (input-pending-p))))
@@ -1826,8 +1824,8 @@ If TIMEOUTSECS is a number, time out after that many seconds."
 	  (error "Proof General: quit in proof-shell-wait")))))
 
 (defun proof-done-invisible (span)
-  "Callback for proof-shell-invisible-command.
-Calls proof-state-change-hook."
+  "Callback for ‘proof-shell-invisible-command’.
+Call ‘proof-state-change-hook’."
   (run-hooks 'proof-state-change-hook))
 
 ;;;###autoload
@@ -2021,7 +2019,7 @@ processing."
 		    (if (listp proof-shell-init-cmd)
 			(mapc 'proof-shell-invisible-command-invisible-result
 				proof-shell-init-cmd)
-		      (proof-shell-invisible-command-invisible-result 
+		      (proof-shell-invisible-command-invisible-result
 		       proof-shell-init-cmd)))
 		  (proof-shell-wait)
 		  (if proof-assistant-settings
diff --git a/generic/proof-site.el b/generic/proof-site.el
index 9900aa5c..e339d022 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -156,7 +156,7 @@ You can use customize to set this variable."
 ;;
 
 (defun proof-add-to-load-path (dir)
-  "Add DIR to `load-path' if not contained already"
+  "Add DIR to `load-path' if not contained already."
   (add-to-list 'load-path dir))
 
 (proof-add-to-load-path (concat proof-home-directory "generic/"))
@@ -206,10 +206,10 @@ Each entry is a list of the form
 The NAME is a string, naming the proof assistant.
 The SYMBOL is used to form the name of the mode for the
 assistant, `SYMBOL-mode', run when files with AUTOMODE-REGEXP
-\(or with extension FILE-EXTENSION) are visited. If present,
+\(or with extension FILE-EXTENSION) are visited.  If present,
 IGNORED-EXTENSIONS-LIST is a list of file-name extensions to be
 ignored when doing file-name completion (IGNORED-EXTENSIONS-LIST
-is added to completion-ignored-extensions).
+is added to ‘completion-ignored-extensions’).
 
 SYMBOL is also used to form the name of the directory and elisp
 file for the mode, which will be
@@ -309,7 +309,7 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'."
       (mapcar (lambda (astnt) (car astnt)) proof-assistant-table))
   "A list of the configured proof assistants.
 Set on startup to contents of environment variable PROOFGENERAL_ASSISTANTS,
-the lisp variable `proof-assistants', or the contents of `proof-assistant-table'.")
+the Lisp variable `proof-assistants', or the contents of `proof-assistant-table'.")
 
 ;; Add auto-loads and load-path elements to support the
 ;; proof assistants selected, and define stub major mode functions
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index daa09eff..75164890 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -104,7 +104,7 @@ If it is nil, a new line is inserted."
   "Name of the Proof General splash buffer.")
 
 (define-derived-mode proof-splash-mode fundamental-mode
-  "Splash" "Mode for splash.  
+  "Splash" "Mode for splash.
 \\{proof-splash-mode-map}"
   (set-buffer-modified-p nil)
   (setq buffer-read-only t))
@@ -138,12 +138,12 @@ Borrowed from startup-center-spaces."
 	 (glyph-pixwidth   (cond ((stringp glyph)
 				  (* avg-pixwidth (length glyph)))
 				 ((proof-emacs-imagep glyph)
-				  (car (with-no-warnings 
+				  (car (with-no-warnings
 					; image-size not available in tty emacs
 					 (image-size glyph 'inpixels))))
 				 (t
 				  (error
-				   "proof-splash-centre-spaces: bad arg")))))
+				   "Function proof-splash-centre-spaces: bad arg")))))
     (+ left-margin
        (round (/ (/ (- fill-area-width glyph-pixwidth) 2) avg-pixwidth)))))
 
@@ -151,7 +151,7 @@ Borrowed from startup-center-spaces."
 ;; underneath the splash screen.  This is just to be polite.
 ;; NB: not as polite as it could be: if minibuffer is active,
 ;; this may deactivate it.
-;; NB2: There is something worse here: pending input 
+;; NB2: There is something worse here: pending input
 ;; causes this function to spoil the mode startup, if the splash
 ;; buffer is killed before the input has been processed.
 ;; Symptom is ProofGeneral mode instead of the native script mode.
@@ -161,7 +161,7 @@ Borrowed from startup-center-spaces."
   "Remove splash screen and restore window config."
   (let ((splashbuf (get-buffer proof-splash-welcome)))
     (proof-splash-unset-frame-titles)
-    (if (and 
+    (if (and
 	 splashbuf
 	 proof-splash-timeout-conf)
 	(progn
@@ -178,10 +178,10 @@ Borrowed from startup-center-spaces."
   "Remove the splash buffer if it's still present."
   (let
       ((splashbuf (get-buffer proof-splash-welcome)))
-    (if splashbuf 
+    (if splashbuf
 	;; Kill should be right, but it can cause core dump
 	;; on XEmacs (kill-buffer splashbuf) (TODO: check Emacs now)
-	(if (eq (selected-window) (window-buffer 
+	(if (eq (selected-window) (window-buffer
 				   (selected-window)))
 	    (bury-buffer splashbuf)))))
 
@@ -208,7 +208,7 @@ Borrowed from startup-center-spaces."
        (let ((spec (car splash-contents)))
 	 (if (functionp spec)
 	     (setq spec (funcall spec)))
-	 (indent-to (proof-splash-centre-spaces 
+	 (indent-to (proof-splash-centre-spaces
 		     (concat (car spec) (cadr spec))))
 	 (insert (car spec))
 	 (insert-button (cadr spec)
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 7af4dd06..5871a993 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -64,56 +64,56 @@ nil if a region cannot be found."
 ;; applicable.
 
 (defsubst proof-search-forward (string &optional bound noerror count)
-  "Like search-forward, but set case-fold-search to proof-case-fold-search."
+  "Like ‘search-forward’, but set ‘case-fold-search’ to ‘proof-case-fold-search’."
   (let
       ((case-fold-search proof-case-fold-search))
     (search-forward string bound noerror count)))
 
 ;;;###autoload
 (defsubst proof-replace-regexp-in-string (regexp rep string)
-  "Like replace-regexp-in-string, but set case-fold-search to proof-case-fold-search."
+  "Like ‘replace-regexp-in-string’, but set ‘case-fold-search’ to ‘proof-case-fold-search’."
   (let ((case-fold-search proof-case-fold-search))
     (replace-regexp-in-string regexp rep string)))
 
 (defsubst proof-re-search-forward (regexp &optional bound noerror count)
-  "Like re-search-forward, but set case-fold-search to proof-case-fold-search."
+  "Like ‘re-search-forward’, but set ‘case-fold-search’ to ‘proof-case-fold-search’."
   (let ((case-fold-search proof-case-fold-search))
     (re-search-forward regexp bound noerror count)))
 
 (defsubst proof-re-search-backward (regexp &optional bound noerror count)
-  "Like re-search-backward, but set case-fold-search to proof-case-fold-search."
+  "Like ‘re-search-backward’, but set ‘case-fold-search’ to ‘proof-case-fold-search’."
   (let ((case-fold-search proof-case-fold-search))
     (re-search-backward regexp bound noerror count)))
 
 (defsubst proof-re-search-forward-safe (regexp &optional bound noerror count)
-  "Like re-search-forward, but set case-fold-search to proof-case-fold-search."
+  "Like ‘re-search-forward’, but set ‘case-fold-search’ to ‘proof-case-fold-search’."
   (and regexp
        (let ((case-fold-search proof-case-fold-search))
 	 (re-search-forward regexp bound noerror count))))
 
 (defsubst proof-string-match (regexp string &optional start)
-  "Like string-match, but set case-fold-search to proof-case-fold-search."
+  "Like ‘string-match’, but set ‘case-fold-search’ to ‘proof-case-fold-search’."
   (let ((case-fold-search proof-case-fold-search))
     (string-match regexp string start)))
 
 (defsubst proof-string-match-safe (regexp string &optional start)
-  "Like `string-match', but return nil if REGEXP or STRING is nil."
+  "Like ‘string-match’, but return nil if REGEXP or STRING is nil."
   (if (and regexp string) (proof-string-match regexp string start)))
 
 (defsubst proof-stringfn-match (regexp-or-fn string)
-  "Like proof-string-match if first arg is regexp, otherwise call it."
+  "Like ‘proof-string-match’ if first arg is regexp, otherwise call it."
   (cond ((stringp regexp-or-fn)
 	 (proof-string-match regexp-or-fn string))
 	((functionp regexp-or-fn)
 	 (funcall regexp-or-fn string))))
 
 (defsubst proof-looking-at (regexp)
-  "Like looking-at, but set case-fold-search to proof-case-fold-search."
+  "Like ‘looking-at’, but set ‘case-fold-search’ to ‘proof-case-fold-search’."
   (let ((case-fold-search proof-case-fold-search))
     (looking-at regexp)))
 
 (defsubst proof-looking-at-safe (regexp)
-  "Like `proof-looking-at', but return nil if REGEXP is nil."
+  "Like ‘proof-looking-at’, but return nil if REGEXP is nil."
   (if regexp (proof-looking-at regexp)))
 
 ;;
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
index 996934b6..cb85952d 100644
--- a/generic/proof-tree.el
+++ b/generic/proof-tree.el
@@ -1,4 +1,4 @@
-;;; tree-tree.el --- Proof General prooftree communication.
+;;; proof-tree.el --- Proof General prooftree communication.
 
 ;; This file is part of Proof General.
 
@@ -15,7 +15,7 @@
 
 ;;; Commentary:
 ;;
-;; Generic code for the communication with prooftree. Prooftree
+;; Generic code for the communication with prooftree.  Prooftree
 ;; is an ocaml-gtk program that displays proof trees.
 ;;
 ;; The main problem with proof tree visualization is that Coq (and
@@ -26,20 +26,20 @@
 ;;
 ;; To solve this problem prooftree relies on unique identification
 ;; strings of goals, which are called goal or sequent ID's in the
-;; code. With these ID's it is easy to keep track which goals are new.
+;; code.  With these ID's it is easy to keep track which goals are new.
 ;;
 ;; A second problem is that, for an undo command, Coq (and probably
 ;; other proof assistants as well) does not tell which subgoals and
-;; which finished branches must be deleted. Therefore prooftree needs
+;; which finished branches must be deleted.  Therefore prooftree needs
 ;; a continuously increasing proof state number and keeps a complete
 ;; undo history for every proof.
 ;;
 ;; A third problem is that Coq (and probably other proof assistants as
 ;; well) is not able to generate the information for a proof tree in
-;; the middle of a proof. Therefore, if the user wants to start the
+;; the middle of a proof.  Therefore, if the user wants to start the
 ;; proof-tree display in the middle of the proof, it is necessary to
 ;; retract to the start of the proof and then to reassert to the
-;; previous end of the locked region. To achieve this, one has to call
+;; previous end of the locked region.  To achieve this, one has to call
 ;; `accept-process-output' at suitable points to let Proof General
 ;; process the `proof-action-list'.
 ;; 
@@ -56,36 +56,36 @@
 ;;
 ;;   * To avoid synchronization trouble the communication between
 ;;     Proof General and prooftree is almost one way only: Only Proof
-;;     General sends display or undo commands to Prooftree. Prooftree
+;;     General sends display or undo commands to Prooftree.  Prooftree
 ;;     never requests any proof-state information from Proof General.
 ;;     Prooftree only sends a quit message to Proof General when the
-;;     user closes the proof-tree display of the current proof. This
+;;     user closes the proof-tree display of the current proof.  This
 ;;     goal requires that some of the heuristics, which decide which
 ;;     subgoals are new and which have to be refreshed, have to be
 ;;     implemented here.
 ;;
-;; In general the glue code here works on the delayed output. That is,
+;; In general the glue code here works on the delayed output.  That is,
 ;; the glue code here runs when the next proof command has already
-;; been sent to the proof assistant. The glue code makes a light
+;; been sent to the proof assistant.  The glue code makes a light
 ;; analysis on the output of the proof assistant, extracts the
 ;; necessary parts with regular expressions and sends appropriate
-;; commands to prooftree. This is achieved by calling the main entry
+;; commands to prooftree.  This is achieved by calling the main entry
 ;; here, the function `proof-tree-handle-delayed-output' from the
 ;; proof shell filter function after `proof-shell-exec-loop' has
 ;; finished.
 ;;
-;; However, some aspects can not be delayed. Those are treated by
-;; `proof-tree-urgent-action'. Its primary use is for inserting
+;; However, some aspects can not be delayed.  Those are treated by
+;; `proof-tree-urgent-action'.  Its primary use is for inserting
 ;; special goal-displaying commands into `proof-action-list' before
-;; the next real proof command runs. For Coq this needs to be done for
+;; the next real proof command runs.  For Coq this needs to be done for
 ;; newly generated subgoals and for goals that contain an existential
 ;; variable that got instantiated in the last proof step.
 ;;
 ;; Actually, for every proof, Prooftree can display a set of disjunct
-;; proof trees, which are organized into layers. More than one proof
+;; proof trees, which are organized into layers.  More than one proof
 ;; tree in more than one layer is needed to support the Grap
-;; Existential Variables command in Coq. There is one proof tree in
-;; the first layer for the original goal. The second layer contains
+;; Existential Variables command in Coq.  There is one proof tree in
+;; the first layer for the original goal.  The second layer contains
 ;; all the goals that the first Grab Existential Variables command
 ;; created from uninstantiated existential variabes in the main proof.
 ;; The third layer contains the goals that the second Grap Existential
@@ -134,8 +134,8 @@
 (defcustom proof-tree-ignored-commands-regexp nil
   "Commands that should be ignored for the prooftree display.
 The output of commands matching this regular expression is not
-sent to prooftree. It should match commands that display
-additional information but do not make any proof progress. Leave
+sent to prooftree.  It should match commands that display
+additional information but do not make any proof progress.  Leave
 at nil to act on all commands.
 
 For Coq this regular expression should contain all commands such
@@ -146,7 +146,7 @@ as Lemma, that can start a proof."
 (defcustom proof-tree-navigation-command-regexp nil
   "Regexp to match a navigation command.
 A navigation command typically focusses on a different open goal
-without changing any of the open goals. Leave at nil if there are
+without changing any of the open goals.  Leave at nil if there are
 no navigation commands."
   :type '(choice regexp (const nil))
   :group 'proof-tree-internals)
@@ -155,15 +155,15 @@ no navigation commands."
   "Regexp to match cheating proofer commands.
 A cheating command finishes the current goal without proving it
 to permit the user to first focus on other parts of the
-development. Examples are \"sorry\" in Isabelle and \"admit\" in
-Coq. Leave at nil if there are no cheating commands."
+development.  Examples are \"sorry\" in Isabelle and \"admit\" in
+Coq.  Leave at nil if there are no cheating commands."
   :type '(choice regexp (const nil))
   :group 'proof-tree-internals)
 
 (defcustom proof-tree-new-layer-command-regexp nil
   "Regexp to match proof commands that add new goals to a proof.
 This regexp must match the command that turns the proof assistant
-into prover mode, which adds the initial goal to the proof. It
+into prover mode, which adds the initial goal to the proof.  It
 must further match commands that add additional goals after all
 previous goals have been proved."
   :type 'regexp
@@ -172,7 +172,7 @@ previous goals have been proved."
 (defcustom proof-tree-current-goal-regexp nil
   "Regexp to match the current goal and its ID.
 The regexp is matched against the output of the proof assistant
-to extract the current goal with its ID. The regexp must have 2
+to extract the current goal with its ID.  The regexp must have 2
 grouping constructs, the first one matches just the ID, the
 second one the complete sequent text that is to be sent to
 prooftree."
@@ -183,9 +183,9 @@ prooftree."
   "Regexp to match a goal and its ID.
 The regexp is matched against the output of additional show-goal
 commands inserted by Proof General with a command returned by
-`proof-tree-show-sequent-command'. Proof General inserts such
-commands to update the goal text in prooftree. This is necessary,
-for instance, when existential variables get instantiated. This
+`proof-tree-show-sequent-command'.  Proof General inserts such
+commands to update the goal text in prooftree.  This is necessary,
+for instance, when existential variables get instantiated.  This
 regexp must have 2 grouping constructs, the first matching the ID
 of the goal, the second the complete sequent text."
   :type 'regexp
@@ -194,7 +194,7 @@ of the goal, the second the complete sequent text."
 (defcustom proof-tree-additional-subgoal-ID-regexp nil
   "Regular expression to match ID's of additional subgoals.
 This regexp is used to extract the ID's of all additionally open
-goals. The regexp is used in a while loop and must match one
+goals.  The regexp is used in a while loop and must match one
 subgoal ID with subgroup 1."
   :type 'regexp
   :group 'proof-tree-internals)
@@ -202,8 +202,8 @@ subgoal ID with subgroup 1."
 (defcustom proof-tree-existential-regexp nil
   "Regexp to match existential variables.
 Existential variables exist for instance in Isabelle/Hol and in
-Coq. They are placeholders for terms that might (for Coq they
-must) get instantiated in a later stage of the proof. This regexp
+Coq.  They are placeholders for terms that might (for Coq they
+must) get instantiated in a later stage of the proof.  This regexp
 should match one existential variable in subgroup 1. It is used
 inside a while loop to extract all existential variables from the
 goal text or from a list of existential variables.
@@ -219,7 +219,7 @@ Together with `proof-tree-existentials-state-end-regexp', this
 regular expression is used to determine the state display of
 existential variables, which contains information about which
 existentials are still uninstantiated and about dependencies of
-instantiated existential variables. Leave this variable nil, if
+instantiated existential variables.  Leave this variable nil, if
 there is no such state display."
   :type '(choice regexp (const nil))
   :group 'proof-tree-internals)
@@ -230,7 +230,7 @@ Together with `proof-tree-existentials-state-start-regexp', this
 regular expression is used to determine the state display of
 existential variables, which contains information about which
 existentials are still uninstantiated and about dependencies of
-instantiated existential variables. If this variable is nil (and
+instantiated existential variables.  If this variable is nil (and
 if `proof-tree-existentials-state-start-regexp' is non-nil), then
 the state display expands to the end of the prover output."
   :type '(choice regexp (const nil))
@@ -242,29 +242,29 @@ This must match in precisely the following cases:
 - The current branch has been finished but there is no current
   open subgoal because the prover has not switched to the next
   subgoal.
-- The last open goal has been proved. "
+- The last open goal has been proved."
   :type 'regexp
   :group 'proof-tree-internals)
 
 (defcustom proof-tree-get-proof-info nil
   "Proof assistant specific function for information about the current proof.
-This function takes no arguments. It must return a list, which
+This function takes no arguments.  It must return a list, which
 contains, in the following order:
 
 * the current state number (as positive integer)
 * the name of the current proof (as string) or nil
 
-The state number is used to implement undo in prooftree. The
+The state number is used to implement undo in prooftree.  The
 proof name is used to distinguish different proofs inside
 prooftree.
 
 The state number is interpreted as the state that has been
-reached after the last command has been processed. It must be
-consistent in the following sense. Firstly, it must be strictly
+reached after the last command has been processed.  It must be
+consistent in the following sense.  Firstly, it must be strictly
 increasing for successive commands that can be individually
-retracted. Secondly, the state number reported after some command
+retracted.  Secondly, the state number reported after some command
 X has been processed must be strictly greater than the state
-reported when X is retracted. Finally, state numbers of commands
+reported when X is retracted.  Finally, state numbers of commands
 preceding X must be less than or equal the state reported when X
 is retracted (but no stuff before X)."
   :type 'function
@@ -277,7 +277,7 @@ variables, that is, if `proof-tree-existential-regexp' is
 non-nil.
 
 If defined, this function should return the list of currently
-instantiated existential variables as a list of strings. The
+instantiated existential variables as a list of strings.  The
 function is called with `proof-shell-buffer' as current
 buffer and with two arguments start and stop, which designate the
 region containing the last output from the proof assistant.
@@ -291,7 +291,7 @@ function."
   "Proof assistant specific function for a show-goal command.
 This function is applied to an ID of a goal and should return a
 command (as string) that will display the complete sequent with
-that ID. The regexp `proof-tree-update-goal-regexp' should match
+that ID.  The regexp `proof-tree-update-goal-regexp' should match
 the output of the proof assistant for the returned command, such
 that `proof-tree-update-sequent' will update the sequent ID
 inside prooftree.
@@ -304,11 +304,11 @@ function should return nil and prooftree will not get updated."
 (defcustom proof-tree-find-begin-of-unfinished-proof nil
   "Proof assistant specific function for the start of the current proof.
 This function is called with no argument when the user switches
-the external proof-tree display on. Then, this function must
+the external proof-tree display on.  Then, this function must
 determine if there is a currently unfinished proof for which the
-proof-tree display should be started. If yes this function must
+proof-tree display should be started.  If yes this function must
 return the starting position of the command that started this
-proof. If there is no such proof, this function must return nil."
+proof.  If there is no such proof, this function must return nil."
   :type 'function
   :group 'proof-tree-internals)
 
@@ -316,8 +316,8 @@ proof. If there is no such proof, this function must return nil."
   "Proof assistant specific function for finding the point to undo to.
 This function is used to convert the state number, which comes
 with an undo command from Prooftree, into a point position for
-`proof-retract-until-point'. This function is called in the
-current scripting buffer with the state number as argument. It
+`proof-retract-until-point'.  This function is called in the
+current scripting buffer with the state number as argument.  It
 must return a buffer position."
   :type 'function
   :group 'proof-tree-internals)
@@ -327,7 +327,7 @@ must return a buffer position."
 This hook is called (indirectly) from inside
 `proof-shell-exec-loop' after the preceeding command and any
 comments that follow have been choped off `proof-action-list' and
-before the next command is sent to the proof assistant. This hook
+before the next command is sent to the proof assistant.  This hook
 can therefore be used to insert additional commands into
 `proof-action-list' that must be executed before the next real
 proof command.
@@ -336,7 +336,7 @@ Functions in this hook can rely on `proof-info' being bound to
 the result of `proof-tree-get-proof-info'.
 
 This hook is used, for instance, for Coq to insert Show commands
-for newly generated subgoals. (The normal Coq output does not
+for newly generated subgoals.  (The normal Coq output does not
 contain the complete sequent text of newly generated subgoals.)"
   :type 'hook
   :group 'proof-tree-internals)
@@ -349,19 +349,19 @@ contain the complete sequent text of newly generated subgoals.)"
 (defvar proof-tree-external-display nil
   "Display proof trees in external prooftree windows if t.
 Actually, if this variable is t then the user requested an
-external proof-tree display. If there was no unfinished proof
+external proof-tree display.  If there was no unfinished proof
 when proof-tree display was requested and if no proof has been
 started since then, then there is obviously no proof-tree
-display. In this case, this variable stays t and the proof-tree
+display.  In this case, this variable stays t and the proof-tree
 display will be started for the next proof.
 
 Controlled by `proof-tree-external-display-toggle'.")
 
 (defvar proof-tree-process nil
-  "Emacs lisp process object of the prooftree process.")
+  "Emacs Lisp process object of the prooftree process.")
 
 (defconst proof-tree-process-name "proof-tree"
-  "Name of the prooftree process for Emacs lisp.")
+  "Name of the prooftree process for Emacs Lisp.")
 
 (defconst proof-tree-process-buffer-name
   (concat "*" proof-tree-process-name "*")
@@ -387,13 +387,13 @@ This variable is only maintained and meaningful if
   "Hash table to remember sequent ID's.
 Needed because some proof assistants do not distinguish between
 new subgoals, which have been created by the last proof command,
-and older, currently unfocussed subgoals. If Proof General meets
+and older, currently unfocussed subgoals.  If Proof General meets
 a goal, it is treated as new subgoal if it is not in this hash yet.
 
-The hash is mostly used as a set of sequent ID's. However, for
+The hash is mostly used as a set of sequent ID's.  However, for
 undo operations it is necessary to delete all those sequents from
 the hash that have been created in a state later than the undo
-state. For this purpose this hash maps sequent ID's to the state
+state.  For this purpose this hash maps sequent ID's to the state
 number in which the sequent has been created.
 
 The hash table is initialized in `proof-tree-start-process'.")
@@ -401,9 +401,9 @@ The hash table is initialized in `proof-tree-start-process'.")
 (defvar proof-tree-existentials-alist nil
   "Alist mapping existential variables to sequent ID's.
 Used to remember which goals need a refresh when an existential
-variable gets instantiated. To support undo commands the old
+variable gets instantiated.  To support undo commands the old
 contents of this list must be stored in
-`proof-tree-existentials-alist-history'. To ensure undo is
+`proof-tree-existentials-alist-history'.  To ensure undo is
 properly working, this variable should only be changed by using
 `proof-tree-delete-existential-assoc',
 `proof-tree-add-existential-assoc' or
@@ -425,7 +425,7 @@ This marker points to the next piece of output that needs to get processed.")
 (defvar proof-tree-filter-continuation nil
   "Continuation when `proof-tree-process-filter' stops early.
 A function that handles a command from Prooftee might fail
-because not all data from Prooftee has yet arrived. In this case
+because not all data from Prooftee has yet arrived.  In this case
 the continuation is stored in this variable and will be called
 from `proof-tree-process-filter' when more output arrives.")
 
@@ -450,7 +450,7 @@ from `proof-tree-process-filter' when more output arrives.")
 
 (defun proof-tree-insert-script (data)
   "Handle an insert-command command from Prooftree."
-  (let ((command-length (string-to-number data))) 
+  (let ((command-length (string-to-number data)))
     (if (and (integerp command-length) (> command-length 0))
 	(condition-case nil
 	    (progn
@@ -768,13 +768,13 @@ state PROOF-STATE."
 			     'proof-tree-existentials-alist-history))
 
 (defun proof-tree-delete-existential-assoc (state ex-assoc)
-  "Delete mapping EX-ASSOC from 'proof-tree-existentials-alist'."
+  "Delete mapping EX-ASSOC from ‘proof-tree-existentials-alist’."
   (proof-tree-record-existentials-state state)
   (setq proof-tree-existentials-alist
 	(delq ex-assoc proof-tree-existentials-alist)))
   
 (defun proof-tree-add-existential-assoc (state ex-var sequent-id)
-  "Add the mapping EX-VAR -> SEQUENT-ID to 'proof-tree-existentials-alist'.
+  "Add the mapping EX-VAR -> SEQUENT-ID to ‘proof-tree-existentials-alist’.
 Do nothing if this mapping does already exist."
   (let ((ex-var-assoc (assoc ex-var proof-tree-existentials-alist)))
     (if ex-var-assoc
@@ -830,7 +830,7 @@ the current output does not come from a command (with the
 
 Urgent actions are only needed if the external proof display is
 currently running. Therefore this function should not be called
-when `proof-tree-external-display' is nil. 
+when `proof-tree-external-display' is nil.
 
 This function assumes that the prover output is not suppressed.
 Therefore, `proof-tree-external-display' being t is actually a
@@ -1073,8 +1073,8 @@ Send the undo command to prooftree and undo changes to the
 internal state of this package. The latter involves currently two
 points:
 * delete those goals from `proof-tree-sequent-hash' that have
-  been generated after the state to which we undo now
-* change proof-tree-existentials-alist back to its previous content"
+  been generated after the state to which we undo now;
+* change proof-tree-existentials-alist back to its previous content."
   ;; (message "PTHU info %s" proof-info)
   (let ((proof-state (car proof-info)))
     ;; delete sequents from the hash
@@ -1103,11 +1103,11 @@ points:
   "Prepare an update-sequent command for prooftree.
 This function processes delayed output that the proof assistant
 generated in response to commands that Proof General inserted in
-order to keep prooftree up-to-date. Such commands are tagged with
+order to keep prooftree up-to-date.  Such commands are tagged with
 a 'proof-tree-show-subgoal flag.
 
 This function uses `proof-tree-update-goal-regexp' to find a
-sequent and its ID in the delayed output. If something is found
+sequent and its ID in the delayed output.  If something is found
 an appropriate update-sequent command is sent to prooftree.
 
 The update-sequent command is associated with state PROOF-STATE
@@ -1143,7 +1143,7 @@ The delayed output is in the region
 (defun proof-tree-handle-delayed-output (old-proof-marker cmd flags span)
   "Process delayed output for prooftree.
 This function is the main entry point of the Proof General
-prooftree support. It examines the delayed output in order to
+prooftree support.  It examines the delayed output in order to
 take appropriate actions and maintains the internal state.
 
 The delayed output to handle is in the region
@@ -1153,7 +1153,7 @@ which contains the position of `proof-marker', before the next
 command was sent to the proof assistant.
 
 All other arguments are (former) fields of the `proof-action-list'
-entry that is now finally retired. CMD is the command, FLAGS are
+entry that is now finally retired.  CMD is the command, FLAGS are
 the flags and SPAN is the span."
   ;; (message "PTHDO cmd %s flags %s span %s-%s" cmd flags
   ;; 	   (if span (span-start span)) (if span (span-end span)))
@@ -1215,10 +1215,10 @@ the flags and SPAN is the span."
 (defun proof-tree-display-current-proof (proof-start)
   "Start an external proof-tree display for the current proof.
 Coq (and probably other proof assistants as well) does not
-support outputing the current proof tree. Therefore this function
+support outputing the current proof tree.  Therefore this function
 retracts to the start of the current proof, switches the
 proof-tree display on, and reasserts then until the former end of
-the locked region. Argument PROOF-START must contain the start
+the locked region.  Argument PROOF-START must contain the start
 position of the current proof."
   ;;(message "PTDCP %s" proof-tree-external-display)
   (unless (and proof-script-buffer
@@ -1247,10 +1247,10 @@ position of the current proof."
 (defun proof-tree-external-display-toggle ()
   "Toggle the external proof-tree display.
 When called outside a proof the external proof-tree display will
-be enabled for the next proof. When called inside a proof the
-proof display will be created for the current proof. If the
+be enabled for the next proof.  When called inside a proof the
+proof display will be created for the current proof.  If the
 external proof-tree display is currently on, then this toggle
-will switch it off. At the end of the proof the proof-tree
+will switch it off.  At the end of the proof the proof-tree
 display is switched off."
   (interactive)
   (unless proof-tree-configured
@@ -1287,4 +1287,4 @@ display is switched off."
 
 (provide 'proof-tree)
 
-;;; tree-tree.el ends here
+;;; proof-tree.el ends here
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index b1d8e2e4..9a60e0ac 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -192,7 +192,7 @@ and displayed lazily.  See `proof-layout-windows'."
   and goal and response buffers on the left (one above the
   other).
 - If 'smart or anything else: 'horizontal when the window
-  is wide enough and 'vertical otherwise. The width threshold
+  is wide enough and 'vertical otherwise.  The width threshold
   is given by `split-width-threshold'.
 
   See `proof-layout-windows'."
@@ -362,8 +362,8 @@ locked (coloured blue); a buffer is completely unprocessed when there
 is no locked region.
 
 For some proof assistants (such as Coq) fully processed buffers make
-no sense. Setting this option to 'process has then the same effect
-as leaving it unset (nil). (This behaviour is controlled by
+no sense.  Setting this option to 'process has then the same effect
+as leaving it unset (nil).  (This behaviour is controlled by
 `proof-no-fully-processed-buffer'.)"
   :type '(choice
 	  (const :tag "No automatic action; query user" nil)
@@ -408,7 +408,7 @@ Hovers will be added when this option is non-nil.  Prover outputs
 can be displayed when the mouse hovers over the region that
 produced it and output is available (see `proof-full-annotation').
 If output is not available, the type of the output region is displayed.
-Changes of this option will not be reflected in already-processed 
+Changes of this option will not be reflected in already-processed
 regions of the script."
   :type 'boolean
   :group 'proof-user-options)
@@ -438,7 +438,7 @@ are distracting or too frequent."
   :type 'boolean
   :group 'proof-user-options)
 
-(defcustom proof-fast-process-buffer 
+(defcustom proof-fast-process-buffer
   (or (featurep 'ns) ; Mac OS X
       ; or Windows (speed up TBC, see Trac #308)
       (memq system-type '(windows-nt ms-dos cygwin)))
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 575a76ee..4a0ca857 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -66,7 +66,7 @@
 ;;
 
 (defmacro proof-with-current-buffer-if-exists (buf &rest body)
-  "As with-current-buffer if BUF exists and is live, otherwise nothing."
+  "Like ‘with-current-buffer’ if BUF exists and is live, otherwise nothing."
   `(if (buffer-live-p ,buf)
        (with-current-buffer ,buf
 	 ,@body)))
@@ -75,7 +75,7 @@
 ;; which work from different PG buffers (goals, response), typically
 ;; bound to toolbar commands.
 (defmacro proof-with-script-buffer (&rest body)
-  "Execute BODY in some script buffer: current buf or otherwise proof-script-buffer.
+  "Execute BODY in some script buffer: current buf, else ‘proof-script-buffer’.
 Return nil if not a script buffer or if no active scripting buffer."
   `(cond
     ((eq proof-buffer-type 'script)
@@ -86,7 +86,7 @@ Return nil if not a script buffer or if no active scripting buffer."
        ,@body))))
 
 (defmacro proof-map-buffers (buflist &rest body)
-  "Do BODY on each buffer in BUFLIST, if it exists."
+  "Eval BODY on each buffer in BUFLIST, if it exists."
   `(dolist (buf ,buflist)
      (proof-with-current-buffer-if-exists buf ,@body)))
 
@@ -187,9 +187,9 @@ user accidently killing an associated buffer."
 ;; Key functions
 
 (defun proof-define-keys (map kbl)
-  "Adds keybindings KBL in MAP.
-The argument KBL is a list of tuples (k . f) where `k' is a keybinding
-\(vector) and `f' the designated function."
+  "Add in MAP the keybindings KBL.
+The argument KBL is a list of tuples (K . F) where K is a keybinding
+\(vector) and F the designated function."
   (mapcar
    (lambda (kbl)
      (let ((k (car kbl)) (f (cdr kbl)))
@@ -230,21 +230,21 @@ Leave point at END."
 (defvar proof-advertise-layout-freq 30
   "Frequency for PG messages to be displayed from time to time.")
 (defvar proof-advertise-layout-count proof-advertise-layout-freq
-  "counter used to display PG messages from time to time.")
+  "Counter used to display PG messages from time to time.")
 
 (defun proof-get-window-for-buffer (buffer)
   "Find a window for BUFFER, display it there, return the window.
-NB: may change the selected window. This function is a wrapper on
-display-buffer. The idea is that if the user has opened and
+NB: may change the selected window.  This function is a wrapper on
+‘display-buffer’.  The idea is that if the user has opened and
 closed some windows we want to preserve the layout by only
-switching buffer in already pg-associate windows. So if the
+switching buffer in already pg-associate windows.  So if the
 buffer is not already displayed, we try to reuse an existing
-associated window, even if in 3-win mode. If no such window
-exists, we fall back to display-buffer while protecting script
+associated window, even if in 3-win mode.  If no such window
+exists, we fall back to ‘display-buffer’ while protecting script
 buffer to be hidden or split.
 
 Experimentally we display a message from time to time advertising
-C-c C-l."
+\\[proof-layout-windows]."
   ;; IF there *isn't* a visible window showing buffer...
   (unless (get-buffer-window buffer 0)
     (if proof-three-window-enable
@@ -323,7 +323,7 @@ Ensure that point is visible in window."
 		      (kill-local-variable 'mode-line-format))))))))))))
 
 (defun proof-clean-buffer (buffer)
-  "Erase buffer and hide from display if proof-delete-empty-windows set.
+  "Erase BUFFER and hide from display if ‘proof-delete-empty-windows’ set.
 Auto deletion only affects selected frame.  (We assume that the selected
 frame is the one showing the script buffer.)
 No effect if buffer is dead."
@@ -699,9 +699,10 @@ KEY is added onto proof assistant map."
 ;;
 
 (defun proof-locate-executable (progname &optional returnnopath extrapath)
-  "Search for PROGNAME on environment PATH.  Return the full path to PROGNAME, or nil.
+  "Search for PROGNAME on environment PATH.
+Return the full path to PROGNAME, or nil.
 If RETURNNOPATH is non-nil, return PROGNAME even if we can't find a full path.
-EXTRAPATH is a list of extra path components"
+EXTRAPATH is a list of extra path components."
   (or
    (let ((exec-path (append exec-path extrapath)))
      (executable-find progname))