blob: d856319943b5822ccd88cf7edd3538ef3a1fa222 (
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
|
;; pg-metadata.el Persistant storage of metadata for proof scripts
;;
;; Copyright (C) 2001-2 LFCS Edinburgh.
;; Author: David Aspinall <da@dcs.ed.ac.uk>
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; $Id$
;;
;; Status: incomplete; experimental
;;
;; TODO:
;; - add file dependency information to proof scripts individually
;; (can approximate from the transitive closure that is included files list)
;;
;; NB: THIS FILE NOT YET USED: once required by PG,
;; must be added to main dist by editing Makefile.devel
;;
(require 'pg-xml)
;; Variables
(defcustom pg-metadata-default-directory "~/.proofgeneral/"
"*Directory for storing metadata information about proof scripts."
:type 'file
:group 'proof-user-options)
(defface proof-preparsed-span
(proof-face-specs
(:background "lightgoldenrodyellow")
(:background "darkgoldenrod")
(:underline t))
"*Face for pre-parsed regions of proof script (unprocessed commands)."
:group 'proof-faces)
;; Utility functions
(defun pg-metadata-filename-for (filename)
"Compute a revised FILENAME for storing corresponding metadata."
;; We replace directory separators with double underscores.
;; Clashes are possible, hopefully unlikely.
(concat
(file-name-as-directory pg-metadata-default-directory)
(replace-in-string
(file-name-sans-extension filename)
(regexp-quote (char-to-string directory-sep-char))
"__")
".pgm"))
;; Main code
(defun pg-write-metadata-file (buffer)
"Write meta data for a script buffer BUFFER."
;; FIXME: should check buffer has been saved
(if (buffer-file-name buffer)
(let* ((scriptfile (buffer-file-name buffer))
(modtime (nth 5 (file-attributes scriptfile)))
(metadatafile (pg-metadata-filename-for scriptfile))
(metadatabuf (find-file-noselect metadatafile 'nowarn))
(span (span-at (point-min) 'type)))
type)
(pg-xml-begin-write)
(pg-xml-openelt 'script-file
(list (list 'filename scriptfile)
(list 'filedate modtime)))
(pg-xml-closeelt)
(while span
(let ((type (span-property span 'type))
(name (span-property span 'name))
(start (span-start span))
(end (span-end span)))
(pg-xml-openelt
'span
(list (list 'type type)
(list 'name name)
(list 'start start)
(list 'end end)))
;; Include the span contents: can recover script file
;; from this. (Could even display script using special
;; display functions?)
(pg-xml-writetext (buffer-substring start end buffer))
(pg-xml-closeelt))
(setq span (next-span 'type)))
(with-current-buffer metadatabuf
(delete-region (point-min) (point-max))
(insert (pg-xml-doc))
(write-file metadatafile))))
;(defun pg-read-metadata-file (buffer)
; "Read meta data for a script file BUFFER, and reconstitute spans.
;Spans are only reconstituted for positions after (proof-unprocessed-begin),
;and providing that the meta-data file is older than the script file."
; (if (buffer-file-name buffer)
; (let* ((scriptfile (buffer-file-name buffer))
; (modtime (nth 5 (file-attributes scriptfile)))
; (metadatafile (pg-metadata-filename-for scriptfile))
; (metadatabuf (find-file-noselect metadatafile 'nowarn))
; (metadata (pg-xml-parse-buffer metadatabuf)))
; (span (span-at (point-min) 'type)))
; type)
(provide 'pg-metadata)
;; pg-metadata.el ends here.
|
