# 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 =