Add support for basic "movie" recording. See http://mws.cs.ru.nl/proviola.

4 files changed, 186 insertions, 43 deletions

diff --git a/generic/pg-movie.el b/generic/pg-movie.el
new file mode 100644
index 00000000..78e85167
--- /dev/null
+++ b/generic/pg-movie.el
@@ -0,0 +1,98 @@
+;;; pg-movie.el --- Export a processed script buffer for external replay
+;;
+;; Copyright (C) 2010 LFCS Edinburgh.
+;; Author:      David Aspinall <David.Aspinall@ed.ac.uk> and others
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+;;
+;; $Id$
+;;
+;;; Commentary:
+;;
+;; Given a processed proof script, write out an XML file that
+;; contains the buffer contents and the contents of prover
+;; output attached to spans.
+;;
+;; See etc/proviola and http://mws.cs.ru.nl/proviola/
+;;
+;; Much more could be done to dump the prettified output from the
+;; prover, but this is probably not the right way of doing things in
+;; general (one would rather have prover-integrated batch tools).  
+;;
+;; It does give quick and easy results for provers already supported by
+;; Proof General though!
+;;
+
+(require 'pg-xml)
+
+(defconst pg-movie-xml-header "<?xml version=\"1.0\"?>")
+
+(defconst pg-movie-stylesheet 
+  "<?xml-stylesheet type=\"text/xsl\" href=\"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)))
+	 (helpspan (span-property span 'pg-helpspan))
+	 (resp     (and helpspan (span-property helpspan 'response)))
+	 (type     (span-property span 'type))
+	 (class    (cond 
+		    ((eq type 'comment) "comment")
+		    ((eq type 'proof) "lemma")
+		    ((eq type 'goalsave) "lemma")
+		    (t "command")))
+	 (label    (span-property span 'rawname))
+	 (frameid  (int-to-string pg-movie-frame)))
+    (incf pg-movie-frame)
+    (pg-xml-node frame 
+		 (list (pg-xml-attr frameNumber frameid))
+		 (list 
+		  (pg-xml-node command 
+			       (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 "")))))))
+
+(defun pg-movie-of-region (start end)
+  (list (pg-xml-node movie nil
+     (list (pg-xml-node film nil
+	(span-mapcar-spans-inorder
+	 'pg-movie-of-span start end 'type))))))
+
+;;;###autoload  
+(defun pg-movie-export ()
+  "Export the movie file from the current script buffer."
+  (interactive)
+  (setq pg-movie-frame 0)
+  (let ((movie (pg-movie-of-region 
+		(point-min)
+		(point-max)))
+	(movie-file-name
+	 (concat (file-name-sans-extension
+		  (buffer-file-name)) ".xml")))
+
+    (with-current-buffer
+	(get-buffer-create "*pg-movie*")
+      (erase-buffer)
+      (insert pg-movie-xml-header "\n")
+      (insert pg-movie-stylesheet "\n")
+      (xml-print movie)
+      (write-file movie-file-name t))))
+
+;;;###autoload  
+(defun pg-movie-export-from (script)
+  "Export the movie file that results from processing SCRIPT."
+  (interactive "f")
+  (let ((proof-full-annotation t)) ; dynamic
+    (find-file script)
+    (goto-char (point-max))
+    (proof-goto-point)
+    (pg-movie-export)))
+     
+
+
+(provide 'pg-movie)
+
+;;; pg-movie.el ends here
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 74afce2e..23b816e0 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -197,6 +197,22 @@ Initialise the goals buffer after the child has been configured.
 
 ;;;***
 
+;;;### (autoloads (pg-movie-export-from pg-movie-export) "pg-movie"
+;;;;;;  "pg-movie.el" (19544 3005))
+;;; Generated autoloads from pg-movie.el
+
+(autoload 'pg-movie-export "pg-movie" "\
+Not documented
+
+\(fn)" t nil)
+
+(autoload 'pg-movie-export-from "pg-movie" "\
+Not documented
+
+\(fn SCRIPT)" nil nil)
+
+;;;***
+
 ;;;### (autoloads (pg-pgip-askprefs pg-pgip-maybe-askpgip pg-pgip-process-packet)
 ;;;;;;  "pg-pgip" "pg-pgip.el" (19122 39720))
 ;;; Generated autoloads from pg-pgip.el
@@ -222,7 +238,7 @@ Send an <askprefs> message to the prover.
 ;;;### (autoloads (pg-response-has-error-location proof-next-error
 ;;;;;;  pg-response-message pg-response-display-with-face pg-response-maybe-erase
 ;;;;;;  proof-response-config-done proof-response-mode) "pg-response"
-;;;;;;  "pg-response.el" (19159 42528))
+;;;;;;  "pg-response.el" (19542 60238))
 ;;; Generated autoloads from pg-response.el
 
 (autoload 'proof-response-mode "pg-response" "\
@@ -306,7 +322,7 @@ All of these settings are optional.
 ;;;;;;  pg-response-buffers-hint pg-slow-fontify-tracing-hint proof-electric-terminator-enable
 ;;;;;;  proof-define-assistant-command-witharg proof-define-assistant-command
 ;;;;;;  proof-goto-point proof-script-new-command-advance) "pg-user"
-;;;;;;  "pg-user.el" (19223 1859))
+;;;;;;  "pg-user.el" (19543 7684))
 ;;; Generated autoloads from pg-user.el
 
 (autoload 'proof-script-new-command-advance "pg-user" "\
@@ -412,11 +428,11 @@ Not documented
 
 ;;;***
 
-;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (19109
-;;;;;;  19687))
+;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (19542
+;;;;;;  60238))
 ;;; Generated autoloads from pg-xml.el
 
-(autoload (quote pg-xml-parse-string) "pg-xml" "\
+(autoload 'pg-xml-parse-string "pg-xml" "\
 Parse string in ARG, same as pg-xml-parse-buffer.
 
 \(fn ARG)" nil nil)
@@ -537,7 +553,7 @@ in future if we have just activated it for this buffer.
 ;;;;;;  proof-insert-pbp-command proof-register-possibly-new-processed-file
 ;;;;;;  pg-set-span-helphighlights proof-locked-region-empty-p proof-locked-region-full-p
 ;;;;;;  proof-unprocessed-begin proof-colour-locked) "proof-script"
-;;;;;;  "proof-script.el" (19223 1323))
+;;;;;;  "proof-script.el" (19543 20729))
 ;;; Generated autoloads from proof-script.el
 
 (autoload 'proof-colour-locked "proof-script" "\
@@ -564,11 +580,14 @@ Non-nil if the locked region is empty.  Works on any buffer.
 
 (autoload 'pg-set-span-helphighlights "proof-script" "\
 Add a daughter help span for SPAN with help message, highlight, actions.
-We add the last output (which should be non-empty) to the hover display here.
+The daughter span covers the non whitespace content of the main span.
+
+We add the last output (which should be non-empty) to the hover display.
+
 Optional argument MOUSEFACE means use the given face as a mouse highlight
 face, if it is a face, otherwise, if it is non-nil but not a face,
 do not add a mouse highlight.
-which case no mouse hover face is added.
+
 Argument FACE means add regular face property FACE to the span.
 
 \(fn SPAN &optional MOUSEFACE FACE)" nil nil)
@@ -618,7 +637,7 @@ finish setup which depends on specific proof assistant configuration.
 ;;;;;;  proof-shell-invisible-cmd-get-result proof-shell-invisible-command
 ;;;;;;  proof-shell-wait proof-extend-queue proof-start-queue proof-shell-insert
 ;;;;;;  proof-shell-available-p proof-shell-ready-prover) "proof-shell"
-;;;;;;  "proof-shell.el" (19220 59810))
+;;;;;;  "proof-shell.el" (19543 16432))
 ;;; Generated autoloads from proof-shell.el
 
 (autoload 'proof-shell-ready-prover "proof-shell" "\
@@ -739,7 +758,7 @@ processing.
 ;;;***
 
 ;;;### (autoloads (proof-ready-for-assistant) "proof-site" "proof-site.el"
-;;;;;;  (19220 63573))
+;;;;;;  (19542 60238))
 ;;; Generated autoloads from proof-site.el
 
 (autoload 'proof-ready-for-assistant "proof-site" "\
@@ -884,10 +903,10 @@ If PROGRAM is a string, any more args are arguments to PROGRAM.
 ;;;***
 
 ;;;### (autoloads (texi-docstring-magic) "texi-docstring-magic" "../lib/texi-docstring-magic.el"
-;;;;;;  (19107 62790))
+;;;;;;  (19542 60238))
 ;;; Generated autoloads from ../lib/texi-docstring-magic.el
 
-(autoload (quote texi-docstring-magic) "texi-docstring-magic" "\
+(autoload 'texi-docstring-magic "texi-docstring-magic" "\
 Update all texi docstring magic annotations in buffer.
 With prefix arg, no errors on unknown symbols.  (This results in
 @def .. @end being deleted if not known).
@@ -910,7 +929,7 @@ in your emacs font.
 ;;;***
 
 ;;;### (autoloads (unicode-tokens-encode-str) "unicode-tokens" "../lib/unicode-tokens.el"
-;;;;;;  (19221 49730))
+;;;;;;  (19496 21913))
 ;;; Generated autoloads from ../lib/unicode-tokens.el
 
 (autoload 'unicode-tokens-encode-str "unicode-tokens" "\
@@ -924,7 +943,7 @@ Return a unicode encoded version presentation of STR.
 ;;;;;;  "../lib/pg-fontsets.el" "../lib/proof-compat.el" "../lib/span.el"
 ;;;;;;  "pg-autotest.el" "pg-custom.el" "pg-pbrpm.el" "pg-vars.el"
 ;;;;;;  "proof-auxmodes.el" "proof-config.el" "proof-faces.el" "proof-useropts.el"
-;;;;;;  "proof.el") (19224 54205 534923))
+;;;;;;  "proof.el") (19544 3030 500218))
 
 ;;;***
 
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 9efe56aa..0d671db5 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -573,8 +573,13 @@ without adjusting window layout."
 (defconst proof-advanced-menu
   (cons "Advanced"
 	(append
-	 '(["Complete Identifier" proof-script-complete t]
-	   ["Insert Last Output" pg-insert-last-output-as-comment proof-shell-last-output])
+	 '(["Complete Identifier" proof-script-complete 
+	    :help "Complete the identifier at point"]
+	   ["Insert Last Output" pg-insert-last-output-as-comment 
+	    :active proof-shell-last-output
+	    :help "Insert the last output into the proof script as a comment"]
+	   ["Make Movie" pg-movie-export
+	    :help "Export processed portion as Movie XML file (enable Full Annotations first!)"])
 	 (list "-----")
 	 proof-show-hide-menu
 	 (list "-----")
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 3ad877a3..2190799d 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -510,14 +510,19 @@ IDIOM is a symbol, ID is a string."
   "Add element of type IDIOMSYM with identifier ID, referred to by SPAN.
 This records the element in `pg-script-portions' and sets span
 properties accordingly.
+
 IDIOMSYM is a symbol, whereas ID and optional NAME are strings.
 Identifiers must be unique for a given idiom; the optional NAME
 will be recorded as a textual name used instead of ID for users;
-NAME does not need to be unique."
+NAME does not need to be unique.
+
+NAME is a name that comes from the proof script or prover output.
+It is recorded in the span with the 'rawname property."
   (assert (symbolp idiomsym))
   (assert (stringp id))
   (if name (assert (stringp name)))
   (let* ((idsym    (intern id))
+	 (rawname  name)
 	 (name	   (or name id))
 	 (idiom    (symbol-name idiomsym))
 	 (delfn	   `(lambda () (pg-remove-element 
@@ -535,6 +540,7 @@ NAME does not need to be unique."
     (span-set-property span 'idiom idiomsym)
     (span-set-property span 'id idsym)
     (span-set-property span 'name name)
+    (span-set-property span 'rawname rawname)
     (span-set-property span 'span-delete-action delfn)
     
     ;; Ideally: would keep invisible property to be the idiom type
@@ -652,13 +658,19 @@ IDIOMSYM is a symbol and ID is a strings."
     "Keymap for the span context menu.")
 
 (defun pg-last-output-displayform ()
-  "Return displayable form of `proof-shell-last-output'."
-  (if (string= proof-shell-last-output "")  ""
-    (let ((text (proof-shell-strip-output-markup
-		 (if (and (boundp 'unicode-tokens-mode)
-			  unicode-tokens-mode)
-		     (unicode-tokens-encode-str proof-shell-last-output)
-		   proof-shell-last-output))))
+  "Return displayable form of `proof-shell-last-output'.
+This is used to annotate the buffer with the result of proof steps."
+  ;; If there's no proof state output we try response output instead.
+  ;; NOTE: Isabelle/Isar uses urgent messages (sigh) in its ordinary output.
+  ;; ("Successful attempt...").  This loses here.
+  (let* ((output (if (string= proof-shell-last-output "")
+		     proof-shell-last-response-output))
+	 (text (proof-shell-strip-output-markup
+		(if (and (boundp 'unicode-tokens-mode)
+			 unicode-tokens-mode)
+		    (unicode-tokens-encode-str proof-shell-last-output)
+		  output))))
+
       ;; NOTE: hack for Isabelle which puts ugly leading \n's around proofstate.
       (if (and (> (length text) 0) 
 	       (string= (substring text 0 1) "\n"))
@@ -666,39 +678,48 @@ IDIOMSYM is a symbol and ID is a strings."
       (if (and (> (length text) 0) 
 	       (string= (substring text -1) "\n"))
 	  (setq text (substring text 0 -1)))
-      text)))
+	
+      text))
 
 ;;;###autoload
 (defun pg-set-span-helphighlights (span &optional mouseface face)
   "Add a daughter help span for SPAN with help message, highlight, actions.
-We add the last output (which should be non-empty) to the hover display here.
+The daughter span covers the non whitespace content of the main span.
+
+We add the last output (which should be non-empty) to the hover display.
+
 Optional argument MOUSEFACE means use the given face as a mouse highlight
 face, if it is a face, otherwise, if it is non-nil but not a face,
 do not add a mouse highlight.
-which case no mouse hover face is added.
+
 Argument FACE means add regular face property FACE to the span."
-  (let ((helpmsg    (pg-span-name span))
-	(proofstate (pg-last-output-displayform))
+  (let ((output     (pg-last-output-displayform))
 	(newspan    (let ((newstart (save-excursion
 				      (goto-char (span-start span))
 				      (skip-chars-forward " \n\t")
 				      (point))))
 		      (span-make newstart (span-end span)))))
-    (setq helpmsg
-	  (concat (if (<= (length proofstate) 2) helpmsg)
-		  proofstate))
+
+    (span-set-property span 'pg-helpspan newspan) ; link to parent
+
     (span-set-property newspan 'pghelp t)
-    (if pg-show-hints ;; only message in minibuf if hints on
-	(span-set-property
-	 newspan 'help-echo
-	   helpmsg
-	   ;; " ("
-	   ;; (substitute-command-keys
-	   ;;  (if (span-property span 'idiom)
-	   ;;	"with point in region, \\[pg-toggle-visibility] to show/hide; "
-	   ;;    "\\<pg-span-context-menu-keymap>\\[pg-span-context-menu]"))
-	   ;; " for menu)")))
-	   ))
+    (span-set-property newspan 'response output)
+
+    (span-set-property newspan 'help-echo 
+	(if (<= (length output) 2)
+	      (pg-span-name span)
+	    output))	       
+
+    ;; Here's the message we used to show in minibuffer 
+    ;; when pg-show-hints was on:
+    ;;
+    ;; " ("
+    ;; (substitute-command-keys
+    ;;  (if (span-property span 'idiom)
+    ;;	"with point in region, \\[pg-toggle-visibility] to show/hide; "
+    ;;    "\\<pg-span-context-menu-keymap>\\[pg-span-context-menu]"))
+    ;; " for menu)")))
+
     (span-set-property newspan 'keymap pg-span-context-menu-keymap)
     (span-set-property newspan 'modification-hooks
 		       (list 'pg-delete-self-modification-hook))