blob: 9be9597221c71f973ce72539e9f27123d947d14b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
|
;;; pg-movie.el --- Export a processed script buffer for external replay
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc.
;; Portions © Copyright 2001-2017 Pierre Courtieu
;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
;; Portions © Copyright 2015-2017 Clément Pit-Claudel
;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;; 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!
;;
;;; Code:
(eval-when-compile
(require 'span)
(require 'unicode-tokens))
(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\"?>")
(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)
"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 (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")
((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 tcmd))
(pg-xml-node response nil (list tresp))))))
(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 (&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
(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 (not force)))))
;;;###autoload
(defun pg-movie-export-from (script &optional force)
"Export the movie file that results from processing SCRIPT."
(interactive "fFile:
P")
(let ((proof-full-annotation t) ; dynamic
(proof-fast-process-buffer t))
(find-file script)
(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)
;;; pg-movie.el ends here
|
