Add setproverflag, to replace other flag controls
authoraspinall
Sat Mar 03 12:42:39 2007 +0100 (2007-03-03)
changeset 22406a591df440b5b
parent 22405 7eef90be0db4
child 22407 6e52564bcb53
Add setproverflag, to replace other flag controls
src/Pure/ProofGeneral/pgip_input.ML
     1.1 --- a/src/Pure/ProofGeneral/pgip_input.ML	Sat Mar 03 12:42:04 2007 +0100
     1.2 +++ b/src/Pure/ProofGeneral/pgip_input.ML	Sat Mar 03 12:42:39 2007 +0100
     1.3 @@ -23,6 +23,7 @@
     1.4      | Stopquiet      of { } 
     1.5      | Pgmlsymbolson  of { } 
     1.6      | Pgmlsymbolsoff of { }
     1.7 +    | Setproverflag  of { flagname:string, value: bool }
     1.8      (* improper proof commands: control proof state *)
     1.9      | Dostep         of { text: string }
    1.10      | Undostep       of { times: int }
    1.11 @@ -91,6 +92,7 @@
    1.12         | Stopquiet	of { } 
    1.13         | Pgmlsymbolson  of { } 
    1.14         | Pgmlsymbolsoff of { }
    1.15 +       | Setproverflag  of { flagname:string, value: bool }
    1.16         (* improper proof commands: control proof state *)
    1.17         | Dostep		of { text: string }
    1.18         | Undostep	of { times: int }
    1.19 @@ -142,6 +144,8 @@
    1.20      val name_attr = get_attr "name"
    1.21      val name_attro = get_attr_opt "name"
    1.22      val thmname_attr = get_attr "thmname"
    1.23 +    val flagname_attr = get_attr "flagname"
    1.24 +    val value_attr = get_attr "value"
    1.25  
    1.26      fun objtype_attro attrs = if has_attr "objtype" attrs then
    1.27  				  SOME (objtype_of_attrs attrs)
    1.28 @@ -186,6 +190,8 @@
    1.29     | "stopquiet"      => Stopquiet { }
    1.30     | "pgmlsymbolson"  => Pgmlsymbolson { }
    1.31     | "pgmlsymbolsoff" => Pgmlsymbolsoff { }
    1.32 +   | "setproverflag"  => Setproverflag { flagname = flagname_attr attrs,
    1.33 +					 value = read_pgipbool (value_attr attrs) }
    1.34     (* improperproofcmd: improper commands not in script *)
    1.35     | "dostep"         => Dostep    { text = xmltext data }
    1.36     | "undostep"       => Undostep  { times = times_attr attrs }