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