Docstring fixes, minor improvements.

3 files changed, 21 insertions, 9 deletions

diff --git a/generic/proof-indent.el b/generic/proof-indent.el
index 4cf14084..1caeaadb 100644
--- a/generic/proof-indent.el
+++ b/generic/proof-indent.el
@@ -45,6 +45,7 @@
 	 (t (cond
 	     ((eq c ?\()
 	      (cond
+	       ;; FIXME broken: comment strings are not generic.
 	       ((looking-at "(\\*")
 		(progn
 		  (incf comment-level)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index ede3f76d..437f3e55 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -60,7 +60,12 @@ Set in proof-shell-mode.")
 (defvar proof-marker nil 
   "Marker in proof shell buffer pointing to previous command input.")
 
-(defvar proof-action-list nil "action list")
+(defvar proof-action-list nil
+  "A list of
+
+  (span,command,action)
+
+triples, which is a queue of things to do.")
 
 
 
@@ -132,7 +137,7 @@ Set in proof-shell-mode.")
 
 (defun proof-shell-ready-prover ()
   "Make sure the proof assistant is ready for a command"
-  (proof-start-shell)
+  (proof-shell-start)
   (if proof-shell-busy (error "Proof Process Busy!")))
 
 (defun proof-shell-live-buffer ()
@@ -174,11 +179,12 @@ No error messages.  Useful as menu or toolbar enabler."
 ;;  Starting and stopping the proof shell  
 ;;
 
-(defun proof-start-shell ()
+(defun proof-shell-start ()
   "Initialise a shell-like buffer for a proof assistant.
 
 Also generates goal and response buffers.
 Does nothing if proof assistant is already running."
+  (interactive)
   (if (proof-shell-live-buffer)
       ()
     (run-hooks 'proof-pre-shell-start-hook)
@@ -353,10 +359,12 @@ and clearing all script buffers."
       (incf a))
     (apply 'concat (nreverse ls))))
 
+;; FIXME da: this is an oddity.  Was bound by default to
+;; control - button1, I've turned it off.
 (defun proof-send-span (event)
   (interactive "e")
   (let* ((span (span-at (mouse-set-point event) 'type))
-	 (str (span-property span 'cmd)))
+	 (str  (if span (span-property span 'cmd))))
     (cond ((and (eq (current-buffer) proof-script-buffer)
 		(not (null span)))
 	   (proof-goto-end-of-locked)
@@ -1017,11 +1025,11 @@ if none of these apply, display."
 				   'proof-eager-annotation-face))))
 
 (defvar proof-shell-urgent-message-marker nil
-  "Marker in proof shell buffer used for parsing urgent messages.")
+  "Marker in proof shell buffer pointing to end of last urgent message.")
 
 (defun proof-shell-process-urgent-messages ()
   "Scan the shell buffer for urgent messages.
-Scanning starts from proof-shell-urgent-message-pos and processes
+Scanning starts from proof-shell-urgent-message-marker and processes
 strings between eager-annotation-start and eager-annotation-end."
   (let ((pt (point)))
     (goto-char
@@ -1051,9 +1059,10 @@ strings between eager-annotation-start and eager-annotation-end."
 ;; FIXME da: moreover, are urgent messages full processed??
 ;; some seem to get dumped in response buffer.
 
-(defun proof-shell-filter (str) 
+(defun proof-shell-filter (str)
   "Filter for the proof assistant shell-process.
-We sleep until we get a wakeup-char in the input, then run
+We process urgent messages first.  Then wait until we get a
+proof-shell-wakeup-char in the input, then run
 proof-shell-process-output, and set proof-marker to keep track of
 how far we've got."
   (save-excursion
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index 44c37a9e..4ce86a4f 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -1,6 +1,7 @@
 ;; proof-toolbar.el    Toolbar for Proof General
 ;;
-;; David Aspinall <da@dcs.ed.ac.uk>
+;; Copyright (C) 1998 David Aspinall.
+;; Author:     David Aspinall <da@dcs.ed.ac.uk>
 ;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk>
 ;;
 ;; $Id$
@@ -353,6 +354,7 @@ Move point if the end of the locked position is invisible."
   )
 
 (defun proof-toolbar-restart  ()
+  "Restart scripting via proof-shell-restart."
   (interactive)
   (if (proof-toolbar-restart-enable-p)
       (proof-shell-restart)))