changeset 51990 | cc66addbba6d |
parent 51988 | a9725750c53a |
child 52111 | 1fd184eaa310 |
--- 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 *)