blob: 49287b7e2ac9f78a4001a72a13087d8815f0d132 (
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
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
|
;; pg-pgip-old.el Functions for processing PGIP for Proof General
;;
;; This file contains some backwards compatiblity functions for
;; dealing with PGIP 1.X messages. The only case that these are
;; needed is for interim backward compatibility with Isabelle2003 and
;; Isabelle2004, for processing preference settings.
;;
;; FIXME: resurrect pg-prover-interpret-pgip-command (could try with pg-pgip-string-of-command)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Message processing: BACKWARD COMPATIBILITY
;;
;; <haspref default="d" kind="k" type="t"
;; description="d" class="c">name</haspref>
(defun pg-pgip-process-oldhaspref (node) ;; for Isabelle 2004
(pg-pgip-process-haspref node))
(defun pg-pgip-process-haspref (node) ;; for Isabelle 2003
"Issue a defpacustom from a <haspref> element with attributes ATTRS, name NAME."
(let*
((name (pg-xml-get-text-content node)) ;; old PGIP: <haspref>name<haspref>
(type (pg-pgip-old-get-type node))
(defattr (pg-xml-get-attr 'default node t))
(default (if defattr
(pg-pgip-old-interpret-value defattr type)
(pg-pgip-old-default-for type)))
(kind (intern
(pg-xml-get-attr 'kind node t "user")))
(descr (pg-xml-get-attr 'descr node t ""))
(subst (pg-pgip-subst-for type))
(setting
(pg-pgip-string-of-command
(concat "<setpref name=\"" name "\">" subst "</setpref>")))
(symname (intern name)))
(ignore-errors
;; FIXME: allow rest of PGIP to be processed, would be better to
;; accumulate errors somehow.
(proof-debug "haspref calling defpacustom: name:%s default:%s type:%s setting:%s" symname default type setting)
(eval
;; FIXME: would like unique custom group for settings introduced by haspref.
;; (preferences or something).
`(defpacustom ,symname ,default
(concat descr (if descr "\n")
"Setting configured by <haspref> PGIP message")
:type (quote ,type)
:setting ,setting)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Interpretation of types in old format
;;
(defun pg-pgip-old-interpret-bool (value)
(cond
((string-equal value "true") t)
((string-equal value "false") nil)
;; Non-boolean value: return false, give debug message.
(t (progn
(proof-debug "pg-pgip-old-interpret-bool: received non-bool value %s" value)
nil))))
(defun pg-pgip-old-interpret-int (value)
;; FIXME: string-to-number returns zero for non int string,
;; should have better validation here.
(string-to-number value))
(defun pg-pgip-old-interpret-string (value)
value)
(defun pg-pgip-old-interpret-choice (choices value)
;; Untagged union types: test for each type in turn.
;; FIXME: nested unions not supported here.
(cond
((and
(memq 'boolean choices)
(or (string-equal value "true") (string-equal value "false")))
(pg-pgip-old-interpret-value value 'boolean))
((and
(memq 'integer choices)
(string-match "[0-9]+$" value))
(pg-pgip-old-interpret-value value 'integer))
((memq 'string choices)
;; FIXME: No special syntax for string inside PGIP yet, should be?
(pg-pgip-old-interpret-value value 'string))
(t
(pg-pgip-old-error
"pg-pgip-old-interpret-choice: mismatching value %s for choices %s"
value choices))))
(defun pg-pgip-old-interpret-value (value type)
(cond
((eq type 'boolean)
(pg-pgip-old-interpret-bool value))
((eq type 'integer)
(pg-pgip-old-interpret-int value))
((eq type 'string)
(pg-pgip-old-interpret-string value))
((and (consp type) (eq (car type) 'choice))
(pg-pgip-old-interpret-choice (cdr type) value))
(t
(pg-pgip-old-error "pg-pgip-old-interpret-value: unkown type %s" type))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Dealing with <pgiptype> in old format
;;
(defun pg-pgip-old-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
(pg-pgip-old-error "pg-pgip-old-default-for: unrecognized type passed in"))))
(defun pg-pgip-old-subst-for (type)
"Return a substitution string for type TYPE."
(cond
((eq type 'boolean) "%b")
((eq type 'integer) "%i")
(t "%s")))
(defun pg-pgip-old-get-type (node)
"Extract and check type value from NODE. Return type in internal (custom) format."
(let
((rawtype (pg-xml-get-attr 'type node)))
(pg-pgip-old-pgiptype rawtype)))
(defun pg-pgip-old-pgiptype (rawtype)
"Return internal (custom format) representation for <pgiptype> element."
(cond
((string-match "choice\(\\(.*\\)\)" rawtype)
(let* ((choiceslist (match-string 1 rawtype))
;; FIXME: nested choices not supported yet
(choices (split-string choiceslist "[ \f\t\n\r\v]*,[ \f\t\n\r\v]*")))
(list 'choice (mapcar 'pg-pgip-old-pgiptype 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-old-pgiptype: unrecognized type %s" rawtype))))
(provide 'pg-pgip-old)
;; End of `pg-pgip-old.el'
|
