aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--generic/pg-metadata.el112
-rw-r--r--generic/pg-xhtml.el104
2 files changed, 0 insertions, 216 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
diff --git a/generic/pg-xhtml.el b/generic/pg-xhtml.el
deleted file mode 100644
index da4eb157..00000000
--- a/generic/pg-xhtml.el
+++ /dev/null
@@ -1,104 +0,0 @@
-;; pg-xhtml.el --- XHTML goal display for Proof General
-;;
-;; Copyright (C) 2002 LFCS Edinburgh.
-;; Author: David Aspinall <David.Aspinall@ed.ac.uk>
-;; License: GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;; $Id$
-;;
-;; NB: THIS FILE NOT YET USED: once required by PG,
-;; must be added to main dist by editing Makefile.devel
-
-
-;;; Commentary:
-;;
-
-;;; Code:
-
-(require 'cl)
-(require 'pg-xml)
-
-;;
-;; Names for temporary files
-;;
-(defvar pg-xhtml-dir nil
- "Default value for XHTML directory.")
-
-(defun pg-xhtml-dir ()
- "Temporary directory for storing XHTML files."
- (or pg-xhtml-dir
- (setq pg-xhtml-dir
- (concat (if proof-running-on-win32
- "c:\\windows\\temp\\" ;; temp dir from env?
- (or (concat (getenv "TMP") "/") "/tmp/"))
- "pg"
- (getenv "USER")
- (int-to-string (emacs-pid))
- "/"))))
-
-(defvar pg-xhtml-file-count 0
- "Counter for generating XHTML files.")
-
-(defun pg-xhtml-next-file ()
- "Return new file name for XHTML storage."
- (concat
- (pg-xhtml-dir)
- (int-to-string (incf pg-xhtml-file-count))
- (if proof-running-on-win32 ".htm" ".html")))
-
-
-;;
-;; Writing an XHMTL file
-;;
-
-(defvar pg-xhtml-header
- "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN
-http://www.w3.org/TR/xhtml11/DTD/xhtml11-strict.dtd\">\n
-<!-- This file was automatically generated by Proof General -->\n\n"
- "Header for XHTML files.")
-
-(defmacro pg-xhtml-write-tempfile (&rest body)
- "Write a new temporary XHTML file, returning its location.
-BODY should contain a sequence of pg-xml writing commands."
- (let ((dir (pg-xhtml-dir))
- (file (pg-xhtml-next-file)))
- ;;
- (or (eq (car-safe (file-attributes dir)) 't)
- (if (not (file-attributes dir))
- (make-directory (pg-xhtml-dir) t)
- (error "Cannot open temp dir %s (in pg-xhtml-write-tempfile)"
- (pg-xhtml-dir))))
- `(with-temp-file ,file
- (pg-xml-begin-write t)
- (pg-xml-add-text pg-xhtml-header)
- ,@body
- (insert (pg-xml-doc))
- ,file)))
-
-(defun pg-xhtml-cleanup-tempdir ()
- "Cleanup temporary directory used for XHTML files."
- (delete-directory (pg-xhtml-dir)))
-
-(defvar pg-mozilla-prog-name
- "/usr/bin/mozilla"
- "Command name of browser to use with XHTML display.")
-
-(defun pg-xhtml-display-file-mozilla (file)
- "Display FILE in netscape/mozilla."
- (shell-command (concat pg-mozilla-prog-name
- " -remote \"openURL(" file ")\"")))
-
-(defalias 'pg-xhtml-display-file 'pg-xhtml-display-file-mozilla)
-
-; Test doc
-;(pg-xhtml-display-file-mozilla
-;(pg-xhtml-write-tempfile
-; (pg-xml-openelt 'root)
-; (pg-xml-openelt 'a '((class . "1B")))
-; (pg-xml-writetext "text a")
-; (pg-xml-closeelt)
-; (pg-xml-closeelt)))
-
-
-(provide 'pg-xhtml)
-;;; pg-xhtml.el ends here
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-22 23:49:54 +0000