diff options
-rw-r--r-- | generic/pg-movie.el | 98 | ||||
-rw-r--r-- | generic/proof-autoloads.el | 47 | ||||
-rw-r--r-- | generic/proof-menu.el | 9 | ||||
-rw-r--r-- | generic/proof-script.el | 75 |
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)) |