# HG changeset patch
# User wenzelm
# Date 1607615226 -3600
# Node ID 8c468d602db196ebf983dbafe6d46c5f29007411
# Parent  015a61936c1300b51b3ce30244b84e4b0ae4d740
clarified: omit presumably pointless Markup.Serial (see also 0b9334adcf05);

diff -r 015a61936c13 -r 8c468d602db1 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)