tuned --- avoid warnings in scala3;
authorwenzelm
Sat, 09 Apr 2022 14:51:54 +0200
changeset 75435 c8087e6bd2ce
parent 75434 f6ee58333aa5
child 75436 40630fec3b5d
tuned --- avoid warnings in scala3;
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
     }
   }