diff -r b9ded33bd58c -r 3546dd4ade74 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Aug 07 15:13:50 2020 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Aug 07 20:19:49 2020 +0200
@@ -209,6 +209,7 @@
   val dialogN: string val dialog: serial -> string -> T
   val jedit_actionN: string
   val functionN: string
+  val ml_pid: int -> Properties.T
   val commands_accepted: Properties.T
   val assign_update: Properties.T
   val removed_versions: Properties.T
@@ -672,6 +673,8 @@
 
 val functionN = "function"
 
+fun ml_pid pid = [(functionN, "ML_pid"), (idN, Value.print_int pid)];
+
 val commands_accepted = [(functionN, "commands_accepted")];
 
 val assign_update = [(functionN, "assign_update")];