made many minor changes to the documentation

6 files changed, 66 insertions, 30 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 31586553..befd32c0 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -103,7 +103,10 @@ use because of a bug."
 (defcustom proof-strict-read-only 
   ;; For FSF Emacs, strict read only is buggy when used in
   ;; conjunction with font-lock.
-  (string-match "XEmacs" emacs-version)
+
+  ;; The second conjunctive ensures that the expression is either
+  ;; `nil' or `strict' (and not 15).  
+  (and (string-match "XEmacs" emacs-version) 'strict)
   "*Whether Proof General is strict about the read-only region in buffers.
 If non-nil, an error is given when an attempt is made to edit the
 read-only region.  If nil, Proof General is more relaxed (but may give
@@ -335,6 +338,7 @@ Suggestion: this can be set in the shell mode configuration."
   :type 'function
   :group 'prover-config)
 
+;; FIXME: ought to be renamed to proof-mode-for-goals
 (defcustom proof-mode-for-pbp 'pbp-mode
   "Mode for proof state display buffers.
 Usually customised for specific prover.
@@ -412,7 +416,7 @@ insert when called interactively."
 
 
 (defcustom proof-terminal-char nil
-  "Character which terminates a proof command in a script buffer."
+  "Character which terminates a command in a script buffer."
   :type 'character
   :group 'proof-script)
 
@@ -423,7 +427,7 @@ The script buffer's comment-start is set to this string plus a space."
   :group 'proof-script)
 
 (defcustom proof-comment-end ""
-  "String which starts a comment in the proof assistant command language.
+  "String which ends a comment in the proof assistant command language.
 The script buffer's comment-end is set to this string plus a space."
   :type 'string
   :group 'proof-script)
@@ -572,7 +576,7 @@ The special string proof-no-command means there is nothing to do."
   "Function which returns cons cell if point is at a goal/hypothesis.
 First element of cell is a symbol, 'goal' or 'hyp'.  The second
 element is a string: the goal or hypothesis itself.  This is used
-when parsing the proofstate output"
+when parsing the proofstate output."
   :type 'function
   :group 'proof-script)
 
@@ -588,7 +592,7 @@ This is used to handle nested goals allowed by some provers."
   :group 'proof-script)
 
 (defcustom proof-state-preserving-p nil
-  "A predicate, non-nil if its argument preserves the proof state."
+  "A predicate, non-nil if its argument (a command) preserves the proof state."
   :type 'function
   :group 'proof-script)
 
@@ -689,7 +693,7 @@ group.  This allows different proof assistants to coexist
 ;;
 
 (defcustom proof-shell-prompt-pattern nil 
-   "Proof shell's value for comint-prompt-pattern, which see."
+   "Proof shell's value for comint-prompt-pattern."
    :type 'regexp
    :group 'proof-shell)
 
@@ -736,7 +740,7 @@ otherwise it will be lost."
 
 (defcustom proof-shell-interrupt-regexp nil
   "Regexp matching output indicating the assistant was interrupted.
-Similar notes apply as for proof-shell-error-regexp, which see."
+Similar notes apply as for `proof-shell-error-regexp'."
   :type 'regexp
   :group 'proof-shell) 
 
@@ -1026,7 +1030,7 @@ inserted."
 
 (defcustom proof-splash-extensions nil
   "Prover specific extensions of splash screen.
-These are evaluated and appended to proof-splash-contents, which see."
+These are evaluated and appended to `proof-splash-contents'."
   :type 'sexp
   :group 'proof-config)
   
@@ -1055,7 +1059,7 @@ These are evaluated and appended to proof-splash-contents, which see."
 (defcustom proof-universal-keys
   '(([(control c) (control c)] . proof-interrupt-process)
     ([(control c) (control v)] . proof-execute-minibuffer-cmd))
-"List of keybindings made for both the script and response buffer. 
+"List of keybindings made for the script, goals and response buffer. 
 Elements of the list are tuples `(k . f)' 
 where `k' is a keybinding (vector) and `f' the designated function."
   :type 'sexp
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 06c768ae..d9d5c686 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -873,6 +873,13 @@ Assumes that point is at the end of a command."
       (forward-line)))
 
 
+(defun proof-assert-until-point-interactive ()
+  "Process the region from the end of the locked-region until point.
+Default action if inside a comment is just process as far as the start of
+the comment."
+  (interactive)
+  (proof-assert-until-point))
+
 
 ; Assert until point - We actually use this to implement the 
 ; assert-until-point, active terminator keypress, and find-next-terminator. 
@@ -889,11 +896,12 @@ Assumes that point is at the end of a command."
   (&optional unclosed-comment-fun ignore-proof-process-p)
   "Process the region from the end of the locked-region until point.
 Default action if inside a comment is just process as far as the start of
-the comment. If you want something different, put it inside
+the comment. 
+
+If you want something different, put it inside
 UNCLOSED-COMMENT-FUN. If IGNORE-PROOF-PROCESS-P is set, no commands
 will be added to the queue and the buffer will not be activated for
 scripting."
-  (interactive)
   (unless ignore-proof-process-p 
     (proof-shell-ready-prover)
     (proof-activate-scripting))
@@ -930,17 +938,23 @@ scripting."
 ;; FIXME: polish the undo behaviour and quit behaviour of this
 ;; command (should inhibit quit somewhere or other).
 
+(defun proof-assert-next-command-interactive ()
+  "Process until the end of the next unprocessed command after point.
+If inside a comment, just process until the start of the comment."
+  (interactive)
+  (proof-assert-next-command))
+  
 (defun proof-assert-next-command
   (&optional unclosed-comment-fun ignore-proof-process-p
 	     dont-move-forward for-new-command)
   "Process until the end of the next unprocessed command after point.
 If inside a comment, just process until the start of the comment.  
+
 If you want something different, put it inside UNCLOSED-COMMENT-FUN. 
 If IGNORE-PROOF-PROCESS-P is set, no commands will be added to the queue.
 Afterwards, move forward to near the next command afterwards, unless
 DONT-MOVE-FORWARD is non-nil.  If FOR-NEW-COMMAND is non-nil,
 a space or newline will be inserted automatically."
-  (interactive)
   (unless ignore-proof-process-p
     (proof-shell-ready-prover)
     ;; FIXME: check this
@@ -1073,6 +1087,13 @@ deletes the region corresponding to the proof sequence."
 
 ;; FIXME da: Maybe retraction to the start of
 ;; a file should remove it from the list of included files?
+(defun proof-retract-until-point-interactive ()
+  "Tell the proof process to retract until point.
+If invoked outside a locked region, undo the last successfully processed
+command."
+  (interactive)
+  (proof-retract-until-point))
+
 (defun proof-retract-until-point (&optional delete-region)
   "Set up the proof process for retracting until point.
 In particular, set a flag for the filter process to call 
@@ -1082,7 +1103,6 @@ If DELETE-REGION is non-nil, delete the region in the proof script
 corresponding to the proof command sequence.
 If invoked outside a locked region, undo the last successfully processed
 command."
-  (interactive)
   (proof-shell-ready-prover)
   (proof-activate-scripting)
   (let ((span (span-at (point) 'type)))
@@ -1150,12 +1170,16 @@ UNCLOSED-COMMENT-FUN."
 ;;         misc other user functions                                ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
+(defun proof-undo-last-successful-command-interactive ()
+  "Undo last successful command at end of locked region.
+The text is also deleted from the proof script."
+  (interactive "p")
+  (proof-undo-last-successful-command))
 
 (defun proof-undo-last-successful-command (&optional no-delete)
   "Undo last successful command at end of locked region.
 Unless optional NO-DELETE is set, the text is also deleted from
 the proof script."
-  (interactive "p")
   (unless (proof-locked-region-empty-p)
     (let ((lastspan (span-at-before (proof-locked-end) 'type)))
       (if lastspan
@@ -1208,7 +1232,7 @@ the proof script."
   "Process the current buffer and set point at the end of the buffer."
   (interactive)
   (goto-char (point-max))
-  (proof-assert-until-point))
+  (proof-assert-until-point-interactive))
 
 ;; FIXME da: this could do with some tweaking.  Be careful to
 ;; avoid memory leaks.  If a buffer is killed and it's local
@@ -1433,7 +1457,7 @@ Start up the proof assistant if necessary."
   (insert cmd)
   ;; FIXME: could do proof-indent-line here, but let's
   ;; wait until indentation is fixed.
-  (proof-assert-until-point))
+  (proof-assert-until-point-interactive))
 
 
 
@@ -1540,8 +1564,7 @@ No action if BUF is nil."
 With arg, turn on the Active Terminator minor mode if and only if arg
 is positive.
 
-If active terminator mode is enabled, a terminator will process the
-current command."
+If active terminator mode is enabled, pressing a terminator will automatically activate `proof-assert-next-command' for convenience."
 
  (interactive "P")
  
@@ -1635,11 +1658,11 @@ Otherwise just do proof-restart-buffers to delete some spans from memory."
 (let ((map proof-mode-map))
 (define-key map [(control c) (control e)] 'proof-find-next-terminator)
 (define-key map [(control c) (control a)] 'proof-goto-command-start)
-(define-key map [(control c) (control n)] 'proof-assert-next-command)
-(define-key map [(control c) (return)]	  'proof-assert-next-command)
+(define-key map [(control c) (control n)] 'proof-assert-next-command-interactive)
+(define-key map [(control c) (return)]	  'proof-assert-next-command-interactive)
 (define-key map [(control c) (control t)] 'proof-try-command)
-(define-key map [(control c) ?u]	  'proof-retract-until-point)
-(define-key map [(control c) (control u)] 'proof-undo-last-successful-command)
+(define-key map [(control c) ?u]	  'proof-retract-until-point-interactive)
+(define-key map [(control c) (control u)] 'proof-undo-last-successful-command-interactive)
 (define-key map [(control c) ?\']	  'proof-goto-end-of-locked-interactive)
 ;; FIXME da: I don't understand what this function is supposed to do.
 ;; It will copy a proof command from within the locked region
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 7bb5c6e0..83098f88 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -66,9 +66,14 @@ Set in proof-shell-mode.")
   (SPAN,COMMAND,ACTION)
 
 triples, which is a queue of things to do.
-See the functions proof-start-queue and proof-exec-loop.")
+See the functions `proof-start-queue' and `proof-exec-loop'.")
 
+(defvar proof-analyse-using-stack nil
+  "Choice of syntax tree encoding for terms.
 
+If `nil', prover is expected to make no optimisations.
+If non-`nil', the pretty printer of the prover only reports local changes. 
+For LEGO 1.3.1 use `nil', for Coq 6.2, use `t'.")
 
 
 ;;
@@ -362,7 +367,7 @@ left around so the user may discover what killed the process."
   "Clear script buffers and send proof-shell-restart-cmd.
 All locked regions are cleared and the active scripting buffer
 deactivated.  The restart command should re-synchronize
-Proof General with the proof assitant."
+Proof General with the proof assistant."
   (interactive)
   (proof-script-remove-all-spans-and-deactivate)
   (setq proof-included-files-list nil
@@ -1390,7 +1395,6 @@ before and after sending the command."
 ;; Proof General shell mode definition				    ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-;; OLD COMMENT: "This has to come after proof-mode is defined"
 
 ;;###autoload
 (eval-and-compile			; to define vars
@@ -1440,7 +1444,7 @@ before and after sending the command."
 
 ;; watch difference with proof-shell-menu, proof-shell-mode-menu.
 (defvar proof-shell-menu proof-shared-menu
-  "The menu for the Proof-assistant shell")
+  "The menu for the Proof-assistant shell.")
 
 (easy-menu-define proof-shell-mode-menu
 		  proof-shell-mode-map
diff --git a/generic/proof-site.el b/generic/proof-site.el
index e758bf60..91802d1f 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -103,7 +103,7 @@ You can use customize to set this variable."
   (mapcar (lambda (astnt) (car astnt))
 	  proof-assistant-table)
   (concat
-   "*Choice of proof assitants to use with Proof General.
+   "*Choice of proof assistants to use with Proof General.
 A list of symbols chosen from:" 
    (apply 'concat (mapcar (lambda (astnt) 
 			    (concat " '" (symbol-name (car astnt))))
@@ -141,7 +141,7 @@ NOTE: to change proof assistant, you must start a new Emacs session.")
 
 ;; Now add auto-loads and load-path elements to support the 
 ;; proof assistants selected, and define a stub 
-(let ((assistants proof-assistants) assistant)
+(let ((assistants proof-assistants))
   (while assistants
     (let*  
 	((assistant (car assistants))	; compiler bogus warning here
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el
index a89dc536..4a0c3e68 100644
--- a/generic/proof-toolbar.el
+++ b/generic/proof-toolbar.el
@@ -13,8 +13,11 @@
 ;; Toolbar is just for scripting buffer at  the moment.
 ;;
 
+
+;;; IMPORT declaration 
 (require 'proof-script)
 (autoload 'proof-shell-live-buffer "proof-shell")
+(autoload 'proof-shell-restart "proof-shell")
 
 (defconst proof-toolbar-default-button-list
   '(proof-toolbar-goal-button
@@ -302,7 +305,7 @@ Move point if the end of the locked position is invisible."
       (progn
 	(proof-toolbar-move
 	 (goto-char (proof-unprocessed-begin))
-	 (proof-assert-next-command))
+	 (proof-assert-next-command-interactive))
 	(proof-toolbar-follow))))
 
 
@@ -321,7 +324,7 @@ Move point if the end of the locked position is invisible."
       (progn
 	(proof-toolbar-move
 	  (goto-char (point-min))
-	  (proof-retract-until-point))	; gives error if process busy
+	  (proof-retract-until-point-interactive))	; gives error if process busy
 	(proof-toolbar-follow))
     (error "Nothing to retract in this buffer!")))
 
diff --git a/generic/span-overlay.el b/generic/span-overlay.el
index fa113911..6cb572df 100644
--- a/generic/span-overlay.el
+++ b/generic/span-overlay.el
@@ -67,6 +67,8 @@ elements = S0 S1 S2 .... [tl-seq.el]"
 (defun span-read-only-hook (overlay after start end &optional len)
   (error "Region is read-only"))
 
+;;; FIXME: This is too harsh and breaks font-lock
+;;;        If only faces are modified we shouldn't call span-read-only-hook 
 (defun span-read-only (span)
   "Set SPAN to be read only."
   ;; Unfortunately, this function is called on spans which are