src/Pure/ML/ml_pid.ML
author wenzelm
Thu, 23 Jan 2025 22:19:30 +0100
changeset 81960 326ecfc079a6
parent 73587 d1767bcb79ec
permissions -rw-r--r--
support for @{instantiate (no_beta) ...};
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
72052
912f13865596 support native PID for ML process;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML/ml_pid.ML
912f13865596 support native PID for ML process;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
912f13865596 support native PID for ML process;
wenzelm
parents:
diff changeset
     3
912f13865596 support native PID for ML process;
wenzelm
parents:
diff changeset
     4
Native PID for ML process.
912f13865596 support native PID for ML process;
wenzelm
parents:
diff changeset
     5
*)
912f13865596 support native PID for ML process;
wenzelm
parents:
diff changeset
     6
912f13865596 support native PID for ML process;
wenzelm
parents:
diff changeset
     7
signature ML_PID =
912f13865596 support native PID for ML process;
wenzelm
parents:
diff changeset
     8
sig
912f13865596 support native PID for ML process;
wenzelm
parents:
diff changeset
     9
  val get: unit -> int
912f13865596 support native PID for ML process;
wenzelm
parents:
diff changeset
    10
end;
912f13865596 support native PID for ML process;
wenzelm
parents:
diff changeset
    11
72114
d00220799735 tuned names;
wenzelm
parents: 72052
diff changeset
    12
structure ML_Pid: ML_PID =
72052
912f13865596 support native PID for ML process;
wenzelm
parents:
diff changeset
    13
struct
912f13865596 support native PID for ML process;
wenzelm
parents:
diff changeset
    14
73587
d1767bcb79ec clarified conditional ML;
wenzelm
parents: 72114
diff changeset
    15
\<^if_windows>\<open>
d1767bcb79ec clarified conditional ML;
wenzelm
parents: 72114
diff changeset
    16
  val get =
d1767bcb79ec clarified conditional ML;
wenzelm
parents: 72114
diff changeset
    17
    Foreign.buildCall0
d1767bcb79ec clarified conditional ML;
wenzelm
parents: 72114
diff changeset
    18
      (Foreign.getSymbol (Foreign.loadLibrary "kernel32.dll") "GetCurrentProcessId", (), Foreign.cInt);
d1767bcb79ec clarified conditional ML;
wenzelm
parents: 72114
diff changeset
    19
\<close>
d1767bcb79ec clarified conditional ML;
wenzelm
parents: 72114
diff changeset
    20
d1767bcb79ec clarified conditional ML;
wenzelm
parents: 72114
diff changeset
    21
\<^if_unix>\<open>
d1767bcb79ec clarified conditional ML;
wenzelm
parents: 72114
diff changeset
    22
  val get = Posix.ProcEnv.getpid #> Posix.Process.pidToWord #> SysWord.toLargeInt;
d1767bcb79ec clarified conditional ML;
wenzelm
parents: 72114
diff changeset
    23
\<close>
72052
912f13865596 support native PID for ML process;
wenzelm
parents:
diff changeset
    24
912f13865596 support native PID for ML process;
wenzelm
parents:
diff changeset
    25
end;