author | wenzelm |
Sun, 13 Dec 2020 23:06:33 +0100 | |
changeset 72906 | 00399e5a6e50 |
parent 72905 | 82570cae3cc2 |
child 72907 | 3883f536d84d |
--- a/src/Pure/PIDE/rendering.scala Sun Dec 13 22:54:27 2020 +0100 +++ b/src/Pure/PIDE/rendering.scala Sun Dec 13 23:06:33 2020 +0100 @@ -436,7 +436,7 @@ for { Text.Info(r, result) <- snapshot.cumulate[(List[Markup], Option[Rendering.Color.Value])]( - range, (List(Markup.Empty), None), Rendering.background_elements, + range, (List(Markup.Empty), None), elements, command_states => { case (((markups, color), Text.Info(_, XML.Elem(markup, _))))