# HG changeset patch
# User aspinall
# Date 1172922159 -3600
# Node ID a591df440b5b2bc039b4a72c1e9b346920b6f00a
# Parent  7eef90be0db4ab1170a635f4f7a1639def36701e
Add setproverflag, to replace other flag controls

diff -r 7eef90be0db4 -r a591df440b5b src/Pure/ProofGeneral/pgip_input.ML
--- a/src/Pure/ProofGeneral/pgip_input.ML	Sat Mar 03 12:42:04 2007 +0100
+++ b/src/Pure/ProofGeneral/pgip_input.ML	Sat Mar 03 12:42:39 2007 +0100
@@ -23,6 +23,7 @@
     | Stopquiet      of { } 
     | Pgmlsymbolson  of { } 
     | Pgmlsymbolsoff of { }
+    | Setproverflag  of { flagname:string, value: bool }
     (* improper proof commands: control proof state *)
     | Dostep         of { text: string }
     | Undostep       of { times: int }
@@ -91,6 +92,7 @@
        | Stopquiet	of { } 
        | Pgmlsymbolson  of { } 
        | Pgmlsymbolsoff of { }
+       | Setproverflag  of { flagname:string, value: bool }
        (* improper proof commands: control proof state *)
        | Dostep		of { text: string }
        | Undostep	of { times: int }
@@ -142,6 +144,8 @@
     val name_attr = get_attr "name"
     val name_attro = get_attr_opt "name"
     val thmname_attr = get_attr "thmname"
+    val flagname_attr = get_attr "flagname"
+    val value_attr = get_attr "value"
 
     fun objtype_attro attrs = if has_attr "objtype" attrs then
 				  SOME (objtype_of_attrs attrs)
@@ -186,6 +190,8 @@
    | "stopquiet"      => Stopquiet { }
    | "pgmlsymbolson"  => Pgmlsymbolson { }
    | "pgmlsymbolsoff" => Pgmlsymbolsoff { }
+   | "setproverflag"  => Setproverflag { flagname = flagname_attr attrs,
+					 value = read_pgipbool (value_attr attrs) }
    (* improperproofcmd: improper commands not in script *)
    | "dostep"         => Dostep    { text = xmltext data }
    | "undostep"       => Undostep  { times = times_attr attrs }