tuned -- avoid warnings for scala3;

--- a/src/Pure/PIDE/rendering.scala	Fri Apr 08 15:49:33 2022 +0200
+++ b/src/Pure/PIDE/rendering.scala	Fri Apr 08 15:56:14 2022 +0200
@@ -563,7 +563,6 @@
             case (res, Text.Info(_, elem)) =>
               Command.State.get_result_proper(command_states, elem.markup.properties)
                 .map(res :+ _)
-            case _ => None
           })
 
     var seen_serials = Set.empty[Long]

--- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Apr 08 15:49:33 2022 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Apr 08 15:56:14 2022 +0200
@@ -143,8 +143,6 @@
 
             case (res, Text.Info(_, msg)) =>
               Command.State.get_result_proper(command_states, msg.markup.properties).map(res + _)
-
-            case _ => None
           }).filterNot(info => info.info.is_empty)
 
   def diagnostics_output(results: List[Text.Info[Command.Results]]): List[LSP.Diagnostic] = {

--- a/src/Tools/jEdit/src/jedit_rendering.scala	Fri Apr 08 15:49:33 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Fri Apr 08 15:56:14 2022 +0200
@@ -353,7 +353,6 @@
       snapshot.cumulate[Int](range, 0, JEdit_Rendering.gutter_elements, _ =>
         {
           case (pri, Text.Info(_, elem)) => Some(pri max gutter_message_pri(elem))
-          case _ => None
         }).map(_.info)
 
     gutter_message_content.get(pris.foldLeft(0)(_ max _))