src/Tools/jEdit/src/jedit_rendering.scala

--- a/src/Tools/jEdit/src/jedit_rendering.scala	Thu Dec 10 16:35:56 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Thu Dec 10 16:47:06 2020 +0100
@@ -347,8 +347,7 @@
     val pris =
       snapshot.cumulate[Int](range, 0, JEdit_Rendering.gutter_elements, _ =>
         {
-          case (pri, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(serial)), _))) =>
-            Some(pri max gutter_message_pri(msg))
+          case (pri, Text.Info(_, elem)) => Some(pri max gutter_message_pri(elem))
           case _ => None
         }).map(_.info)