tuned names;
authorwenzelm
Fri, 07 Aug 2020 21:02:02 +0200
changeset 72114 d00220799735
parent 72113 2d9e40cfe9af
child 72115 c998827f1df9
tuned names;
src/Pure/ML/ml_pid.ML
src/Pure/System/isabelle_process.ML
--- a/src/Pure/ML/ml_pid.ML	Fri Aug 07 20:28:53 2020 +0200
+++ b/src/Pure/ML/ml_pid.ML	Fri Aug 07 21:02:02 2020 +0200
@@ -11,7 +11,7 @@
 
 if ML_System.platform_is_windows then ML
 \<open>
-structure ML_PID: ML_PID =
+structure ML_Pid: ML_PID =
 struct
 
 val get =
@@ -22,7 +22,7 @@
 \<close>
 else ML
 \<open>
-structure ML_PID: ML_PID =
+structure ML_Pid: ML_PID =
 struct
 
 val get = Posix.ProcEnv.getpid #> Posix.Process.pidToWord #> SysWord.toLargeInt
--- a/src/Pure/System/isabelle_process.ML	Fri Aug 07 20:28:53 2020 +0200
+++ b/src/Pure/System/isabelle_process.ML	Fri Aug 07 21:02:02 2020 +0200
@@ -201,7 +201,7 @@
 
     fun protocol () =
      (Session.init_protocol_handlers ();
-      Output.protocol_message (Markup.ml_pid (ML_PID.get ())) [];
+      Output.protocol_message (Markup.ml_pid (ML_Pid.get ())) [];
       message Markup.initN [] [XML.Text (Session.welcome ())];
       protocol_loop ());