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