src/Pure/ProofGeneral/pgip_types.ML

                       url: pgipurl option,
                       line: int option,
                       column: int option,
                       char: int option,
                       length: int option }
-
-    (* Prover preference *)   
-    type preference = { name: string,
-                        descr: string option,
-                        default: string option,
-                        pgiptype: pgiptype }
 end
 
 signature PGIPTYPES_OPNS = 
 sig
     include PGIPTYPES

     val attrs_of_displayarea : displayarea -> XML.attributes
     val attrs_of_fatality : fatality -> XML.attributes
     val attrs_of_location : location -> XML.attributes
     val location_of_attrs : XML.attributes -> location (* raises PGIP *)
 
-    val haspref : preference -> XML.tree
-
     val pgipurl_of_url : Url.T -> pgipurl              (* raises PGIP *)
     val pgipurl_of_string : string -> pgipurl          (* raises PGIP *)
     val pgipurl_of_path : Path.T -> pgipurl
     val path_of_pgipurl : pgipurl -> Path.T
     val string_of_pgipurl : pgipurl -> string
     val attrs_of_pgipurl : pgipurl -> XML.attributes
     val pgipurl_of_attrs : XML.attributes -> pgipurl   (* raises PGIP *)
 
     (* XML utils, only for PGIP code *)
-    val has_attr       : string -> XML.attributes -> bool
     val attr           : string -> string -> XML.attributes
     val opt_attr       : string -> string option -> XML.attributes
     val opt_attr_map   : ('a -> string) -> string -> 'a option -> XML.attributes
     val get_attr       : string -> XML.attributes -> string           (* raises PGIP *)
     val get_attr_opt   : string -> XML.attributes -> string option

 structure PgipTypes : PGIPTYPES_OPNS =
 struct
 exception PGIP of string
 
 (** XML utils **)
-
-fun has_attr attr attrs = Properties.defined attrs attr
 
 fun get_attr_opt attr attrs = Properties.get attrs attr
 
 fun get_attr attr attrs =
     (case get_attr_opt attr attrs of

       in 
           {descr=descr, url=url, line=line, column=column, char=char, length=length}
       end
 end
 
-(** Preferences **)
-
-type preference = { name: string,
-                    descr: string option,
-                    default: string option,
-                    pgiptype: pgiptype }
-
-fun haspref ({ name, descr, default, pgiptype}:preference) = 
-    XML.Elem (("haspref",
-              attr "name" name @
-              opt_attr "descr" descr @
-              opt_attr "default" default),
-              [pgiptype_to_xml pgiptype])
-
 end