# HG changeset patch
# User wenzelm
# Date 1294837649 -3600
# Node ID 3a70387b5e01143aa3a9f90b41e41d4743185f10
# Parent  2b456655b077ca256d738132de7457bc670a90af
smart_string_of_real: print integer values without fractional part;

diff -r 2b456655b077 -r 3a70387b5e01 src/Pure/ProofGeneral/pgip_types.ML
--- 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
 
diff -r 2b456655b077 -r 3a70387b5e01 src/Pure/library.ML
--- 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 **)