# HG changeset patch
# User wenzelm
# Date 1368476819 -7200
# Node ID 39052352427d3d9ee8bf80628a61212aeb98ccbd
# Parent  716bb7e2e272f7bfd922dcedc6c7bba5c11b0930
more direct output of remaining PGIP rudiments;
tuned signature;

diff -r 716bb7e2e272 -r 39052352427d src/Pure/ProofGeneral/pgip_types.ML
--- a/src/Pure/ProofGeneral/pgip_types.ML	Mon May 13 22:12:24 2013 +0200
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Mon May 13 22:26:59 2013 +0200
@@ -49,12 +49,6 @@
                       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 = 
@@ -88,8 +82,6 @@
     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
@@ -99,7 +91,6 @@
     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
@@ -114,8 +105,6 @@
 
 (** 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 =
@@ -432,19 +421,5 @@
       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
 
diff -r 716bb7e2e272 -r 39052352427d src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon May 13 22:12:24 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon May 13 22:26:59 2013 +0200
@@ -62,15 +62,13 @@
 
 fun invalid_pgip () = raise PgipTypes.PGIP "Invalid PGIP packet received";
 
+fun haspref ({name, descr, default, pgiptype, ...}: Preferences.preference) =
+  XML.Elem (("haspref", [("name", name), ("descr", descr), ("default", default)]),
+    [PgipTypes.pgiptype_to_xml pgiptype]);
+
 fun process_element_emacs (XML.Elem (("askprefs", _), _)) =
-      let
-        fun haspref {name, descr, default, pgiptype, get = _, set = _} =
-          PgipTypes.haspref {name = name, descr = SOME descr, default = SOME default,
-            pgiptype = pgiptype};
-      in
-        ! preferences |> List.app (fn (category, prefs) =>
-            output_pgip [XML.Elem (("hasprefs", [("prefcategory", category)]), map haspref prefs)])
-      end
+      ! preferences |> List.app (fn (category, prefs) =>
+          output_pgip [XML.Elem (("hasprefs", [("prefcategory", category)]), map haspref prefs)])
   | process_element_emacs (XML.Elem (("setpref", attrs), data)) =
       let
         val name =