# HG changeset patch
# User wenzelm
# Date 1649426174 -7200
# Node ID be5aa2c9c9ad383ecb085cdaeb424de2a5cad752
# Parent  6e0a452dab7212d7e4cf491ceafda91c8bf8c879
tuned -- avoid warnings for scala3;

diff -r 6e0a452dab72 -r be5aa2c9c9ad src/Pure/PIDE/rendering.scala
--- 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]
diff -r 6e0a452dab72 -r be5aa2c9c9ad src/Tools/VSCode/src/vscode_rendering.scala
--- 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] = {
diff -r 6e0a452dab72 -r be5aa2c9c9ad src/Tools/jEdit/src/jedit_rendering.scala
--- 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 _))