support native PID for ML process;
authorwenzelm
Thu, 16 Jul 2020 22:24:03 +0200
changeset 72282 912f13865596
parent 72281 438adb97d82c
child 72283 4ed33ea8d957
support native PID for ML process;
src/Pure/ML/ml_pid.ML
src/Pure/ROOT.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>
--- 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";