diff -r 850ba6d47300 -r 319dd5c618a5 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Tue Sep 29 12:12:34 2020 +0200 +++ b/src/Pure/PIDE/markup.scala Tue Sep 29 13:19:34 2020 +0200 @@ -605,9 +605,10 @@ object Invoke_Scala extends Function("invoke_scala") { - def unapply(props: Properties.T): Option[(String, String)] = + def unapply(props: Properties.T): Option[(String, String, Boolean)] = props match { - case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id)) + case List(PROPERTY, (NAME, name), (ID, id), ("thread", Value.Boolean(thread))) => + Some((name, id, thread)) case _ => None } }