removed obsolete get_string;
authorwenzelm
Thu, 28 Aug 2008 00:33:07 +0200
changeset 2803100bf98c154fa
parent 28030 8b197e2bc66a
child 28032 cb0021c989cd
removed obsolete get_string;
moved get_int to property.ML;
src/Pure/General/markup.ML
     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);