# HG changeset patch
# User wenzelm
# Date 1252800472 -7200
# Node ID e6b66a59bed6a8bbabf72facf75ec8de7e440aaa
# Parent  5047ab238cc05f873a6111843f3e210e4a93bbf8
wrapper for Real.fmt -- via StringCvt.realfmt;

diff -r 5047ab238cc0 -r e6b66a59bed6 src/Pure/ML-Systems/proper_int.ML
--- a/src/Pure/ML-Systems/proper_int.ML	Sun Sep 13 02:07:06 2009 +0200
+++ b/src/Pure/ML-Systems/proper_int.ML	Sun Sep 13 02:07:52 2009 +0200
@@ -136,6 +136,24 @@
 end;
 
 
+(* StringCvt *)
+
+structure StringCvt =
+struct
+  open StringCvt;
+  datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option
+  fun realfmt fmt = Real.fmt
+    (case fmt of
+      EXACT => StringCvt.EXACT
+    | FIX NONE => StringCvt.FIX NONE
+    | FIX (SOME b) => StringCvt.FIX (SOME (dest_int b))
+    | GEN NONE => StringCvt.GEN NONE
+    | GEN (SOME b) => StringCvt.GEN (SOME (dest_int b))
+    | SCI NONE => StringCvt.SCI NONE
+    | SCI (SOME b) => StringCvt.SCI (SOME (dest_int b)));
+end;
+
+
 (* Word *)
 
 structure Word =
@@ -165,6 +183,7 @@
   val trunc = mk_int o Real.trunc;
   fun toInt a b = mk_int (Real.toInt a b);
   fun fromInt a = Real.fromInt (dest_int a);
+  val fmt = StringCvt.realfmt;
 end;
 
 val ceil = Real.ceil;