--- 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 }
--- 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