Deleted file

1 files changed, 0 insertions, 112 deletions

diff --git a/generic/pg-metadata.el b/generic/pg-metadata.el
deleted file mode 100644
index 32a61049..00000000
--- a/generic/pg-metadata.el
+++ /dev/null
@@ -1,112 +0,0 @@
-;; pg-metadata.el ---  Persistant storage of metadata for proof scripts
-;;
-;; Copyright (C) 2001-2 LFCS Edinburgh.
-;; Author:      David Aspinall <David.Aspinall@ed.ac.uk>
-;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
-
-;;; Commentary:
-;; 
-;; Status: incomplete; experimental
-;;
-;; TODO:
-;;  - add file dependency information to proof scripts individually
-;;    (can approximate from the transitive closure that is included files list)
-;;
-;; NB: THIS FILE NOT YET USED: once required by PG,
-;; must be added to main dist by editing Makefile.devel
-;;
-;; TODO:
-;;  - look at using cookies for this (Elib)
-
-;;; Code:
-
-(require 'pg-xml)
-(require 'proof-config)			; proof-face-specs
-
-(defcustom pg-metadata-default-directory "~/.proofgeneral/"
-  "*Directory for storing metadata information about proof scripts."
-  :type 'file
-  :group 'proof-user-options)
-
-(defface proof-preparsed-span
-  (proof-face-specs
-   (:background "lightgoldenrodyellow")
-   (:background "darkgoldenrod")
-   (:underline t))
-  "*Face for pre-parsed regions of proof script (unprocessed commands)."
-  :group 'proof-faces)
-
-
-;; Utility functions
-
-(defun pg-metadata-filename-for (filename)
-  "Compute a revised FILENAME for storing corresponding metadata."
-  ;; We replace directory separators with double underscores.
-  ;; Clashes are possible, hopefully unlikely.
-  (concat
-   (file-name-as-directory pg-metadata-default-directory)
-   (replace-in-string (file-name-sans-extension filename) "/" "__")
-   ".pgm"))
-
-
-;; Main code
-
-; 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)
-;  "Read meta data for a script file BUFFER, and reconstitute spans.
-;Spans are only reconstituted for positions after (proof-unprocessed-begin),
-;and providing that the meta-data file is older than the script file."
-;  (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))
-;	     (metadata      (pg-xml-parse-buffer metadatabuf)))
-	
-;	     (span	   (span-at (point-min) 'type)))
-;	     type)
-
-
-(provide 'pg-metadata)
-;;; pg-metadata.el ends here