clarified: omit presumably pointless Markup.Serial (see also 0b9334adcf05);
authorwenzelm
Thu, 10 Dec 2020 16:47:06 +0100
changeset 72870 8c468d602db1
parent 72869 015a61936c13
child 72871 17533d0a11b8
clarified: omit presumably pointless Markup.Serial (see also 0b9334adcf05);
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)