added string_of_pid;
authorwenzelm
Tue, 11 Oct 2005 13:28:08 +0200
changeset 17824 36b2978d339a
parent 17823 4735c07399c8
child 17825 ede984daba01
added string_of_pid;
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/poplogml.ML
src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/mosml.ML	Tue Oct 11 13:28:07 2005 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Tue Oct 11 13:28:08 2005 +0200
@@ -156,6 +156,9 @@
   if Process.system cmd = Process.success then 0 else 1;
 
 
+val string_of_pid = Int.toString;
+
+
 (* getenv *)
 
 fun getenv var =
--- a/src/Pure/ML-Systems/polyml.ML	Tue Oct 11 13:28:07 2005 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Oct 11 13:28:08 2005 +0200
@@ -178,6 +178,11 @@
   if OS.Process.isSuccess (OS.Process.system cmd) then 0 else 1;
 
 
+(*Convert a process ID to a decimal string (chiefly for tracing)*)
+fun string_of_pid pid = 
+    Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid));
+
+
 (* getenv *)
 
 fun getenv var =
--- a/src/Pure/ML-Systems/poplogml.ML	Tue Oct 11 13:28:07 2005 +0200
+++ b/src/Pure/ML-Systems/poplogml.ML	Tue Oct 11 13:28:08 2005 +0200
@@ -331,6 +331,8 @@
   let val (rc, result) = execute_result cmdline
   in TextIO.output (TextIO.stdOut, result); TextIO.flushOut TextIO.stdOut; rc end;
 
+val string_of_pid: int -> string = makestring;
+
 fun getenv var = (case OS.translate var of NONE => "" | SOME s => s);
 
 structure OS =
--- a/src/Pure/ML-Systems/smlnj.ML	Tue Oct 11 13:28:07 2005 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Tue Oct 11 13:28:08 2005 +0200
@@ -206,6 +206,11 @@
 val system = OS.Process.system: string -> int;
 
 
+(*Convert a process ID to a decimal string (chiefly for tracing)*)
+fun string_of_pid pid = 
+    Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord pid));
+
+
 (* getenv *)
 
 fun getenv var =