# HG changeset patch
# User wenzelm
# Date 1607897501 -3600
# Node ID 3883f536d84dfc2733256c08c5df4c90baf66842
# Parent  00399e5a6e50df7b8bec6e23a03302f9a82c4efd
unused (see 29566b6810f7);

diff -r 00399e5a6e50 -r 3883f536d84d src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sun Dec 13 23:06:33 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Sun Dec 13 23:11:41 2020 +0100
@@ -457,7 +457,7 @@
                     case _ => Rendering.Color.markdown_bullet4
                   }
                 Some((Nil, Some(color)))
-              case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
+              case (_, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
                 command_states.collectFirst(
                   { case st if st.results.defined(serial) => st.results.get(serial).get }) match
                 {