Comments

3 files changed, 10 insertions, 15 deletions

diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index 6869bab9..e28ef1cd 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -389,10 +389,9 @@ user types by hand."
    (mouse-set-point event)
    (pg-goals-construct-command))
 
-;; Using the spans in a mouse behavior is quite simple: from the
-;; mouse position, find the relevant span, then get its annotation
-;; and produce a piece of text that will be inserted in the right
-;; buffer.  
+;; Using the spans in a mouse behavior is quite simple: from the mouse
+;; position, find the relevant span, then get its annotation and
+;; produce a piece of text that will be inserted in the right buffer.
 
 (defun proof-expand-path (string)
   (let ((a 0) (l (length string)) ls)
@@ -404,7 +403,8 @@ user types by hand."
     (apply 'concat (nreverse ls))))
 
 (defun pg-goals-construct-command ()
-  (let* ((span (span-at (point) 'goalsave))
+  ;; Examine the goals 
+  (let* ((span (span-at (point) 'goalsave)) ;; goalsave means subgoal no/name
 	 (top-span (span-at (point) 'proof-top-element))
 	 top-info)
     (if (null top-span) ()
@@ -418,6 +418,7 @@ user types by hand."
 		 (concat (cdr top-info) (proof-expand-path 
 					 (span-property span 'goalsave))))))
        ((eq (car top-info) 'hyp)
+	;; Switch focus to another subgoal; a non-scripting command
 	(proof-shell-invisible-command
 	 (format pbp-hyp-command (cdr top-info))))
        (t
diff --git a/generic/proof-config.el b/generic/proof-config.el
index f4664ec2..5b09ed1a 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -2146,14 +2146,12 @@ For LEGO 1.3.1 use `nil', for Coq 6.2, use `t'."
   :group 'proof-goals)
 
 (defcustom pbp-goal-command nil
-  "Command informing the prover that `pg-goals-button-action' has been
-requested on a goal."
+  "Command sent when `pg-goals-button-action' is requested on a goal."
   :type '(choice nil string)
   :group 'proof-goals)
 
 (defcustom pbp-hyp-command nil
-  "Command informing the prover that `pg-goals-button-action' has been
-requested on an assumption."
+  "Command sent when `pg-goals-button-action' is requested on an assumption."
   :type '(choice nil string)
   :group 'proof-goals)
 
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index e171da86..0a40433c 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -826,8 +826,7 @@ proof-shell-exec-loop, to process the next item."
     (unless (null (marker-position proof-marker))
       (set-marker proof-marker (point)))
 
-    ;; FIXME: possible improvement.  Make for post 3.0 releases
-    ;; in case of problems.
+    ;; FIXME: consider as possible improvement.
     ;; (set-marker proof-shell-urgent-message-marker (point))
     ;; (set-marker proof-shell-urgent-message-scanner (point))
 
@@ -1040,9 +1039,6 @@ The return value is non-nil if the action list is now empty."
 	    ;; indicate not finished
 	    nil)))))
 
-;; FIXME da: some places in the code need to be made robust in
-;; case of buffer kills, etc, before callbacks.  Is this function
-;; one?
 (defun proof-shell-insert-loopback-cmd  (cmd)
   "Insert command sequence triggered by the proof process
 at the end of locked region (after inserting a newline and indenting).
@@ -1054,7 +1050,7 @@ Assume proof-script-buffer is active."
 	(proof-goto-end-of-locked)
 	;; Fix 16.11.99.  This attempts to indent current line which can
 	;; be read-only.  
-      ;; (newline-and-indent)
+	;; (newline-and-indent)
 	(let ((proof-one-command-per-line t)) ; because pbp several commands
 	  (proof-script-new-command-advance))
 	(insert cmd)