simplified modules and exceptions;

--- a/src/Pure/ProofGeneral/pgip_types.ML	Tue May 14 21:40:25 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(*  Title:      Pure/ProofGeneral/pgip_types.ML
-    Author:     David Aspinall
-
-Some PGIP types and conversions.
-*)
-
-signature PGIPTYPES =
-sig
-  exception PGIP of string
-  val attr: string -> string -> XML.attributes
-  val opt_attr: string -> string option -> XML.attributes
-  val get_attr: XML.attributes -> string -> string           (* raises PGIP *)
-end
-
-structure PgipTypes : PGIPTYPES =
-struct
-
-exception PGIP of string
-
-fun get_attr attrs name =
-  (case Properties.get attrs name of
-    SOME value => value
-  | NONE => raise PGIP ("Missing attribute: " ^ quote name));
-
-fun attr x y = [(x,y)] : XML.attributes
-
-fun opt_attr _ NONE = []
-  | opt_attr name (SOME value) = attr name value;
-
-end
-

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue May 14 21:40:25 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue May 14 21:56:19 2013 +0200
@@ -14,18 +14,28 @@
 
 (* output PGIP packets *)
 
+fun get_attr attrs name =
+  (case Properties.get attrs name of
+    SOME value => value
+  | NONE => raise Fail ("Missing attribute: " ^ quote name));
+
+fun attr x y = [(x, y)] : XML.attributes;
+
+fun opt_attr _ NONE = []
+  | opt_attr name (SOME value) = attr name value;
+
 val pgip_id = "dummy";
 val pgip_serial = Synchronized.counter ();
 
 fun output_pgip refid refseq content =
   XML.Elem (("pgip",
-    PgipTypes.attr "tag" "Isabelle/Isar" @
-    PgipTypes.attr "id" pgip_id @
-    PgipTypes.opt_attr "destid" refid @
-    PgipTypes.attr "class" "pg" @
-    PgipTypes.opt_attr "refid" refid @
-    PgipTypes.attr "refseq" refseq @
-    PgipTypes.attr "seq" (string_of_int (pgip_serial ()))), content)
+    attr "tag" "Isabelle/Isar" @
+    attr "id" pgip_id @
+    opt_attr "destid" refid @
+    attr "class" "pg" @
+    opt_attr "refid" refid @
+    attr "refseq" refseq @
+    attr "seq" (string_of_int (pgip_serial ()))), content)
   |> XML.string_of
   |> Output.urgent_message;
 
@@ -47,7 +57,7 @@
 
 local
 
-fun invalid_pgip () = raise PgipTypes.PGIP "Invalid PGIP packet received";
+fun invalid_pgip () = raise Fail "Invalid PGIP packet";
 
 fun haspref ({name, descr, default, pgiptype, ...}: Preferences.preference) =
   XML.Elem (("haspref", [("name", name), ("descr", descr), ("default", default)]),
@@ -71,17 +81,17 @@
   (case XML.parse str of
     XML.Elem (("pgip", attrs), pgips) =>
       let
-        val class = PgipTypes.get_attr attrs "class";
+        val class = get_attr attrs "class";
         val dest = Properties.get attrs "destid";
         val refid = Properties.get attrs "id";
-        val refseq = PgipTypes.get_attr attrs "seq";
+        val refseq = get_attr attrs "seq";
         val processit =
           (case dest of
             NONE => class = "pa"
           | SOME id => id = pgip_id);
        in if processit then List.app (process_element refid refseq) pgips else () end
   | _ => invalid_pgip ())
-  handle PgipTypes.PGIP msg => error (msg ^ "\n" ^ str);
+  handle Fail msg => raise Fail (msg ^ "\n" ^ str);
 
 in
 

--- a/src/Pure/ROOT	Tue May 14 21:40:25 2013 +0200
+++ b/src/Pure/ROOT	Tue May 14 21:56:19 2013 +0200
@@ -160,7 +160,6 @@
     "Proof/proof_rewrite_rules.ML"
     "Proof/proof_syntax.ML"
     "Proof/reconstruct.ML"
-    "ProofGeneral/pgip_types.ML"
     "ProofGeneral/preferences.ML"
     "ProofGeneral/proof_general_emacs.ML"
     "ProofGeneral/proof_general_pgip.ML"

--- a/src/Pure/ROOT.ML	Tue May 14 21:40:25 2013 +0200
+++ b/src/Pure/ROOT.ML	Tue May 14 21:56:19 2013 +0200
@@ -298,8 +298,6 @@
 
 (* configuration for Proof General *)
 
-use "ProofGeneral/pgip_types.ML";
-
 (use
   |> Unsynchronized.setmp Proofterm.proofs 0
   |> Unsynchronized.setmp Multithreading.max_threads 0)