# HG changeset patch
# User wenzelm
# Date 1129030088 -7200
# Node ID 36b2978d339a6d1c880107fde89f2579d9fdb763
# Parent  4735c07399c88cb1a92443c77053e0d7a2749346
added string_of_pid;

diff -r 4735c07399c8 -r 36b2978d339a src/Pure/ML-Systems/mosml.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 =
diff -r 4735c07399c8 -r 36b2978d339a src/Pure/ML-Systems/polyml.ML
--- 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 =
diff -r 4735c07399c8 -r 36b2978d339a src/Pure/ML-Systems/poplogml.ML
--- 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 =
diff -r 4735c07399c8 -r 36b2978d339a src/Pure/ML-Systems/smlnj.ML
--- 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 =