src/Pure/PIDE/markup.scala

--- a/src/Pure/PIDE/markup.scala	Fri Aug 07 15:13:50 2020 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Aug 07 20:19:49 2020 +0200
@@ -569,13 +569,22 @@
 
   class Name_Function(name: String) extends Function(name)
   {
-    def unapply(props: Properties.T): Option[(String)] =
+    def unapply(props: Properties.T): Option[String] =
       props match {
         case List(PROPERTY, (NAME, a)) => Some(a)
         case _ => None
       }
   }
 
+  object ML_Pid extends Function("ML_pid")
+  {
+    def unapply(props: Properties.T): Option[Long] =
+      props match {
+        case List(PROPERTY, (ID, Value.Long(pid))) => Some(pid)
+        case _ => None
+      }
+  }
+
   val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
 
   object Command_Timing extends Properties_Function("command_timing")