diff -r b04afc51914c -r ab2edd87b912 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Thu Jul 12 00:15:26 2007 +0200
+++ b/src/Pure/General/markup.ML	Thu Jul 12 00:15:28 2007 +0200
@@ -9,6 +9,8 @@
 sig
   type property = string * string
   type T = string * property list
+  val get_string: T -> string -> string option
+  val get_int: T -> string -> int option
   val none: T
   val properties: (string * string) list -> T -> T
   val nameN: string
@@ -68,16 +70,20 @@
 
 val none = ("", []);
 
+
 fun properties more_props ((elem, props): T) =
   (elem, fold_rev (AList.update (op =)) more_props props);
 
+fun get_string ((_, props): T) prop = AList.lookup (op =) props prop;
+fun get_int m prop = (case get_string m prop of NONE => NONE | SOME s => Int.fromString s);
+
+fun markup elem = (elem, (elem, []): T);
+fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
+fun markup_int elem prop = (elem, fn i => (elem, [(prop, Int.toString i)]): T);
+
 val nameN = "name";
 val kindN = "kind";
 
-fun markup elem = (elem, (elem, []): T);
-fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
-fun markup_int elem prop = (elem, fn i => (elem, [(prop, string_of_int i)]): T);
-
 
 (* position *)