Fix some compile errors

13 files changed, 94 insertions, 80 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index cc6ecc60..e54822ef 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -51,27 +51,41 @@ is set to t, then ProofGeneral guesses the version of coq by doing
 ;; only coq-version-is-V74 and coq-version-is-V7 are used later (V6
 ;; corresponds to v7=nil and v74=nil)
 
+(unless (noninteractive) ;; DA: evaluating here gives error during compile
 (let* ((seedoc " (to force another version, do for example C-h v coq-version-is-V7)")
 		(v74 (concat "proofgeneral is in coq >= 7.4 mode" seedoc))
 		(v7 (concat "proofgeneral is in coq =< 7.3 mode" seedoc))
 		(v6 (concat "proofgeneral is in coq V6 mode" seedoc)))
   (cond
-	(coq-version-is-V74 (message v74) (setq coq-version-is-V7 t))
-	(coq-version-is-V7  (message v7)  (setq coq-version-is-V74 nil))
-	(coq-version-is-V6  (message v6)  (setq coq-version-is-V74 nil) (setq coq-version-is-V7 nil))
-	(t 
-	 (let* ((str (shell-command-to-string (concat coq-prog-name " -v")))
-			  (x (string-match "version \\([.0-9]*\\)" str))
-			  (num (match-string 1 str)))
-		(cond
-		 ((string-match num "\\<6.") (message msgv6)
-		  (setq coq-version-is-V7 nil) (setq coq-version-is-V74 nil))
-		 ((or (string-match num "\\<7.0") (string-match num "\\<7.1") 
-				(string-match num "\\<7.2") (string-match num "\\<7.3")) 
-		  (message v7) 
-		  (setq coq-version-is-V7 t) (setq coq-version-is-V74 nil))
-													 ;default: 7.3.1 and above ---> 7.4 
-		 (t (message v74) (setq coq-version-is-V7 t) (setq coq-version-is-V74 t)))))))
+   (coq-version-is-V74 
+    (message v74) 
+    (setq coq-version-is-V7 t))
+   (coq-version-is-V7  
+    (message v7)  
+    (setq coq-version-is-V74 nil))
+   (coq-version-is-V6  
+    (message v6)  
+    (setq coq-version-is-V74 nil) 
+    (setq coq-version-is-V7 nil))
+   (t 
+    (let* ((str (shell-command-to-string (concat coq-prog-name " -v")))
+	   (x (string-match "version \\([.0-9]*\\)" str))
+	   (num (match-string 1 str)))
+      (cond
+       ((string-match num "\\<6.") 
+	(message v6)
+	(setq coq-version-is-V7 nil) 
+	(setq coq-version-is-V74 nil))
+       ((or (string-match num "\\<7.0") (string-match num "\\<7.1") 
+	    (string-match num "\\<7.2") (string-match num "\\<7.3")) 
+	(message v7) 
+	(setq coq-version-is-V7 t) 
+	(setq coq-version-is-V74 nil))
+       ;;default: 7.3.1 and above ---> 7.4 
+       (t 
+	(message v74) 
+	(setq coq-version-is-V7 t) 
+	(setq coq-version-is-V74 t))))))))
 
 ;; ----- keywords for font-lock.
 
diff --git a/coq/coq.el b/coq/coq.el
index fd008ec8..810db4b4 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -847,7 +847,6 @@ This is specific to coq-mode."
 		proof-shell-process-file nil
 		proof-shell-inform-file-retracted-cmd nil)))
 
-(provide 'coq)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -896,6 +895,9 @@ mouse activation."
                  ,(format "Check %s." thm))))))
   )
 
+(provide 'coq)
+
+
 ;;;   Local Variables: ***
 ;;;   tab-width:2 ***
 ;;;   fill-column: 85 ***
diff --git a/generic/pg-metadata.el b/generic/pg-metadata.el
index d8563199..5dcfb276 100644
--- a/generic/pg-metadata.el
+++ b/generic/pg-metadata.el
@@ -59,7 +59,7 @@
 	     (modtime	    (nth 5 (file-attributes scriptfile)))
 	     (metadatafile  (pg-metadata-filename-for scriptfile))
 	     (metadatabuf   (find-file-noselect metadatafile 'nowarn))
-	     (span	   (span-at (point-min) 'type)))
+	     (span	   (span-at (point-min) 'type))
 	     type)
 	(pg-xml-begin-write)
 	(pg-xml-openelt 'script-file 
@@ -86,7 +86,7 @@
 	(with-current-buffer metadatabuf
 	  (delete-region (point-min) (point-max))
 	  (insert (pg-xml-doc))
-	  (write-file metadatafile))))
+	  (write-file metadatafile)))))
 
 
 ;(defun pg-read-metadata-file (buffer)
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el
index 7ff79d00..7842063d 100644
--- a/generic/pg-pgip.el
+++ b/generic/pg-pgip.el
@@ -247,15 +247,16 @@
      (or (string-equal value "true") (string-equal value "false")))
     (pg-pgip-interpret-value value 'boolean))
    ((and 
-     (memq 'integer (cdr type))
+     (memq 'integer choices)
      (string-match "[0-9]+$" value))
     (pg-pgip-interpret-value value 'integer))
-   ((memq 'string (cdr type))
+   ((memq 'string choices)
     ;; FIXME: No special syntax for string inside PGIP yet, should be?
     (pg-pgip-interpret-value value 'string))
    (t
-    (pg-pgip-error "pg-pgip-interpret-choice: mismatching value %s for choices %s" 
-		   value choices))))
+    (pg-pgip-error 
+     "pg-pgip-interpret-choice: mismatching value %s for choices %s" 
+     value choices))))
 
 (defun pg-pgip-interpret-value (value type)
   (cond
diff --git a/generic/pg-response.el b/generic/pg-response.el
index 6f555513..1591ad1a 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -325,13 +325,14 @@ and start at the first error."
 (defun pg-thms-buffer-clear ()
   "Clear the theorems buffer."
   (with-current-buffer proof-thms-buffer
+    (let (start str)
       (goto-char (point-max))
       (newline)				
       (setq start (point))
       (insert str)
       (unless (bolp) (newline))
       (proof-fontify-region start (point))
-      (set-buffer-modified-p nil)))
+      (set-buffer-modified-p nil))))
 
 
 
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 27adf37f..f6b7cdd6 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -552,7 +552,7 @@ Make sure the modeline is updated to display new value for electric terminator."
 
 (defun proof-electric-term-incomment-fn ()
   "Used as argument to proof-assert-until-point."
-  ;; CAREFUL: (1) dynamic scoping here 
+  ;; CAREFUL: (1) dynamic scoping here  (incomment, ins, mrk)
   ;;          (2) needs this name to be recognized in 
   ;;		  proof-assert-until-point
   (setq incomment t)
@@ -803,7 +803,7 @@ If NUM is negative, move upwards.  Return new span."
 
 (defun pg-fixup-children-span (span)
   (if (span-property span 'controlspan)
-      ;; WARNING: dynamic binding
+      ;; WARNING: dynamic binding for new-span
       (progn
 	(set-span-property span 'controlspan new-span)
 	(list span))))
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 56080211..3a8f7167 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1839,10 +1839,9 @@ This version is used when `proof-script-command-end-regexp' is set."
 		;; (FIXME: ignore nested comments here, we should
 		;; have a consistent policy!)
 		(unless
-		    (if (fboundp 'comment-forward)
-			(progn
+		    (if (progn
 			  (goto-char (or (match-end 1) (match-beginning 0)))
-			  (comment-forward))
+			  (forward-comment))
 		    (proof-re-search-forward 
 		     proof-script-comment-end-regexp cmdend t))
 		  (error
@@ -2385,7 +2384,7 @@ with `proof-script-set-buffer-hooks' which is what this function does,
 as well as setting `proof-script-buffer-file-name' (which see).
 
 This hook also gives a warning in case this is the active scripting buffer."
-  (setq proof-script-buffer-file-true buffer-file-name)
+  (setq proof-script-buffer-file-name buffer-file-name)
   (if (eq (current-buffer) proof-script-buffer)
       (proof-warning 
 "Active scripting buffer changed name; synchronization risked if prover tracks filenames!"))
diff --git a/generic/proof-site.el b/generic/proof-site.el
index d2205a2f..6001771d 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -83,9 +83,9 @@ You can use customize to set this variable."
 		    (cons proof-info-directory Info-directory-list))
 	      (setq Info-dir-contents nil)))
       ;; Info is not yet initialized.  Change its default.
-      (if (not (member proof-info-directory Info-default-directory-list))
-	  (setq Info-default-directory-list
-		(cons proof-info-directory Info-default-directory-list)))))
+      (if (not (member proof-info-directory Info-directory-list))
+	  (setq Info-directory-list
+		(cons proof-info-directory Info-directory-list)))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index da796e2c..639f206d 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -782,7 +782,7 @@ EXTRAPATH is a list of extra path components"
        (executable-find progname)))	;; PG 3.4: try a new Emacs function.
     ((fboundp 'locate-file)
      (locate-file progname
-		  (append (split-path (getenv "PATH") extrapth)) 
+		  (append (split-path (getenv "PATH") extrapath)) 
 		  (if proof-running-on-win32 '(".exe"))
 		  1)))
    (if returnnopath progname)))
diff --git a/generic/span-overlay.el b/generic/span-overlay.el
index 41097447..6055e03a 100644
--- a/generic/span-overlay.el
+++ b/generic/span-overlay.el
@@ -280,7 +280,7 @@ A span is before PT if it covers the character before PT."
   ;; list may be huge: is it a bottleneck?)
   ;; [Why has this function never used the before-list ?]
   (let* ((start     (overlay-start span))
-	 (pos       start)
+	 ;; (pos       start)
 	 (nextos    (overlays-in 
 		     (1+ start)
 		     (point-max)))
diff --git a/isa/x-symbol-isabelle.el b/isa/x-symbol-isabelle.el
index 5288f5aa..0fbb575c 100644
--- a/isa/x-symbol-isabelle.el
+++ b/isa/x-symbol-isabelle.el
@@ -175,6 +175,8 @@ Uses `x-symbol-isabelle-font-lock-scripts-regexp'."
 ;;;  Charsym Info
 ;;;===========================================================================
 
+;;; FIXME: da: attempting to compile these defcustoms gives error on
+;;;   !! Symbol's function definition is void ((x-symbol-set-cache-variable))
 (defcustom x-symbol-isabelle-class-alist
   '((VALID "Isabelle Symbol" (x-symbol-info-face))
     (INVALID "no Isabelle Symbol" (red x-symbol-info-face)))
diff --git a/lego/lego.el b/lego/lego.el
index 6a8b50d6..00a32319 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -350,11 +350,11 @@ Checks the width in the `proof-goals-buffer'"
   (setq outline-heading-end-regexp lego-outline-heading-end-regexp)
 
 ;; tags
-  (cond ((boundp 'tags-table-list)
+  (cond ((boundp 'tags-table-list) ;; GNU Emacs
 	 (make-local-variable 'tags-table-list)
 	 (setq tags-table-list (cons lego-tags tags-table-list))))
 
-  (and (boundp 'tag-table-alist)
+  (and (boundp 'tag-table-alist)  ;; XEmacs
        (setq tag-table-alist
 	     (append '(("\\.l$" . lego-tags)
 		       ("lego"  . lego-tags))
diff --git a/plastic/plastic.el b/plastic/plastic.el
index 5b033daf..463ab4ec 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -540,60 +540,55 @@ We assume that module identifiers coincide with file names."
 
 (defun plastic-large-bar () (interactive) (insert "%-------------------------------------------------------------------------------\n"))
 
-(defun plastic-preprocessing () 
+(defun plastic-preprocessing () ;; NB: dynamic scoping of string
    "clear comments and remove literate marks (ie, \\n> ) - acts on var string"
 
-   ;; might want to use proof-string-match here if matching is going to be
-   ;; case sensitive (see docs)
+   ;; might want to use proof-string-match here if matching is going
+   ;; to be case sensitive (see docs)
 
    (if (= 0 (length plastic-lit-string)) 
-	string		;; no-op if non-literate
-
-			;; remaining lines are the Else. (what, no 'return'?)
+       string				; no-op if non-literate
+     					; remaining lines are the
+     					; Else. (what, no 'return'?)
    (setq string (concat "\n" string " "))   ;; seed routine below, & extra char
    (let* ;; da: let* not really needed, added to nuke byte-comp warnings. 
-     ( (i 0)
-       (l (length string))
-       (eat-rest (lambda () 
+       (x 
+	(i 0)
+	(l (length string))
+	(eat-rest (lambda () 
                     (aset string i ?\ )  ;; kill the \n or "-" at least
                     (incf i)
                     (while (and (< i l) (/= (aref string i) ?\n))
-                           (aset string i ?\ )
-                           (incf i) )))
-       (keep-rest (lambda () 
-                    (loop for x in (string-to-list plastic-lit-string)
-                          do (aset string i ?\ ) (incf i))
-                    (while (and (< i l) 
-                                (/= (aref string i) ?\n)
-                                (/= (aref string i) ?-))
-                           (incf i) )))
-   )
-   (while (< i l)
-          (cond
-               ((eq 0 (string-match "--" (substring string i)))
-                   (funcall eat-rest))           ;; comment.
-               ((eq 0 (string-match "\n\n" (substring string i)))
-                   (aset string i ?\ ) 
-                   (incf i)) ;; kill repeat \n
-
-               ((= (aref string i) ?\n)		;; start of new line
-                   (aset string i ?\ ) (incf i) ;; remove \n
-
-	               (if (eq 0 (string-match plastic-lit-string 
-					         (substring string i)))
-                       (funcall keep-rest)       ;; code line.
-                       (funcall eat-rest)        ;; non-code line
-                   ))
-
-               (t (incf i))                      ;; else include.
-            )
-   )
-   (setq string (replace-in-string string "  *" " "))
-   (setq string (replace-in-string string "^ *" ""))
+		      (aset string i ?\ )
+		      (incf i) )))
+	(keep-rest (lambda () 
+		     (loop for x in (string-to-list plastic-lit-string)
+		       do (aset string i ?\ ) (incf i))
+		     (while (and (< i l) 
+				 (/= (aref string i) ?\n)
+				 (/= (aref string i) ?-))
+		       (incf i) ))))
+     (while (< i l)
+       (cond
+	((eq 0 (string-match "--" (substring string i)))
+	 (funcall eat-rest))		; comment.
+	((eq 0 (string-match "\n\n" (substring string i)))
+	 (aset string i ?\ ) 
+	 (incf i))			; kill repeat \n
+	((= (aref string i) ?\n)	; start of new line
+	 (aset string i ?\ ) (incf i)	; remove \n
+	 (if (eq 0 (string-match plastic-lit-string 
+				 (substring string i)))
+	     (funcall keep-rest)	; code line.
+	   (funcall eat-rest)		; non-code line
+	   ))
+	(t 
+	 (incf i))))			; else include.
+     (setq string (replace-in-string string "  *" " "))
+     (setq string (replace-in-string string "^ *" ""))
    (if (string-match "^\\s-*$" string)
        (setq string (concat "ECHO comment line" proof-terminal-string))
-       string)
-   )))
+     string))))
 
 
 (defun plastic-all-ctxt ()