1.1 --- a/src/Pure/General/markup.ML Thu Aug 28 00:33:04 2008 +0200
1.2 +++ b/src/Pure/General/markup.ML Thu Aug 28 00:33:07 2008 +0200
1.3 @@ -8,8 +8,6 @@
1.4 signature MARKUP =
1.5 sig
1.6 type T = string * Properties.T
1.7 - val get_string: T -> string -> string option
1.8 - val get_int: T -> string -> int option
1.9 val none: T
1.10 val is_none: T -> bool
1.11 val properties: (string * string) list -> T -> T
1.12 @@ -126,9 +124,6 @@
1.13 fun properties more_props ((elem, props): T) =
1.14 (elem, fold_rev Properties.put more_props props);
1.15
1.16 -fun get_string (_, props) = Properties.get props;
1.17 -fun get_int m prop = (case get_string m prop of NONE => NONE | SOME s => Int.fromString s);
1.18 -
1.19 fun markup_elem elem = (elem, (elem, []): T);
1.20 fun markup_string elem prop = (elem, fn s => (elem, [(prop, s)]): T);
1.21 fun markup_int elem prop = (elem, fn i => (elem, [(prop, Int.toString i)]): T);