# HG changeset patch
# User wenzelm
# Date 1649508714 -7200
# Node ID c8087e6bd2cef1a0fbe8efb480c7550d2c562be8
# Parent  f6ee58333aa5332efda3dd92d5cc36dac244d42c
tuned --- avoid warnings in scala3;

diff -r f6ee58333aa5 -r c8087e6bd2ce src/Tools/jEdit/src/jedit_bibtex.scala
--- a/src/Tools/jEdit/src/jedit_bibtex.scala	Sat Apr 09 14:29:34 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_bibtex.scala	Sat Apr 09 14:51:54 2022 +0200
@@ -26,24 +26,20 @@
 object JEdit_Bibtex {
   /** context menu **/
 
-  def context_menu(text_area0: JEditTextArea): List[JMenuItem] = {
-    text_area0 match {
-      case text_area: TextArea =>
-        text_area.getBuffer match {
-          case buffer: Buffer
-          if (Bibtex.is_bibtex(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
-            val menu = new JMenu("BibTeX entries")
-            for (entry <- Bibtex.known_entries) {
-              val item = new JMenuItem(entry.kind)
-              item.addActionListener(new ActionListener {
-                def actionPerformed(evt: ActionEvent): Unit =
-                  Isabelle.insert_line_padding(text_area, entry.template)
-              })
-              menu.add(item)
-            }
-            List(menu)
-          case _ => Nil
+  def context_menu(text_area: JEditTextArea): List[JMenuItem] = {
+    text_area.getBuffer match {
+      case buffer: Buffer
+      if Bibtex.is_bibtex(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable =>
+        val menu = new JMenu("BibTeX entries")
+        for (entry <- Bibtex.known_entries) {
+          val item = new JMenuItem(entry.kind)
+          item.addActionListener(new ActionListener {
+            def actionPerformed(evt: ActionEvent): Unit =
+              Isabelle.insert_line_padding(text_area, entry.template)
+          })
+          menu.add(item)
         }
+        List(menu)
       case _ => Nil
     }
   }