# HG changeset patch
# User wenzelm
# Date 1607960433 -3600
# Node ID cd6f6e2fe99dc6a7596cdf3145c96f4dd0b5a45e
# Parent  3883f536d84dfc2733256c08c5df4c90baf66842
tuned;

diff -r 3883f536d84d -r cd6f6e2fe99d src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sun Dec 13 23:11:41 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala	Mon Dec 14 16:40:33 2020 +0100
@@ -439,7 +439,7 @@
           range, (List(Markup.Empty), None), elements,
           command_states =>
             {
-              case (((markups, color), Text.Info(_, XML.Elem(markup, _))))
+              case ((markups, color), Text.Info(_, XML.Elem(markup, _)))
               if markups.nonEmpty && Document_Status.Command_Status.proper_elements(markup.name) =>
                 Some((markup :: markups, color))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
@@ -472,7 +472,7 @@
                 else None
             })
       color <-
-        (result match {
+        result match {
           case (markups, opt_color) if markups.nonEmpty =>
             val status = Document_Status.Command_Status.make(markups.iterator)
             if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
@@ -480,7 +480,7 @@
             else if (status.is_canceled) Some(Rendering.Color.canceled)
             else opt_color
           case (_, opt_color) => opt_color
-        })
+        }
     } yield Text.Info(r, color)
   }