--- a/src/Pure/PIDE/session.scala Sat Oct 29 21:36:33 2022 +0200
+++ b/src/Pure/PIDE/session.scala Mon Oct 31 11:04:54 2022 +0100
@@ -487,7 +487,7 @@
try { global_state.change(_.begin_theory(node_name, id, msg.text, blobs_info)) }
catch { case _: Document.State.Fail => bad_output() }
- case List(Markup.Commands_Accepted.PROPERTY) =>
+ case List(Markup.Commands_Accepted.THIS) =>
msg.text match {
case Protocol.Commands_Accepted(ids) =>
ids.foreach(id =>
@@ -495,7 +495,7 @@
case _ => bad_output()
}
- case List(Markup.Assign_Update.PROPERTY) =>
+ case List(Markup.Assign_Update.THIS) =>
msg.text match {
case Protocol.Assign_Update(id, edited, update) =>
try {
@@ -509,7 +509,7 @@
}
delay_prune.invoke()
- case List(Markup.Removed_Versions.PROPERTY) =>
+ case List(Markup.Removed_Versions.THIS) =>
msg.text match {
case Protocol.Removed(removed) =>
try {