--- a/src/Pure/PIDE/markup.scala Fri Mar 12 23:30:35 2021 +0100
+++ b/src/Pure/PIDE/markup.scala Sat Mar 13 12:36:24 2021 +0100
@@ -636,10 +636,9 @@
object Invoke_Scala extends Function("invoke_scala")
{
- def unapply(props: Properties.T): Option[(String, String, Boolean)] =
+ def unapply(props: Properties.T): Option[(String, String)] =
props match {
- case List(PROPERTY, (NAME, name), (ID, id), ("thread", Value.Boolean(thread))) =>
- Some((name, id, thread))
+ case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id))
case _ => None
}
}