# HG changeset patch
# User aspinall
# Date 1182345034 -7200
# Node ID 343e84195e2cbf4b3718626da8515358cb13ce76
# Parent  061f288540171d3c2379562486596ecb2ad41438
Remove dedicated flag setting elements in favour of setproverflag.

diff -r 061f28854017 -r 343e84195e2c src/Pure/ProofGeneral/pgip_input.ML
--- a/src/Pure/ProofGeneral/pgip_input.ML	Wed Jun 20 15:10:02 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_input.ML	Wed Jun 20 15:10:34 2007 +0200
@@ -19,10 +19,6 @@
     (* prover control *)
     | Proverinit     of { }
     | Proverexit     of { }
-    | Startquiet     of { }
-    | Stopquiet      of { } 
-    | Pgmlsymbolson  of { } 
-    | Pgmlsymbolsoff of { }
     | Setproverflag  of { flagname:string, value: bool }
     (* improper proof commands: control proof state *)
     | Dostep         of { text: string }
@@ -88,10 +84,6 @@
        (* prover control *)
        | Proverinit 	of { }
        | Proverexit 	of { }
-       | Startquiet 	of { }
-       | Stopquiet	of { } 
-       | Pgmlsymbolson  of { } 
-       | Pgmlsymbolsoff of { }
        | Setproverflag  of { flagname:string, value: bool }
        (* improper proof commands: control proof state *)
        | Dostep		of { text: string }
@@ -186,10 +178,6 @@
    (* provercontrol *)
    | "proverinit"     => Proverinit { }
    | "proverexit"     => Proverexit { }
-   | "startquiet"     => Startquiet { }
-   | "stopquiet"      => Stopquiet { }
-   | "pgmlsymbolson"  => Pgmlsymbolson { }
-   | "pgmlsymbolsoff" => Pgmlsymbolsoff { }
    | "setproverflag"  => Setproverflag { flagname = flagname_attr attrs,
 					 value = read_pgipbool (value_attr attrs) }
    (* improperproofcmd: improper commands not in script *)
diff -r 061f28854017 -r 343e84195e2c src/Pure/ProofGeneral/pgip_tests.ML
--- a/src/Pure/ProofGeneral/pgip_tests.ML	Wed Jun 20 15:10:02 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_tests.ML	Wed Jun 20 15:10:34 2007 +0200
@@ -80,10 +80,12 @@
 val _ = asseqi "<askpgip/>" (SOME (Askpgip()));
 val _ = asseqi "<askpgml/>" (SOME (Askpgml()));
 val _ = asseqi "<askconfig/>" (SOME (Askconfig()));
+(* FIXME: new tests:
 val _ = asseqi "<pgmlsymbolson/>" (SOME (Pgmlsymbolson()));
 val _ = asseqi "<pgmlsymbolsoff/>" (SOME (Pgmlsymbolsoff()));
 val _ = asseqi "<startquiet/>" (SOME (Startquiet()));
 val _ = asseqi "<stopquiet/>" (SOME (Stopquiet()));
+*)
 val _ = asseqi "<askrefs thyname='foo' objtype='theory'/>" (SOME (Askrefs {url=NONE, thyname=SOME "foo",
 									  objtype=SOME ObjTheory,name=NONE}));
 val _ = asseqi "<otherelt/>" NONE;