more direct output of remaining PGIP rudiments;

--- a/src/Pure/ProofGeneral/pgip_output.ML	Mon May 13 21:07:01 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-(*  Title:      Pure/ProofGeneral/pgip_output.ML
-    Author:     David Aspinall
-
-PGIP abstraction: output commands.
-*)
-
-signature PGIPOUTPUT =
-sig
-    datatype pgipoutput =
-      Hasprefs            of { prefcategory: string option, 
-                               prefs: PgipTypes.preference list }
-    | Pgip                of { tag: string option,
-                               class: string,
-                               seq: int, id: string,
-                               destid: string option,
-                               refid: string option,
-                               refseq: int option,
-                               content: XML.tree list }
-
-    val output : pgipoutput -> XML.tree
-end
-
-structure PgipOutput : PGIPOUTPUT =
-struct
-
-datatype pgipoutput =
-         Hasprefs            of { prefcategory: string option, 
-                                  prefs: PgipTypes.preference list }
-  |      Pgip                of { tag: string option,
-                                  class: string,
-                                  seq: int, id: string,
-                                  destid: string option,
-                                  refid: string option,
-                                  refseq: int option,
-                                  content: XML.tree list }
-
-fun output (Hasprefs vs) =
-    let 
-        val prefcategory = #prefcategory vs
-        val prefs = #prefs vs
-    in 
-        XML.Elem (("hasprefs", PgipTypes.opt_attr "prefcategory" prefcategory),
-          map PgipTypes.haspref prefs)
-    end
-  | output (Pgip vs) =
-    let
-        val tag = #tag vs
-        val class = #class vs
-        val seq = #seq vs
-        val id = #id vs
-        val destid = #destid vs
-        val refid = #refid vs
-        val refseq = #refseq vs
-        val content = #content vs
-    in
-        XML.Elem(("pgip",
-                 PgipTypes.opt_attr "tag" tag @
-                 PgipTypes.attr "id" id @
-                 PgipTypes.opt_attr "destid" destid @
-                 PgipTypes.attr "class" class @
-                 PgipTypes.opt_attr "refid" refid @
-                 PgipTypes.opt_attr_map string_of_int "refseq" refseq @
-                 PgipTypes.attr "seq" (string_of_int seq)),
-                 content)
-    end
-
-end
-

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon May 13 21:07:01 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon May 13 21:42:27 2013 +0200
@@ -34,21 +34,20 @@
   val pgip_seq = Unsynchronized.ref 0
   fun pgip_serial () = Unsynchronized.inc pgip_seq
 
-  fun assemble_pgips pgips =
-    PgipOutput.Pgip { tag = SOME pgip_tag,
-           class = pgip_class,
-           seq = pgip_serial (),
-           id = pgip_id,
-           destid = ! pgip_refid,
-           (* destid=refid since Isabelle only communicates back to sender *)
-           refid = ! pgip_refid,
-           refseq = ! pgip_refseq,
-           content = pgips }
+  fun assemble_pgip content =
+    XML.Elem(("pgip",
+             [("tag", pgip_tag), ("id", pgip_id)] @
+             PgipTypes.opt_attr "destid" (! pgip_refid) @
+             [("class", pgip_class)] @
+             PgipTypes.opt_attr "refid" (! pgip_refid) @
+             PgipTypes.opt_attr_map string_of_int "refseq" (! pgip_refseq) @
+             [("seq", string_of_int (pgip_serial ()))]),
+             content)
 in
 
 fun matching_pgip_id id = (id = pgip_id)
 
-val output_pgips = XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
+fun output_pgip content = Output.urgent_message (XML.string_of (assemble_pgip content));
 
 end;
 
@@ -106,16 +105,14 @@
 
 fun invalid_pgip () = raise PgipTypes.PGIP "Invalid PGIP packet received";
 
-fun output_emacs pgips = Output.urgent_message (output_pgips pgips);
-
 fun process_element_emacs (XML.Elem (("askprefs", _), _)) =
       let
-        fun preference_of {name, descr, default, pgiptype, get = _, set = _} =
-          {name = name, descr = SOME descr, default = SOME default, pgiptype = pgiptype};
+        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 (prefcat, prefs) =>
-            output_emacs
-              [PgipOutput.Hasprefs {prefcategory = SOME prefcat, prefs = map preference_of prefs}])
+        ! preferences |> List.app (fn (category, prefs) =>
+            output_pgip [XML.Elem (("hasprefs", [("prefcategory", category)]), map haspref prefs)])
       end
   | process_element_emacs (XML.Elem (("setpref", attrs), data)) =
       let

--- a/src/Pure/ROOT	Mon May 13 21:07:01 2013 +0200
+++ b/src/Pure/ROOT	Mon May 13 21:42:27 2013 +0200
@@ -160,7 +160,6 @@
     "Proof/proof_rewrite_rules.ML"
     "Proof/proof_syntax.ML"
     "Proof/reconstruct.ML"
-    "ProofGeneral/pgip_output.ML"
     "ProofGeneral/pgip_types.ML"
     "ProofGeneral/preferences.ML"
     "ProofGeneral/proof_general_emacs.ML"

--- a/src/Pure/ROOT.ML	Mon May 13 21:07:01 2013 +0200
+++ b/src/Pure/ROOT.ML	Mon May 13 21:42:27 2013 +0200
@@ -299,7 +299,6 @@
 (* configuration for Proof General *)
 
 use "ProofGeneral/pgip_types.ML";
-use "ProofGeneral/pgip_output.ML";
 
 (use
   |> Unsynchronized.setmp Proofterm.proofs 0