# HG changeset patch
# User wenzelm
# Date 1594931043 -7200
# Node ID 912f13865596193883107186b4427028bb781916
# Parent  438adb97d82c29cf706134d92174a7085b16c07b
support native PID for ML process;

diff -r 438adb97d82c -r 912f13865596 src/Pure/ML/ml_pid.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_pid.ML	Thu Jul 16 22:24:03 2020 +0200
@@ -0,0 +1,31 @@
+(*  Title:      Pure/ML/ml_pid.ML
+    Author:     Makarius
+
+Native PID for ML process.
+*)
+
+signature ML_PID =
+sig
+  val get: unit -> int
+end;
+
+if ML_System.platform_is_windows then ML
+\<open>
+structure ML_PID: ML_PID =
+struct
+
+val get =
+  Foreign.buildCall0
+    (Foreign.getSymbol (Foreign.loadLibrary "kernel32.dll") "GetCurrentProcessId", (), Foreign.cInt);
+
+end;
+\<close>
+else ML
+\<open>
+structure ML_PID: ML_PID =
+struct
+
+val get = Posix.ProcEnv.getpid #> Posix.Process.pidToWord #> SysWord.toLargeInt
+
+end;
+\<close>
diff -r 438adb97d82c -r 912f13865596 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Jul 16 20:35:03 2020 +0200
+++ b/src/Pure/ROOT.ML	Thu Jul 16 22:24:03 2020 +0200
@@ -239,6 +239,7 @@
 ML_file "ML/ml_context.ML";
 ML_file "ML/ml_antiquotation.ML";
 ML_file "ML/ml_compiler2.ML";
+ML_file "ML/ml_pid.ML";
 
 
 section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup";