added get_int;

--- a/src/Pure/General/properties.ML	Thu Aug 28 00:33:07 2008 +0200
+++ b/src/Pure/General/properties.ML	Thu Aug 28 00:33:08 2008 +0200
@@ -11,6 +11,7 @@
   type T = property list
   val defined: T -> string -> bool
   val get: T -> string -> string option
+  val get_int: T -> string -> int option
   val put: string * string -> T -> T
   val remove: string -> T -> T
 end;
@@ -22,7 +23,10 @@
 type T = property list;
 
 fun defined (props: T) name = AList.defined (op =) props name;
+
 fun get (props: T) name = AList.lookup (op =) props name;
+fun get_int props name = (case get props name of NONE => NONE | SOME s => Int.fromString s);
+
 fun put prop (props: T) = AList.update (op =) prop props;
 fun remove name (props: T) = AList.delete (op =) name props;