# HG changeset patch
# User wenzelm
# Date 1219876387 -7200
# Node ID 00bf98c154fad03cf041e70978b09523844c7bde
# Parent  8b197e2bc66a07b74084465830ad6a466e43ad95
removed obsolete get_string;
moved get_int to property.ML;

diff -r 8b197e2bc66a -r 00bf98c154fa src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Thu Aug 28 00:33:04 2008 +0200
+++ b/src/Pure/General/markup.ML	Thu Aug 28 00:33:07 2008 +0200
@@ -8,8 +8,6 @@
 signature MARKUP =
 sig
   type T = string * Properties.T
-  val get_string: T -> string -> string option
-  val get_int: T -> string -> int option
   val none: T
   val is_none: T -> bool
   val properties: (string * string) list -> T -> T
@@ -126,9 +124,6 @@
 fun properties more_props ((elem, props): T) =
   (elem, fold_rev Properties.put more_props props);
 
-fun get_string (_, props) = Properties.get props;
-fun get_int m prop = (case get_string m prop of NONE => NONE | SOME s => Int.fromString s);
-
 fun markup_elem 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);