From b642237b9e312e57743561e674d65c4b1f8f15ce Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Sat, 17 Apr 2004 22:29:42 +0000
Subject: Minor changes to avoid some compiler warnings

---
 generic/pg-assoc.el    | 14 ++++++++++
 generic/pg-metadata.el | 73 +++++++++++++++++++++++++-------------------------
 generic/proof-shell.el |  8 ------
 3 files changed, 51 insertions(+), 44 deletions(-)

(limited to 'generic')

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
@@ -24,6 +24,20 @@
     (proof-define-keys proof-universal-keys-only-mode-map 
 		       proof-universal-keys)))
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; 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
-- 
cgit v1.2.3