author | wenzelm |
Thu, 10 Dec 2020 16:47:06 +0100 | |
changeset 72870 | 8c468d602db1 |
parent 72869 | 015a61936c13 |
child 72871 | 17533d0a11b8 |
--- 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)