Fix some compile errors

8 files changed, 19 insertions, 18 deletions

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)))