From 791e024efb9bdcb0b32a38d98158306996feea75 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Fri, 20 Aug 2010 11:19:30 +0000
Subject: Support Unicode from tokens.  Add export for whole directory

---
 generic/pg-movie.el | 68 +++++++++++++++++++++++++++++++++++++++--------------
 1 file changed, 51 insertions(+), 17 deletions(-)

(limited to 'generic/pg-movie.el')

diff --git a/generic/pg-movie.el b/generic/pg-movie.el
index 4e16b112..aecc5757 100644
--- a/generic/pg-movie.el
+++ b/generic/pg-movie.el
@@ -24,7 +24,9 @@
 
 ;;; Code:
 (eval-when-compile
-  (require 'span))
+  (require 'span)
+  (require 'unicode-tokens)
+  (require 'pg-user))
 
 (require 'pg-xml)
 
@@ -33,13 +35,29 @@
 (defconst pg-movie-stylesheet
   "<?xml-stylesheet type=\"text/xsl\" href=\"proviola-spp.xsl\"?>")
 
+(defun pg-movie-stylesheet-location ()
+  (concat proof-home-directory "etc/proviola/proviola-spp.xsl"))
+  
+
 (defvar pg-movie-frame 0 "Frame counter for movie.")
 
 (defun pg-movie-of-span (span)
-  (let* ((cmd      (buffer-substring-no-properties
-		    (span-start span) (span-end span)))
+  "Render annotated SPAN in XML."
+  (let* ((tokens   (proof-ass unicode-tokens-enable))
+	 (cmd      (buffer-substring-no-properties
+		      (span-start span) (span-end span)))
+	 (tcmd     (if tokens 
+		       ;; no subscripts of course
+		       (unicode-tokens-encode-str cmd)
+		     cmd))
 	 (helpspan (span-property span 'pg-helpspan))
-	 (resp     (and helpspan (span-property helpspan 'response)))
+	 (resp     (when helpspan 
+		     (span-property helpspan 'response)))
+	 (tresp    (if resp
+		       (if tokens 
+			   (unicode-tokens-encode-str resp)
+			 resp)
+		     ""))
 	 (type     (span-property span 'type))
 	 (class    (cond
 		    ((eq type 'comment) "comment")
@@ -56,8 +74,8 @@
 			       (append
 				(list (pg-xml-attr class class))
 				(if label (list (pg-xml-attr label label))))
-			       (list cmd))
-		  (pg-xml-node response nil (list (or resp "")))))))
+			       (list tcmd))
+		  (pg-xml-node response nil (list tresp))))))
 
 (defun pg-movie-of-region (start end)
   (list (pg-xml-node movie nil
@@ -66,15 +84,17 @@
 	 'pg-movie-of-span start end 'type))))))
 
 ;;;###autoload
-(defun pg-movie-export ()
-  "Export the movie file from the current script buffer."
-  (interactive)
+(defun pg-movie-export (&optional force)
+  "Export the movie file from the current script buffer.
+If FORCE, overwrite existing file without asking."
+  (interactive "DP")
   (setq pg-movie-frame 0)
   (let ((movie (pg-movie-of-region
 		(point-min)
 		(point-max)))
 	(movie-file-name
-	 (concat (file-name-sans-extension
+	 (concat 
+	  (file-name-sans-extension
 		  (buffer-file-name)) ".xml")))
 
     (with-current-buffer
@@ -83,18 +103,32 @@
       (insert pg-movie-xml-header "\n")
       (insert pg-movie-stylesheet "\n")
       (xml-print movie)
-      (write-file movie-file-name t))))
+      (write-file movie-file-name (not force)))))
 
 ;;;###autoload
-(defun pg-movie-export-from (script)
+(defun pg-movie-export-from (script &optional force)
   "Export the movie file that results from processing SCRIPT."
-  (interactive "f")
-  (let ((proof-full-annotation t)) ; dynamic
+  (interactive "fFile: 
+P")
+  (let ((proof-full-annotation t) ; dynamic
+	(proof-fast-process-buffer t))
     (find-file script)
-    (goto-char (point-max))
-    (proof-goto-point)
-    (pg-movie-export)))
+    (proof-process-buffer)
+    (pg-movie-export force)))
      
+;;;###autoload
+(defun pg-movie-export-directory (dir extn)
+  "Export movie files from directory DIR with extension EXTN.
+Existing XML files are overwritten."
+  (interactive "DDirectory: 
+sFile extension: ")
+  (let ((files (directory-files 
+		dir t 
+		(concat "\\." extn "$"))))
+    (dolist (f files)
+      (pg-movie-export-from f 'force))
+    (copy-file (pg-movie-stylesheet-location)
+	       dir 'overwrite)))
 
 
 (provide 'pg-movie)
-- 
cgit v1.2.3