# HG changeset patch
# User wenzelm
# Date 1219876388 -7200
# Node ID cb0021c989cd872d7efc10f4ebf8dc3dd8c4cbe9
# Parent  00bf98c154fad03cf041e70978b09523844c7bde
added get_int;

diff -r 00bf98c154fa -r cb0021c989cd src/Pure/General/properties.ML
--- 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;