1.1 --- a/src/Pure/General/properties.ML	Thu Aug 28 00:33:07 2008 +0200
     1.2 +++ b/src/Pure/General/properties.ML	Thu Aug 28 00:33:08 2008 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    type T = property list
     1.5    val defined: T -> string -> bool
     1.6    val get: T -> string -> string option
     1.7 +  val get_int: T -> string -> int option
     1.8    val put: string * string -> T -> T
     1.9    val remove: string -> T -> T
    1.10  end;
    1.11 @@ -22,7 +23,10 @@
    1.12  type T = property list;
    1.13  
    1.14  fun defined (props: T) name = AList.defined (op =) props name;
    1.15 +
    1.16  fun get (props: T) name = AList.lookup (op =) props name;
    1.17 +fun get_int props name = (case get props name of NONE => NONE | SOME s => Int.fromString s);
    1.18 +
    1.19  fun put prop (props: T) = AList.update (op =) prop props;
    1.20  fun remove name (props: T) = AList.delete (op =) name props;
    1.21