Minor changes to avoid some compiler warnings

3 files changed, 51 insertions, 44 deletions

diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el
index 8e73fd48..ba987aeb 100644
--- a/generic/pg-assoc.el
+++ b/generic/pg-assoc.el
@@ -26,6 +26,20 @@
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
+;; Return a list of associated buffers
+;;
+
+(defun proof-associated-buffers ()
+  "Return a list of the associated buffers.  
+Some may be dead/nil."
+  (list proof-goals-buffer
+	proof-response-buffer
+	proof-trace-buffer
+	proof-thms-buffer))
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
 ;; Manipulating prover output
 ;;
 
diff --git a/generic/pg-metadata.el b/generic/pg-metadata.el
index 1032d684..c6fd5504 100644
--- a/generic/pg-metadata.el
+++ b/generic/pg-metadata.el
@@ -51,42 +51,43 @@
 
 ;; Main code
 
-(defun pg-write-metadata-file (buffer)
-  "Write meta data for a script buffer BUFFER."
-  ;; FIXME: should check buffer has been saved
-  (if (buffer-file-name buffer)
-      (let* ((scriptfile    (buffer-file-name buffer))
-	     (modtime	    (nth 5 (file-attributes scriptfile)))
-	     (metadatafile  (pg-metadata-filename-for scriptfile))
-	     (metadatabuf   (find-file-noselect metadatafile 'nowarn))
-	     (span	   (span-at (point-min) 'type))
-	     type)
-	(pg-xml-begin-write)
-	(pg-xml-openelt 'script-file 
-			(list (list 'filename scriptfile)
-			      (list 'filedate modtime)))
-	(pg-xml-closeelt)
-	(while span
-	  (let ((type  (span-property span 'type))
-		(name  (span-property span 'name))
-		(start (span-start span))
-		(end   (span-end span)))
-	  (pg-xml-openelt 
-	   'span
-	   (list (list 'type type)
-		 (list 'name name)
-		 (list 'start start)
-		 (list 'end end)))
-	  ;; Include the span contents: can recover script file
-	  ;; from this.  (Could even display script using special
-	  ;; display functions?)
-	  (pg-xml-writetext (buffer-substring start end buffer))
-	  (pg-xml-closeelt))
-	  (setq span (next-span 'type)))
-	(with-current-buffer metadatabuf
-	  (delete-region (point-min) (point-max))
-	  (insert (pg-xml-doc))
-	  (write-file metadatafile)))))
+; FIXME: has compiler errors
+;(defun pg-write-metadata-file (buffer)
+;  "Write meta data for a script buffer BUFFER."
+;  ;; FIXME: should check buffer has been saved
+;  (if (buffer-file-name buffer)
+;      (let* ((scriptfile    (buffer-file-name buffer))
+;	     (modtime	    (nth 5 (file-attributes scriptfile)))
+;	     (metadatafile  (pg-metadata-filename-for scriptfile))
+;	     (metadatabuf   (find-file-noselect metadatafile 'nowarn))
+;	     (span	   (span-at (point-min) 'type))
+;	     type)
+;	(pg-xml-begin-write)
+;	(pg-xml-openelt 'script-file 
+;			(list (list 'filename scriptfile)
+;			      (list 'filedate modtime)))
+;	(pg-xml-closeelt)
+;	(while span
+;	  (let ((type  (span-property span 'type))
+;		(name  (span-property span 'name))
+;		(start (span-start span))
+;		(end   (span-end span)))
+;	  (pg-xml-openelt 
+;	   'span
+;	   (list (list 'type type)
+;		 (list 'name name)
+;		 (list 'start start)
+;		 (list 'end end)))
+;	  ;; Include the span contents: can recover script file
+;	  ;; from this.  (Could even display script using special
+;	  ;; display functions?)
+;	  (pg-xml-writetext (buffer-substring start end buffer))
+;	  (pg-xml-closeelt))
+;	  (setq span (next-span 'type)))
+;	(with-current-buffer metadatabuf
+;	  (delete-region (point-min) (point-max))
+;	  (insert (pg-xml-doc))
+;	  (write-file metadatafile)))))
 
 
 ;(defun pg-read-metadata-file (buffer)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 7927c22b..0eadcc28 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -397,14 +397,6 @@ Does nothing if proof assistant is already running."
 
       (message "Starting %s process... done." proc))))
 
-(defun proof-associated-buffers ()
-  "Return a list of the associated buffers.  
-Some may be dead/nil."
-  (list proof-goals-buffer
-	proof-response-buffer
-	proof-trace-buffer
-	proof-thms-buffer))
-
 
 ;;
 ;;  Shutting down proof shell and associated buffers