diff options
| author | David Aspinall | 2002-03-21 14:58:25 +0000 |
|---|---|---|
| committer | David Aspinall | 2002-03-21 14:58:25 +0000 |
| commit | 981a484180a242cbb17eb1f03c8eb37c96e0d310 (patch) | |
| tree | c3484ca3534d586f25e2e265d899a67c88d8659b | |
| parent | 7087f9f56126c7517cf2685ec15118c787639fd0 (diff) | |
New files.
| -rw-r--r-- | generic/pg-xhtml.el | 95 |
1 files changed, 95 insertions, 0 deletions
diff --git a/generic/pg-xhtml.el b/generic/pg-xhtml.el new file mode 100644 index 00000000..cc0a8cc6 --- /dev/null +++ b/generic/pg-xhtml.el @@ -0,0 +1,95 @@ +;; pg-xhtml.el XHTML goal display for Proof General +;; +;; Copyright (C) 2002 LFCS Edinburgh. +;; +;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; +;; $Id$ +;; + +(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)) + (char-to-string directory-sep-char))))) + +(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 "pg-xhtml-write-tempfile: cannot open temp dir " + (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 FILENAME 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) +;; End of pg-xhtml |