clarified conditional ML;
authorwenzelm
Fri, 16 Apr 2021 23:35:20 +0200
changeset 73843 d1767bcb79ec
parent 73842 76d0b6597c91
child 73844 a96de8bbe8a3
clarified conditional ML;
src/Pure/ML/ml_pid.ML
src/Pure/ROOT.ML
--- a/src/Pure/ML/ml_pid.ML	Fri Apr 16 23:16:00 2021 +0200
+++ b/src/Pure/ML/ml_pid.ML	Fri Apr 16 23:35:20 2021 +0200
@@ -9,23 +9,17 @@
   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);
+\<^if_windows>\<open>
+  val get =
+    Foreign.buildCall0
+      (Foreign.getSymbol (Foreign.loadLibrary "kernel32.dll") "GetCurrentProcessId", (), Foreign.cInt);
+\<close>
+
+\<^if_unix>\<open>
+  val get = Posix.ProcEnv.getpid #> Posix.Process.pidToWord #> SysWord.toLargeInt;
+\<close>
 
 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	Fri Apr 16 23:16:00 2021 +0200
+++ b/src/Pure/ROOT.ML	Fri Apr 16 23:35:20 2021 +0200
@@ -238,7 +238,6 @@
 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";
@@ -302,6 +301,7 @@
 ML_file "Thy/term_style.ML";
 ML_file "Isar/outer_syntax.ML";
 ML_file "ML/ml_antiquotations.ML";
+ML_file "ML/ml_pid.ML";
 ML_file "Thy/document_antiquotation.ML";
 ML_file "Thy/thy_output.ML";
 ML_file "Thy/document_antiquotations.ML";