src/Pure/library.ML
changeset 41516 3a70387b5e01
parent 41494 364f672d8827
child 42403 38b29c9fc742
     1.1 --- a/src/Pure/library.ML	Tue Jan 11 21:52:10 2011 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Jan 12 14:07:29 2011 +0100
     1.3 @@ -129,10 +129,6 @@
     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 @@ -157,6 +153,11 @@
    1.15    val translate_string: (string -> string) -> string -> string
    1.16    val match_string: string -> string -> bool
    1.17  
    1.18 +  (*reals*)
    1.19 +  val string_of_real: real -> string
    1.20 +  val signed_string_of_real: real -> string
    1.21 +  val smart_string_of_real: real -> string
    1.22 +
    1.23    (*lists as sets -- see also Pure/General/ord_list.ML*)
    1.24    val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
    1.25    val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
    1.26 @@ -682,15 +683,6 @@
    1.27  
    1.28  
    1.29  
    1.30 -(** reals **)
    1.31 -
    1.32 -val string_of_real = Real.fmt (StringCvt.GEN NONE);
    1.33 -
    1.34 -fun signed_string_of_real x =
    1.35 -  if x < 0.0 then "-" ^ string_of_real (~ x) else string_of_real x;
    1.36 -
    1.37 -
    1.38 -
    1.39  (** strings **)
    1.40  
    1.41  (* functions tuned for strings, avoiding explode *)
    1.42 @@ -783,6 +775,23 @@
    1.43    in match (space_explode "*" pat) str end;
    1.44  
    1.45  
    1.46 +(** reals **)
    1.47 +
    1.48 +val string_of_real = Real.fmt (StringCvt.GEN NONE);
    1.49 +
    1.50 +fun signed_string_of_real x =
    1.51 +  if x < 0.0 then "-" ^ string_of_real (~ x) else string_of_real x;
    1.52 +
    1.53 +fun smart_string_of_real x =
    1.54 +  let
    1.55 +    val s = signed_string_of_real x;
    1.56 +  in
    1.57 +    (case space_explode "." s of
    1.58 +      [a, b] => if forall_string (fn c => c = "0") b then a else s
    1.59 +    | _ => s)
    1.60 +  end;
    1.61 +
    1.62 +
    1.63  
    1.64  (** lists as sets -- see also Pure/General/ord_list.ML **)
    1.65