--- 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")];