src/Pure/PIDE/markup.ML
changeset 51990 cc66addbba6d
parent 51988 a9725750c53a
child 52111 1fd184eaa310
     1.1 --- a/src/Pure/PIDE/markup.ML	Tue May 14 20:32:10 2013 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Tue May 14 20:46:09 2013 +0200
     1.3 @@ -185,7 +185,12 @@
     1.4      SOME x => x
     1.5    | NONE => raise Fail ("Bad real: " ^ quote s));
     1.6  
     1.7 -val print_real = smart_string_of_real;
     1.8 +fun print_real x =
     1.9 +  let val s = signed_string_of_real x in
    1.10 +    (case space_explode "." s of
    1.11 +      [a, b] => if forall_string (fn c => c = "0") b then a else s
    1.12 +    | _ => s)
    1.13 +  end;
    1.14  
    1.15  
    1.16  (* basic markup *)