Remove dedicated flag setting elements in favour of setproverflag.
--- 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 *)
--- 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;