author | wenzelm |
Mon, 07 May 2007 00:49:59 +0200 | |
changeset 22846 | fb79144af9a3 |
parent 22402 | a1cce5b241be |
child 23753 | d74a16b84e05 |
permissions | -rw-r--r-- |
21637 | 1 |
(* Title: Pure/ProofGeneral/pgip_types.ML |
2 |
ID: $Id$ |
|
3 |
Author: David Aspinall |
|
4 |
||
21940 | 5 |
PGIP abstraction: types and conversions. |
21637 | 6 |
*) |
7 |
||
22402 | 8 |
(* TODO: PGML, proverflag *) |
21637 | 9 |
signature PGIPTYPES = |
10 |
sig |
|
21867 | 11 |
(* Object types: the types of values which can be manipulated externally. |
12 |
Ideally a list of other types would be configured as a parameter. *) |
|
13 |
datatype objtype = ObjFile | ObjTheory | ObjTheorem | ObjComment |
|
14 |
| ObjTerm | ObjType | ObjOther of string |
|
15 |
||
16 |
(* Names for values of objtypes (i.e. prover identifiers). Could be a parameter. |
|
17 |
Names for ObjFiles are URIs. *) |
|
18 |
type objname = string |
|
19 |
||
20 |
type idtable = { context: objname option, (* container's objname *) |
|
21 |
objtype: objtype, |
|
22 |
ids: objname list } |
|
23 |
||
21637 | 24 |
(* Types and values (used for preferences and dialogs) *) |
25 |
||
26 |
datatype pgiptype = Pgipnull | Pgipbool | Pgipint of int option * int option | Pgipnat |
|
27 |
| Pgipstring | Pgipconst of string | Pgipchoice of pgipdtype list |
|
28 |
||
29 |
and pgipdtype = Pgipdtype of string option * pgiptype (* type with opt. description *) |
|
30 |
||
31 |
type pgipval (* typed value *) |
|
32 |
||
33 |
(* URLs we can cope with *) |
|
34 |
type pgipurl |
|
35 |
||
36 |
(* Representation error in reading/writing PGIP *) |
|
37 |
exception PGIP of string |
|
38 |
||
39 |
||
40 |
(* Interface areas for message output *) |
|
41 |
datatype displayarea = Status | Message | Display | Other of string |
|
42 |
||
43 |
(* Kinds of message output (influence display behaviour) *) |
|
44 |
datatype messagecategory = Normal | Information | Tracing | Internal |
|
45 |
||
46 |
(* Error levels *) |
|
22041 | 47 |
datatype fatality = Info | Warning | Nonfatal | Fatal | Panic | Log | Debug |
21637 | 48 |
|
49 |
(* File location *) |
|
50 |
type location = { descr: string option, |
|
51 |
url: pgipurl option, |
|
52 |
line: int option, |
|
53 |
column: int option, |
|
22162
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
54 |
char: int option, |
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
55 |
length: int option } |
21637 | 56 |
|
57 |
(* Prover preference *) |
|
58 |
type preference = { name: string, |
|
59 |
descr: string option, |
|
60 |
default: string option, |
|
61 |
pgiptype: pgiptype } |
|
62 |
end |
|
63 |
||
64 |
signature PGIPTYPES_OPNS = |
|
65 |
sig |
|
66 |
include PGIPTYPES |
|
21867 | 67 |
|
68 |
(* Object types *) |
|
69 |
val name_of_objtype : objtype -> string |
|
70 |
val attrs_of_objtype : objtype -> XML.attributes |
|
71 |
val objtype_of_attrs : XML.attributes -> objtype (* raises PGIP *) |
|
72 |
val idtable_to_xml : idtable -> XML.tree |
|
21637 | 73 |
|
74 |
(* Values as XML strings *) |
|
75 |
val read_pgipint : (int option * int option) -> string -> int (* raises PGIP *) |
|
76 |
val read_pgipnat : string -> int (* raises PGIP *) |
|
77 |
val read_pgipbool : string -> bool (* raises PGIP *) |
|
78 |
val read_pgipstring : string -> string (* raises PGIP *) |
|
79 |
val int_to_pgstring : int -> string |
|
80 |
val bool_to_pgstring : bool -> string |
|
81 |
val string_to_pgstring : string -> string |
|
82 |
||
83 |
(* PGIP datatypes *) |
|
84 |
val pgiptype_to_xml : pgiptype -> XML.tree |
|
85 |
val read_pgval : pgiptype -> string -> pgipval (* raises PGIP *) |
|
86 |
val pgval_to_string : pgipval -> string |
|
87 |
||
88 |
val attrs_of_displayarea : displayarea -> XML.attributes |
|
89 |
val attrs_of_messagecategory : messagecategory -> XML.attributes |
|
90 |
val attrs_of_fatality : fatality -> XML.attributes |
|
91 |
val attrs_of_location : location -> XML.attributes |
|
92 |
val location_of_attrs : XML.attributes -> location (* raises PGIP *) |
|
93 |
||
94 |
val haspref : preference -> XML.tree |
|
95 |
||
96 |
val pgipurl_of_url : Url.T -> pgipurl (* raises PGIP *) |
|
97 |
val pgipurl_of_string : string -> pgipurl (* raises PGIP *) |
|
98 |
val pgipurl_of_path : Path.T -> pgipurl |
|
21867 | 99 |
val path_of_pgipurl : pgipurl -> Path.T |
22003
34e190b24399
Be more chatty in PGIP file operations.proof_general_pgip.ML
aspinall
parents:
22000
diff
changeset
|
100 |
val string_of_pgipurl : pgipurl -> string |
21637 | 101 |
val attrs_of_pgipurl : pgipurl -> XML.attributes |
102 |
val pgipurl_of_attrs : XML.attributes -> pgipurl (* raises PGIP *) |
|
103 |
||
104 |
(* XML utils, only for PGIP code *) |
|
21867 | 105 |
val has_attr : string -> XML.attributes -> bool |
21637 | 106 |
val attr : string -> string -> XML.attributes |
107 |
val opt_attr : string -> string option -> XML.attributes |
|
108 |
val opt_attr_map : ('a -> string) -> string -> 'a option -> XML.attributes |
|
109 |
val get_attr : string -> XML.attributes -> string (* raises PGIP *) |
|
110 |
val get_attr_opt : string -> XML.attributes -> string option |
|
111 |
val get_attr_dflt : string -> string -> XML.attributes -> string |
|
112 |
end |
|
113 |
||
114 |
structure PgipTypes : PGIPTYPES_OPNS = |
|
115 |
struct |
|
116 |
exception PGIP of string |
|
117 |
||
21867 | 118 |
(** XML utils **) |
119 |
||
21902 | 120 |
fun has_attr (attr : string) attrs = AList.defined (op =) attrs attr |
21637 | 121 |
|
21902 | 122 |
fun get_attr_opt (attr : string) attrs = AList.lookup (op =) attrs attr |
21637 | 123 |
|
124 |
fun get_attr attr attrs = |
|
125 |
(case get_attr_opt attr attrs of |
|
126 |
SOME value => value |
|
21973
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
127 |
| NONE => raise PGIP ("Missing attribute: " ^ quote attr)) |
21637 | 128 |
|
129 |
fun get_attr_dflt attr dflt attrs = the_default dflt (get_attr_opt attr attrs) |
|
130 |
||
131 |
fun attr x y = [(x,y)] : XML.attributes |
|
132 |
||
133 |
fun opt_attr_map f attr_name opt_val = |
|
134 |
case opt_val of NONE => [] | SOME v => [(attr_name,f v)] |
|
135 |
(* or, if you've got function-itis: |
|
136 |
the_default [] (Option.map (single o (pair attr_name) o f) opt_val) |
|
137 |
*) |
|
138 |
||
21902 | 139 |
fun opt_attr attr_name = opt_attr_map I attr_name |
21637 | 140 |
|
21867 | 141 |
|
142 |
(** Objtypes **) |
|
143 |
||
144 |
datatype objtype = ObjFile | ObjTheory | ObjTheorem | ObjComment |
|
145 |
| ObjTerm | ObjType | ObjOther of string |
|
146 |
||
147 |
fun name_of_objtype obj = |
|
148 |
case obj of |
|
149 |
ObjFile => "file" |
|
150 |
| ObjTheory => "theory" |
|
151 |
| ObjTheorem => "theorem" |
|
152 |
| ObjComment => "comment" |
|
153 |
| ObjTerm => "term" |
|
154 |
| ObjType => "type" |
|
155 |
| ObjOther s => s |
|
156 |
||
21940 | 157 |
val attrs_of_objtype = attr "objtype" o name_of_objtype |
21867 | 158 |
|
159 |
fun objtype_of_attrs attrs = case get_attr "objtype" attrs of |
|
160 |
"file" => ObjFile |
|
161 |
| "theory" => ObjTheory |
|
162 |
| "theorem" => ObjTheorem |
|
163 |
| "comment" => ObjComment |
|
164 |
| "term" => ObjTerm |
|
165 |
| "type" => ObjType |
|
166 |
| s => ObjOther s (* where s mem other_objtypes_parameter *) |
|
167 |
||
168 |
type objname = string |
|
169 |
type idtable = { context: objname option, (* container's objname *) |
|
170 |
objtype: objtype, |
|
171 |
ids: objname list } |
|
172 |
||
173 |
fun idtable_to_xml {context, objtype, ids} = |
|
174 |
let |
|
175 |
val objtype_attrs = attrs_of_objtype objtype |
|
176 |
val context_attrs = opt_attr "context" context |
|
177 |
val ids_content = map (fn x => XML.Elem("identifier",[],[XML.Text x])) ids |
|
178 |
in |
|
179 |
XML.Elem ("idtable", |
|
180 |
objtype_attrs @ context_attrs, |
|
181 |
ids_content) |
|
182 |
end |
|
183 |
||
184 |
||
21637 | 185 |
(** Types and values **) |
186 |
||
187 |
(* readers and writers for values represented in XML strings *) |
|
188 |
||
189 |
fun read_pgipbool s = |
|
190 |
(case s of |
|
191 |
"false" => false |
|
192 |
| "true" => true |
|
21973
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
193 |
| _ => raise PGIP ("Invalid boolean value: " ^ quote s)) |
21637 | 194 |
|
195 |
local |
|
196 |
fun int_in_range (NONE,NONE) _ = true |
|
197 |
| int_in_range (SOME min,NONE) i = min<= i |
|
198 |
| int_in_range (NONE,SOME max) i = i<=max |
|
199 |
| int_in_range (SOME min,SOME max) i = min<= i andalso i<=max |
|
200 |
in |
|
201 |
fun read_pgipint range s = |
|
22009
b0c966b30066
approximate Syntax.read_int/nat by Int.fromString -- avoids dependency on Syntax module;
wenzelm
parents:
22003
diff
changeset
|
202 |
(case Int.fromString s of |
21637 | 203 |
SOME i => if int_in_range range i then i |
21973
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
204 |
else raise PGIP ("Out of range integer value: " ^ quote s) |
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
205 |
| NONE => raise PGIP ("Invalid integer value: " ^ quote s)) |
21637 | 206 |
end; |
207 |
||
208 |
fun read_pgipnat s = |
|
22009
b0c966b30066
approximate Syntax.read_int/nat by Int.fromString -- avoids dependency on Syntax module;
wenzelm
parents:
22003
diff
changeset
|
209 |
(case Int.fromString s of |
b0c966b30066
approximate Syntax.read_int/nat by Int.fromString -- avoids dependency on Syntax module;
wenzelm
parents:
22003
diff
changeset
|
210 |
SOME i => if i >= 0 then i |
b0c966b30066
approximate Syntax.read_int/nat by Int.fromString -- avoids dependency on Syntax module;
wenzelm
parents:
22003
diff
changeset
|
211 |
else raise PGIP ("Invalid natural number: " ^ quote s) |
21973
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
212 |
| NONE => raise PGIP ("Invalid natural number: " ^ quote s)) |
21637 | 213 |
|
214 |
(* NB: we can maybe do without xml decode/encode here. *) |
|
215 |
fun read_pgipstring s = (* non-empty strings, XML escapes decoded *) |
|
216 |
(case XML.parse_string s of |
|
217 |
SOME s => s |
|
21973
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
218 |
| NONE => raise PGIP ("Expected a non-empty string: " ^ quote s)) |
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
219 |
handle _ => raise PGIP ("Invalid XML string syntax: " ^ quote s) |
21637 | 220 |
|
21944 | 221 |
val int_to_pgstring = signed_string_of_int |
21637 | 222 |
|
223 |
fun string_to_pgstring s = XML.text s |
|
224 |
||
225 |
fun bool_to_pgstring b = if b then "true" else "false" |
|
226 |
||
227 |
||
228 |
(* PGIP datatypes. |
|
229 |
||
230 |
This is a reflection of the type structure of PGIP configuration, |
|
231 |
which is meant for setting up user dialogs and preference settings. |
|
232 |
These are configured declaratively in XML, using a syntax for types |
|
233 |
and values which is like a (vastly cut down) form of XML Schema |
|
234 |
Datatypes. |
|
235 |
||
236 |
The prover needs to interpret the strings representing the typed |
|
237 |
values, at least for the types it expects from the dialogs it |
|
238 |
configures. Here we go further and construct a type-safe |
|
239 |
encapsulation of these values, which would be useful for more |
|
240 |
advanced cases (e.g. generating and processing forms). |
|
241 |
*) |
|
242 |
||
243 |
||
244 |
datatype pgiptype = |
|
245 |
Pgipnull (* unit type: unique element is empty string *) |
|
246 |
| Pgipbool (* booleans: "true" or "false" *) |
|
247 |
| Pgipint of int option * int option (* ranged integers, should be XSD canonical *) |
|
248 |
| Pgipnat (* naturals: non-negative integers (convenience) *) |
|
249 |
| Pgipstring (* non-empty strings *) |
|
250 |
| Pgipconst of string (* singleton type *) |
|
251 |
| Pgipchoice of pgipdtype list (* union type *) |
|
252 |
||
253 |
(* Compared with the PGIP schema, we push descriptions of types inside choices. *) |
|
254 |
||
255 |
and pgipdtype = Pgipdtype of string option * pgiptype |
|
256 |
||
257 |
datatype pgipuval = Pgvalnull | Pgvalbool of bool | Pgvalint of int | Pgvalnat of int |
|
258 |
| Pgvalstring of string | Pgvalconst of string |
|
259 |
||
260 |
type pgipval = pgiptype * pgipuval (* type-safe values *) |
|
261 |
||
262 |
fun pgipdtype_to_xml (desco,ty) = |
|
263 |
let |
|
264 |
val desc_attr = opt_attr "descr" desco |
|
265 |
||
266 |
val elt = case ty of |
|
267 |
Pgipnull => "pgipnull" |
|
268 |
| Pgipbool => "pgipbool" |
|
269 |
| Pgipint _ => "pgipint" |
|
270 |
| Pgipnat => "pgipint" |
|
271 |
| Pgipstring => "pgipstring" |
|
272 |
| Pgipconst _ => "pgipconst" |
|
273 |
| Pgipchoice _ => "pgipchoice" |
|
274 |
||
275 |
fun range_attr r v = attr r (int_to_pgstring v) |
|
276 |
||
277 |
val attrs = case ty of |
|
278 |
Pgipint (SOME min,SOME max) => (range_attr "min" min)@(range_attr "max" max) |
|
279 |
| Pgipint (SOME min,NONE) => (range_attr "min" min) |
|
280 |
| Pgipint (NONE,SOME max) => (range_attr "max" max) |
|
281 |
| Pgipnat => (range_attr "min" 0) |
|
282 |
| Pgipconst nm => attr "name" nm |
|
283 |
| _ => [] |
|
284 |
||
285 |
fun destpgipdtype (Pgipdtype x) = x |
|
286 |
||
287 |
val typargs = case ty of |
|
288 |
Pgipchoice ds => map destpgipdtype ds |
|
289 |
| _ => [] |
|
290 |
in |
|
291 |
XML.Elem (elt, (desc_attr @ attrs), (map pgipdtype_to_xml typargs)) |
|
292 |
end |
|
293 |
||
21940 | 294 |
val pgiptype_to_xml = pgipdtype_to_xml o pair NONE |
21637 | 295 |
|
296 |
fun read_pguval Pgipnull s = |
|
297 |
if s="" then Pgvalnull |
|
21973
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
298 |
else raise PGIP ("Expecting empty string for null type, not: " ^ quote s) |
21637 | 299 |
| read_pguval Pgipbool s = Pgvalbool (read_pgipbool s) |
300 |
| read_pguval (Pgipint range) s = Pgvalint (read_pgipint range s) |
|
301 |
| read_pguval Pgipnat s = Pgvalnat (read_pgipnat s) |
|
302 |
| read_pguval (Pgipconst c) s = |
|
303 |
if c=s then Pgvalconst c |
|
21973
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
304 |
else raise PGIP ("Given string: "^quote s^" doesn't match expected string: "^quote c) |
21637 | 305 |
| read_pguval Pgipstring s = |
306 |
if s<>"" then Pgvalstring s |
|
307 |
else raise PGIP ("Expecting non-empty string, empty string illegal.") |
|
308 |
| read_pguval (Pgipchoice tydescs) s = |
|
309 |
let |
|
310 |
(* Union type: match first in list *) |
|
21940 | 311 |
fun getty (Pgipdtype(_, ty)) = ty |
21637 | 312 |
val uval = get_first |
313 |
(fn ty => SOME (read_pguval ty s) handle PGIP _ => NONE) |
|
314 |
(map getty tydescs) |
|
315 |
in |
|
21973
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
316 |
case uval of SOME pgv => pgv | NONE => raise PGIP ("Can't match string: "^quote s^ |
21637 | 317 |
" against any allowed types.") |
318 |
end |
|
319 |
||
320 |
fun read_pgval ty s = (ty, read_pguval ty s) |
|
321 |
||
322 |
fun pgval_to_string (_, Pgvalnull) = "" |
|
21940 | 323 |
| pgval_to_string (_, Pgvalbool b) = bool_to_pgstring b |
324 |
| pgval_to_string (_, Pgvalnat n) = int_to_pgstring n |
|
325 |
| pgval_to_string (_, Pgvalint i) = int_to_pgstring i |
|
326 |
| pgval_to_string (_, Pgvalconst c) = string_to_pgstring c |
|
327 |
| pgval_to_string (_, Pgvalstring s) = string_to_pgstring s |
|
21637 | 328 |
|
329 |
||
21867 | 330 |
type pgipurl = Path.T (* URLs: only local files *) |
21637 | 331 |
|
332 |
datatype displayarea = Status | Message | Display | Other of string |
|
333 |
||
334 |
datatype messagecategory = Normal | Information | Tracing | Internal |
|
335 |
||
22041 | 336 |
datatype fatality = Info | Warning | Nonfatal | Fatal | Panic | Log | Debug |
21637 | 337 |
|
338 |
type location = { descr: string option, |
|
339 |
url: pgipurl option, |
|
340 |
line: int option, |
|
341 |
column: int option, |
|
22162
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
342 |
char: int option, |
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
343 |
length: int option } |
21637 | 344 |
|
345 |
||
346 |
||
347 |
(** Url operations **) |
|
348 |
||
21867 | 349 |
|
21637 | 350 |
fun pgipurl_of_string url = (* only handle file:/// or file://localhost/ *) |
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents:
21637
diff
changeset
|
351 |
case Url.explode url of |
21637 | 352 |
(Url.File path) => path |
21973
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
353 |
| _ => raise PGIP ("Cannot access non-local URL " ^ quote url) |
21637 | 354 |
|
355 |
fun pgipurl_of_path p = p |
|
356 |
||
21973
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
357 |
fun path_of_pgipurl p = p (* potentially raises PGIP, but not with this implementation *) |
21867 | 358 |
|
22003
34e190b24399
Be more chatty in PGIP file operations.proof_general_pgip.ML
aspinall
parents:
22000
diff
changeset
|
359 |
fun string_of_pgipurl p = Path.implode p |
34e190b24399
Be more chatty in PGIP file operations.proof_general_pgip.ML
aspinall
parents:
22000
diff
changeset
|
360 |
|
22162
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
361 |
fun attrval_of_pgipurl purl = "file:" ^ (XML.text (File.platform_path (File.full_path purl))) |
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
362 |
fun attrs_of_pgipurl purl = [("url", attrval_of_pgipurl purl)] |
21637 | 363 |
|
21940 | 364 |
val pgipurl_of_attrs = pgipurl_of_string o get_attr "url" |
21637 | 365 |
|
366 |
fun pgipurl_of_url (Url.File p) = p |
|
21973
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
367 |
| pgipurl_of_url url = |
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
368 |
raise PGIP ("Cannot access non-local/non-file URL " ^ quote (Url.implode url)) |
21637 | 369 |
|
370 |
||
371 |
(** Messages and errors **) |
|
372 |
||
373 |
local |
|
374 |
fun string_of_area Status = "status" |
|
375 |
| string_of_area Message = "message" |
|
376 |
| string_of_area Display = "display" |
|
377 |
| string_of_area (Other s) = s |
|
378 |
||
379 |
fun string_of_msgcat Internal = "internal" |
|
380 |
| string_of_msgcat Information = "information" |
|
381 |
| string_of_msgcat Tracing = "tracing" |
|
382 |
| string_of_msgcat Normal = "normal" (* omitted in PGIP *) |
|
383 |
||
22041 | 384 |
fun string_of_fatality Info = "info" |
385 |
| string_of_fatality Warning = "warning" |
|
22000 | 386 |
| string_of_fatality Nonfatal = "nonfatal" |
21637 | 387 |
| string_of_fatality Fatal = "fatal" |
388 |
| string_of_fatality Panic = "panic" |
|
389 |
| string_of_fatality Log = "log" |
|
390 |
| string_of_fatality Debug = "debug" |
|
391 |
in |
|
392 |
fun attrs_of_displayarea area = [("area", string_of_area area)] |
|
393 |
||
394 |
fun attrs_of_messagecategory msgcat = |
|
395 |
case msgcat of |
|
396 |
Normal => [] |
|
397 |
| _ => [("messagecategory", string_of_msgcat msgcat)] |
|
398 |
||
399 |
fun attrs_of_fatality fatality = [("fatality", string_of_fatality fatality)] |
|
400 |
||
22162
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
401 |
fun attrs_of_location ({ descr, url, line, column, char, length }:location) = |
21637 | 402 |
let |
22162
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
403 |
val descr = opt_attr "location_descr" descr |
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
404 |
val url = opt_attr_map attrval_of_pgipurl "location_url" url |
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
405 |
val line = opt_attr_map int_to_pgstring "locationline" line |
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
406 |
val column = opt_attr_map int_to_pgstring "locationcolumn" column |
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
407 |
val char = opt_attr_map int_to_pgstring "locationcharacter" char |
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
408 |
val length = opt_attr_map int_to_pgstring "locationlength" length |
21637 | 409 |
in |
22162
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
410 |
descr @ url @ line @ column @ char @ length |
21637 | 411 |
end |
412 |
||
413 |
fun pgipint_of_string err s = |
|
22009
b0c966b30066
approximate Syntax.read_int/nat by Int.fromString -- avoids dependency on Syntax module;
wenzelm
parents:
22003
diff
changeset
|
414 |
case Int.fromString s of |
21637 | 415 |
SOME i => i |
21973
e7c9b0d3ce82
Quote arguments in PGIP exceptions. Tune comment.
aspinall
parents:
21944
diff
changeset
|
416 |
| NONE => raise PGIP ("Type error in " ^ quote err ^ ": expected integer.") |
21637 | 417 |
|
418 |
fun location_of_attrs attrs = |
|
419 |
let |
|
22162
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
420 |
val descr = get_attr_opt "location_descr" attrs |
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
421 |
val url = Option.map pgipurl_of_string (get_attr_opt "location_url" attrs) |
21637 | 422 |
val line = Option.map (pgipint_of_string "location element line attribute") |
22162
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
423 |
(get_attr_opt "locationline" attrs) |
21637 | 424 |
val column = Option.map (pgipint_of_string "location element column attribute") |
22162
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
425 |
(get_attr_opt "locationcolumn" attrs) |
21637 | 426 |
val char = Option.map (pgipint_of_string "location element char attribute") |
22162
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
427 |
(get_attr_opt "locationcharacter" attrs) |
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
428 |
val length = Option.map (pgipint_of_string "location element length attribute") |
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
429 |
(get_attr_opt "locationlength" attrs) |
21637 | 430 |
in |
22162
63dbc68eb527
Sync location with pgip.rnc, fixing attribute names
aspinall
parents:
22041
diff
changeset
|
431 |
{descr=descr, url=url, line=line, column=column, char=char, length=length} |
21637 | 432 |
end |
433 |
end |
|
434 |
||
435 |
(** Preferences **) |
|
436 |
||
437 |
type preference = { name: string, |
|
438 |
descr: string option, |
|
439 |
default: string option, |
|
440 |
pgiptype: pgiptype } |
|
441 |
||
442 |
fun haspref ({ name, descr, default, pgiptype}:preference) = |
|
443 |
XML.Elem ("haspref", |
|
444 |
attr "name" name @ |
|
445 |
opt_attr "descr" descr @ |
|
446 |
opt_attr "default" default, |
|
447 |
[pgiptype_to_xml pgiptype]) |
|
448 |
||
449 |
end |
|
450 |