# HG changeset patch
# User wenzelm
# Date 1186151304 -7200
# Node ID c6402b61d44a9bd076530a699b8876541aa0522c
# Parent  ec51a0f7eefe157c64aad74a64f1d2e3bbe32694
preparations for proper type int;

diff -r ec51a0f7eefe -r c6402b61d44a src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Fri Aug 03 16:28:23 2007 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Fri Aug 03 16:28:24 2007 +0200
@@ -4,6 +4,10 @@
 Compatibility file for Standard ML of New Jersey 110 or later.
 *)
 
+fun mk_int (i: int) = i;
+fun dest_int (i: int) = i;
+(*use "ML-Systems/proper_int.ML";*)
+
 use "ML-Systems/exn.ML";
 use "ML-Systems/multithreading_dummy.ML";
 
@@ -18,8 +22,8 @@
 
 (* restore old-style character / string functions *)
 
-val ord     = SML90.ord;
-val chr     = SML90.chr;
+val ord     = mk_int o SML90.ord;
+val chr     = SML90.chr o dest_int;
 val explode = SML90.explode;
 val implode = SML90.implode;
 
@@ -40,8 +44,8 @@
 
 (*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
 fun print_depth n =
- (Control.Print.printDepth := n div 2;
-  Control.Print.printLength := n);
+ (Control.Print.printDepth := (dest_int n) div 2;
+  Control.Print.printLength := dest_int n);
 
 
 (* compiler-independent timing functions *)
@@ -92,8 +96,8 @@
 
     fun pp pps obj =
       pprint obj
-        (string pps, openHOVBox pps o Rel,
-          fn wd => break pps {nsp=wd, offset=0}, fn () => newline pps,
+        (string pps, openHOVBox pps o Rel o dest_int,
+          fn wd => break pps {nsp=dest_int wd, offset=0}, fn () => newline pps,
           fn () => closeBox pps);
   in (path, pp) end;
 
@@ -231,7 +235,7 @@
   end;
 
 (*plain version; with return code*)
-val system = OS.Process.system: string -> int;
+val system = mk_int o OS.Process.system;
 
 
 (*Convert a process ID to a decimal string (chiefly for tracing)*)