more uniform Markup.print_real;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue May 14 20:32:10 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue May 14 20:46:09 2013 +0200
@@ -219,7 +219,7 @@
 
 fun encode_feature (name, weight) =
   encode_str name ^
-  (if Real.== (weight, 1.0) then "" else "=" ^ smart_string_of_real weight)
+  (if Real.== (weight, 1.0) then "" else "=" ^ Markup.print_real weight)
 
 val encode_features = map encode_feature #> space_implode " "
 

--- a/src/Pure/Concurrent/future.ML	Tue May 14 20:32:10 2013 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue May 14 20:46:09 2013 +0200
@@ -193,7 +193,7 @@
       val active = count_workers Working;
       val waiting = count_workers Waiting;
       val stats =
-       [("now", signed_string_of_real (Time.toReal (Time.now ()))),
+       [("now", Markup.print_real (Time.toReal (Time.now ()))),
         ("tasks_proof", Markup.print_int (! forked_proofs)),
         ("tasks_ready", Markup.print_int ready),
         ("tasks_pending", Markup.print_int pending),

--- a/src/Pure/Concurrent/task_queue.ML	Tue May 14 20:32:10 2013 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Tue May 14 20:46:09 2013 +0200
@@ -153,7 +153,7 @@
       (case timing of NONE => timing_start | SOME var => Synchronized.value var);
     fun micros time = string_of_int (Time.toNanoseconds time div 1000);
   in
-    [("now", signed_string_of_real (Time.toReal (Time.now ()))),
+    [("now", Markup.print_real (Time.toReal (Time.now ()))),
      ("task_name", name), ("task_id", Markup.print_int id),
      ("run", micros run), ("wait", micros wait), ("wait_deps", commas wait_deps)] @
     Position.properties_of pos

--- a/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Tue May 14 20:32:10 2013 +0200
+++ b/src/Pure/ML/ml_statistics_polyml-5.5.0.ML	Tue May 14 20:46:09 2013 +0200
@@ -51,8 +51,8 @@
      ("threads_wait_IO", Markup.print_int threadsWaitIO),
      ("threads_wait_mutex", Markup.print_int threadsWaitMutex),
      ("threads_wait_signal", Markup.print_int threadsWaitSignal),
-     ("time_CPU", signed_string_of_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
-     ("time_GC", signed_string_of_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
+     ("time_CPU", Markup.print_real (Time.toReal timeNonGCSystem + Time.toReal timeNonGCUser)),
+     ("time_GC", Markup.print_real (Time.toReal timeGCSystem + Time.toReal timeGCUser))] @
     user_counters
   end;
 

--- a/src/Pure/PIDE/markup.ML	Tue May 14 20:32:10 2013 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue May 14 20:46:09 2013 +0200
@@ -185,7 +185,12 @@
     SOME x => x
   | NONE => raise Fail ("Bad real: " ^ quote s));
 
-val print_real = smart_string_of_real;
+fun print_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;
 
 
 (* basic markup *)

--- a/src/Pure/ProofGeneral/pgip_types.ML	Tue May 14 20:32:10 2013 +0200
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Tue May 14 20:46:09 2013 +0200
@@ -92,7 +92,7 @@
 
 val int_to_pgstring = signed_string_of_int
 
-val real_to_pgstring = smart_string_of_real;
+val real_to_pgstring = Markup.print_real;
 
 
 fun string_to_pgstring s = XML.text s

--- a/src/Pure/System/options.ML	Tue May 14 20:32:10 2013 +0200
+++ b/src/Pure/System/options.ML	Tue May 14 20:46:09 2013 +0200
@@ -103,7 +103,7 @@
 
 val put_bool = put boolT Markup.print_bool;
 val put_int = put intT Markup.print_int;
-val put_real = put realT signed_string_of_real;
+val put_real = put realT Markup.print_real;
 val put_string = put stringT I;
 
 

--- a/src/Pure/config.ML	Tue May 14 20:32:10 2013 +0200
+++ b/src/Pure/config.ML	Tue May 14 20:46:09 2013 +0200
@@ -45,7 +45,7 @@
 fun print_value (Bool true) = "true"
   | print_value (Bool false) = "false"
   | print_value (Int i) = signed_string_of_int i
-  | print_value (Real x) = signed_string_of_real x
+  | print_value (Real x) = Markup.print_real x
   | print_value (String s) = quote s;
 
 fun print_type (Bool _) = "bool"

--- a/src/Pure/library.ML	Tue May 14 20:32:10 2013 +0200
+++ b/src/Pure/library.ML	Tue May 14 20:46:09 2013 +0200
@@ -157,7 +157,6 @@
   (*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
@@ -778,15 +777,6 @@
 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 **)