# HG changeset patch
# User aspinall
# Date 1169115409 -3600
# Node ID 4bfd987b005c7bec05f8066b0e0b370064ca784d
# Parent  b1be13d32efd0575f67a11251042ebef1b5eaee9
Fix pgmlsymbolsoff

diff -r b1be13d32efd -r 4bfd987b005c src/Pure/ProofGeneral/pgip_input.ML
--- a/src/Pure/ProofGeneral/pgip_input.ML	Wed Jan 17 19:29:55 2007 +0100
+++ b/src/Pure/ProofGeneral/pgip_input.ML	Thu Jan 18 11:16:49 2007 +0100
@@ -177,6 +177,7 @@
    | "startquiet"     => Startquiet { }
    | "stopquiet"      => Stopquiet { }
    | "pgmlsymbolson"  => Pgmlsymbolson { }
+   | "pgmlsymbolsoff" => Pgmlsymbolsoff { }
    (* improperproofcmd: improper commands not in script *)
    | "dostep"         => Dostep    { text = xmltext data }
    | "undostep"       => Undostep  { times = times_attr attrs }
diff -r b1be13d32efd -r 4bfd987b005c src/Pure/ProofGeneral/pgip_tests.ML
--- a/src/Pure/ProofGeneral/pgip_tests.ML	Wed Jan 17 19:29:55 2007 +0100
+++ b/src/Pure/ProofGeneral/pgip_tests.ML	Thu Jan 18 11:16:49 2007 +0100
@@ -78,6 +78,10 @@
 val _ = asseqi "<askpgip/>" (SOME (Askpgip()));
 val _ = asseqi "<askpgml/>" (SOME (Askpgml()));
 val _ = asseqi "<askconfig/>" (SOME (Askconfig()));
+val _ = asseqi "<pgmlsymbolson/>" (SOME (Pgmlsymbolson()));
+val _ = asseqi "<pgmlsymbolsoff/>" (SOME (Pgmlsymbolsoff()));
+val _ = asseqi "<startquiet/>" (SOME (Startquiet()));
+val _ = asseqi "<stopquiet/>" (SOME (Stopquiet()));
 val _ = asseqi "<otherelt/>" NONE;
 
 end