--- a/src/Pure/ProofGeneral/pgip_types.ML Tue Jan 11 21:52:10 2011 +0100
+++ b/src/Pure/ProofGeneral/pgip_types.ML Wed Jan 12 14:07:29 2011 +0100
@@ -220,7 +220,8 @@
val int_to_pgstring = signed_string_of_int
-val real_to_pgstring = signed_string_of_real
+val real_to_pgstring = smart_string_of_real;
+
fun string_to_pgstring s = XML.text s
--- a/src/Pure/library.ML Tue Jan 11 21:52:10 2011 +0100
+++ b/src/Pure/library.ML Wed Jan 12 14:07:29 2011 +0100
@@ -129,10 +129,6 @@
val read_int: string list -> int * string list
val oct_char: string -> string
- (*reals*)
- val string_of_real: real -> string
- val signed_string_of_real: real -> string
-
(*strings*)
val nth_string: string -> int -> string
val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
@@ -157,6 +153,11 @@
val translate_string: (string -> string) -> string -> string
val match_string: string -> string -> bool
+ (*reals*)
+ val string_of_real: real -> string
+ val signed_string_of_real: real -> string
+ val smart_string_of_real: real -> string
+
(*lists as sets -- see also Pure/General/ord_list.ML*)
val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
@@ -682,15 +683,6 @@
-(** reals **)
-
-val string_of_real = Real.fmt (StringCvt.GEN NONE);
-
-fun signed_string_of_real x =
- if x < 0.0 then "-" ^ string_of_real (~ x) else string_of_real x;
-
-
-
(** strings **)
(* functions tuned for strings, avoiding explode *)
@@ -783,6 +775,23 @@
in match (space_explode "*" pat) str end;
+(** reals **)
+
+val string_of_real = Real.fmt (StringCvt.GEN NONE);
+
+fun signed_string_of_real x =
+ if x < 0.0 then "-" ^ string_of_real (~ x) else string_of_real x;
+
+fun smart_string_of_real x =
+ let
+ val s = signed_string_of_real x;
+ in
+ (case space_explode "." s of
+ [a, b] => if forall_string (fn c => c = "0") b then a else s
+ | _ => s)
+ end;
+
+
(** lists as sets -- see also Pure/General/ord_list.ML **)