blob: 963c6fd05992be431ff1cf12894eec610a0210c3 (
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
|
;; pg-pgip.el Functions for processing PGIP for Proof General
;;
;; Copyright (C) 2000-2002 LFCS Edinburgh.
;; Author: David Aspinall <da@dcs.ed.ac.uk>
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; $Id$
;;
;; Proof General Kit uses PGIP, an XML-message protocol
;; for interactive proof. This file contains functions
;; to process PGIP commands sent from the proof assistant.
;;
(defun pg-pgip-process-cmd (pgip)
"Process the command in PGIP, which should be parsed XML according to pg-xml-parse-*."
(while (pgip)
(let ((elt (caar pgip))
(attrs (cdar pgip)))
(cond
;; <pgip>
((eq elt 'pgip)) ;; ignore pgip attributes for now
;; <usespgml>
((eq elt 'usespgml)
(message "Received usespgml message, version %s"
(pg-pgip-get-version "usespgml" attrs)))
;; <haspref>
((eq elt 'haspref)
(pg-pgip-haspref attrs) ;; (cadr pgip))
(setq pgip (cdr pgip)))
;; <prefval>
((eq elt 'prefval)
)
;; <idtable>
((eq elt 'idtable)
)
;; <addid>
((eq elt 'addid)
)
;; <delid>
((eq elt 'delid)
)
;; <menuadd>
((eq elt 'menuadd)
)
((eq elt 'menudel)
))
;; Move on to next element
(setq pgip (cdr pgip)))))
(defun pg-pgip-haspref (attrs)
"Issue a defpacustom from a <haspref> element with attributes ATTRS"
(let*
((type (pg-pgip-get-type attrs))
(default (or (pg-pgip-get-attr "haspref" "default" attrs t)
;; If no default is supplied, make one
(pg-pgip-default-for type)))
(kind (intern
(or
(pg-pgip-get-attr "haspref" "kind" attrs t)
;; Default to kind user
"user")))
(name (intern (pg-pgip-get-attr "haspref" "name")))
(subst (pg-pgip-subst-for type))
(setting (concat "<pgip><setpref name=\"" name "\">" subst "</setpref></pgip>")))
(eval
(list 'defpacustom name default
;; FIXME: better docstring
"Setting configured by <haspref> PGIP message"
:type type
:setting setting))))
(defun pg-pgip-default-for (type)
"Synthesize a default value for type TYPE."
(cond
((eq type 'boolean) nil)
((eq type 'integer) 0)
((eq type 'string) "")
((eq (car-safe type) 'choice)
(car-safe (cdr-safe type)))
(t
(error "pg-pgip-default-for: unrecognized type passed in"))))
(defun pg-pgip-subst-for (type)
"Return a substitution string for type TYPE."
(cond
((eq type 'boolean) "%b")
((eq type 'integer) "%i")
(t "%s")))
(defun pg-pgip-get-type (attrs)
"Extract and check type value from ATTRS. Normalize to custom format."
(let ((rawtype (pg-pgip-get-attr "haspref" "type" attrs)))
(cond
((string-match "choice(\\(.*\\))" rawtype)
(let* ((choiceslist (match-string 1 rawtype))
(choices (split-string choiceslist "[ \f\t\n\r\v]*,[ \f\t\n\r\v]*")))
(list 'choice choices)))
((equal rawtype "boolean")
'boolean)
((equal rawtype "int")
'integer)
((equal rawtype "nat") ;; nat treated as int
'integer)
((equal rawtype "string")
'string)
(t
(error "pg-pgip-get-type: unrecognized type %s" rawtype)))))
;; Auxiliary functions for parsing
(defun pg-pgip-get-attr (elt attrnm attrs &optional optional)
(let ((vrs (assoc attrnm attrs)))
(if optional
vrs
(or vrs
(error "Didn't find %s attribute in %s element" attrnm elt)))))
(defun pg-pgip-get-version (elt attrs &optional optional)
(pg-pgip-get-attr elt "version" attrs optional))
;; End of `pg-pgip.el'
|
