src/Pure/library.ML
changeset 40291 012ed4426fda
parent 39811 0659e84bdc5f
child 40318 035b2afbeb2e
     1.1 --- a/src/Pure/library.ML	Sat Oct 30 15:26:40 2010 +0200
     1.2 +++ b/src/Pure/library.ML	Sat Oct 30 16:33:58 2010 +0200
     1.3 @@ -130,6 +130,10 @@
     1.4    val read_int: string list -> int * string list
     1.5    val oct_char: string -> string
     1.6  
     1.7 +  (*reals*)
     1.8 +  val string_of_real: real -> string
     1.9 +  val signed_string_of_real: real -> string
    1.10 +
    1.11    (*strings*)
    1.12    val nth_string: string -> int -> string
    1.13    val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
    1.14 @@ -668,6 +672,15 @@
    1.15  
    1.16  
    1.17  
    1.18 +(** reals **)
    1.19 +
    1.20 +val string_of_real = Real.fmt (StringCvt.GEN NONE);
    1.21 +
    1.22 +fun signed_string_of_real x =
    1.23 +  if x < 0.0 then "-" ^ string_of_real (~ x) else string_of_real x;
    1.24 +
    1.25 +
    1.26 +
    1.27  (** strings **)
    1.28  
    1.29  (* functions tuned for strings, avoiding explode *)