diff -r 700693cb96f1 -r cc66addbba6d src/Pure/PIDE/markup.ML
--- 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 *)