src/Pure/ProofGeneral/pgip_input.ML
changeset 21867 8750fbc28d5c
parent 21655 01b2d13153c8
child 21940 fbd068dd4d29
     1.1 --- a/src/Pure/ProofGeneral/pgip_input.ML	Sat Dec 16 20:27:56 2006 +0100
     1.2 +++ b/src/Pure/ProofGeneral/pgip_input.ML	Sun Dec 17 22:43:50 2006 +0100
     1.3 @@ -29,11 +29,15 @@
     1.4      | Redostep       of { }
     1.5      | Abortgoal      of { }
     1.6      | Forget         of { thyname: string option, name: string option, 
     1.7 -                          objtype: string option }
     1.8 +                          objtype: PgipTypes.objtype option }
     1.9      | Restoregoal    of { thmname : string }
    1.10      (* context inspection commands *)
    1.11 -    | Askids         of { thyname:string option, objtype:string option }
    1.12 -    | Showid         of { thyname:string option, objtype:string, name:string }
    1.13 +    | Askids         of { url: PgipTypes.pgipurl option,
    1.14 +			  thyname: PgipTypes.objname option,
    1.15 +			  objtype: PgipTypes.objtype option }
    1.16 +    | Showid         of { thyname: PgipTypes.objname option, 
    1.17 +			  objtype: PgipTypes.objtype, 
    1.18 +			  name: PgipTypes.objname }
    1.19      | Askguise       of { }
    1.20      | Parsescript    of { text: string, location: PgipTypes.location,
    1.21                            systemdata: string option } 
    1.22 @@ -89,11 +93,15 @@
    1.23         | Redostep	of { }
    1.24         | Abortgoal	of { }
    1.25         | Forget		of { thyname: string option, name: string option, 
    1.26 -			     objtype: string option }
    1.27 +			     objtype: PgipTypes.objtype option }
    1.28         | Restoregoal    of { thmname : string }
    1.29         (* context inspection commands *)
    1.30 -       | Askids		of { thyname:string option, objtype:string option }
    1.31 -       | Showid		of { thyname:string option, objtype:string, name:string }
    1.32 +       | Askids         of { url: PgipTypes.pgipurl option,
    1.33 +			     thyname: PgipTypes.objname option,
    1.34 +			     objtype: PgipTypes.objtype option }
    1.35 +       | Showid         of { thyname: PgipTypes.objname option, 
    1.36 +			     objtype: PgipTypes.objtype, 
    1.37 +			     name: PgipTypes.objname }
    1.38         | Askguise	of { }
    1.39         | Parsescript	of { text: string, location: location,
    1.40  			     systemdata: string option } 
    1.41 @@ -123,12 +131,18 @@
    1.42  
    1.43      val thyname_attro = get_attr_opt "thyname"
    1.44      val thyname_attr = get_attr "thyname"
    1.45 -    val objtype_attro = get_attr_opt "objtype"
    1.46 -    val objtype_attr = get_attr "objtype"
    1.47      val name_attr = get_attr "name"
    1.48      val name_attro = get_attr_opt "name"
    1.49      val thmname_attr = get_attr "thmname"
    1.50  
    1.51 +    fun objtype_attro attrs = if has_attr "objtype" attrs then
    1.52 +				  SOME (objtype_of_attrs attrs)
    1.53 +			      else NONE
    1.54 +
    1.55 +    fun pgipurl_attro attrs = if has_attr "url" attrs then
    1.56 +				  SOME (pgipurl_of_attrs attrs)
    1.57 +			      else NONE
    1.58 +
    1.59      val times_attr = read_pgipnat o (get_attr_dflt "times" "1")
    1.60      val prefcat_attr = get_attr_opt "prefcategory"
    1.61  
    1.62 @@ -173,10 +187,11 @@
    1.63  				  objtype = objtype_attro attrs }
    1.64     | "restoregoal"    => Restoregoal { thmname = thmname_attr attrs}
    1.65     (* proofctxt: improper commands *)
    1.66 -   | "askids"         => Askids { thyname = thyname_attro attrs, 
    1.67 +   | "askids"         => Askids { url = pgipurl_attro attrs,
    1.68 +				  thyname = thyname_attro attrs, 
    1.69  				  objtype = objtype_attro attrs }
    1.70     | "showid"         => Showid { thyname = thyname_attro attrs,
    1.71 -				  objtype = objtype_attr attrs,
    1.72 +				  objtype = objtype_of_attrs attrs,
    1.73  				  name = name_attr attrs }
    1.74     | "askguise"       => Askguise { }
    1.75     | "parsescript"    => Parsescript { text = (xmltext data),