--- a/src/Pure/PIDE/markup.scala Thu Mar 04 15:41:46 2021 +0100
+++ b/src/Pure/PIDE/markup.scala Thu Mar 04 15:49:15 2021 +0100
@@ -733,7 +733,7 @@
def update_properties(more_props: Properties.T): Markup =
if (more_props.isEmpty) this
- else Markup(name, (more_props :\ properties) { case (p, ps) => Properties.put(ps, p) })
+ else Markup(name, more_props.foldRight(properties) { case (p, ps) => Properties.put(ps, p) })
def + (entry: Properties.Entry): Markup =
Markup(name, Properties.put(properties, entry))