src/Tools/Metis/src/PortableMosml.sml

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Metis/src/PortableMosml.sml	Wed Jun 20 22:07:52 2007 +0200
@@ -0,0 +1,48 @@
+(* ========================================================================= *)
+(* MOSCOW ML SPECIFIC FUNCTIONS                                              *)
+(* Copyright (c) 2002-2004 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+structure Portable :> Portable =
+struct
+
+(* ------------------------------------------------------------------------- *)
+(* The ML implementation.                                                    *)
+(* ------------------------------------------------------------------------- *)
+
+val ml = "mosml";
+
+(* ------------------------------------------------------------------------- *)
+(* Pointer equality using the run-time system.                               *)
+(* ------------------------------------------------------------------------- *)
+
+local val address : 'a -> int = Obj.magic
+in fun pointerEqual (x : 'a, y : 'a) = address x = address y
+end;
+
+(* ------------------------------------------------------------------------- *)
+(* Timing function applications a la Mosml.time.                             *)
+(* ------------------------------------------------------------------------- *)
+
+val time = Mosml.time;
+
+end
+
+(* ------------------------------------------------------------------------- *)
+(* Ensuring that interruptions (SIGINTs) are actually seen by the            *)
+(* linked executable as Interrupt exceptions.                                *)
+(* ------------------------------------------------------------------------- *)
+
+prim_val catch_interrupt : bool -> unit = 1 "sys_catch_break";
+val _ = catch_interrupt true;
+
+(* ------------------------------------------------------------------------- *)
+(* Ad-hoc upgrading of the Moscow ML basis library.                          *)
+(* ------------------------------------------------------------------------- *)
+
+fun TextIO_inputLine h =
+    let
+      open TextIO
+    in
+      case inputLine h of "" => NONE | s => SOME s
+    end;