# HG changeset patch
# User wenzelm
# Date 1660382302 -7200
# Node ID 1c0407b900db73d309203fbb28078495123c1551
# Parent  96e66ba48052eb5e1bfbf9b912a4e80ef3a9cde7
tuned, following hints by IntelliJ IDEA;

diff -r 96e66ba48052 -r 1c0407b900db src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Fri Aug 12 20:21:09 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Sat Aug 13 11:18:22 2022 +0200
@@ -27,7 +27,7 @@
 object Isabelle {
   /* editor modes */
 
-  val modes =
+  val modes: List[String] =
     List(
       "isabelle",         // theory source
       "isabelle-ml",      // ML source
@@ -300,7 +300,7 @@
       val line = text_area.getCaretLine
       val caret = text_area.getCaretPosition
 
-      def nl: Unit = text_area.userInput('\n')
+      def nl(): Unit = text_area.userInput('\n')
 
       if (indent_enabled(buffer, "jedit_indent_newline")) {
         buffer_syntax(buffer) match {
@@ -316,11 +316,11 @@
               text_area.setSelectedText("\n")
               if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)
             }
-            else nl
-          case None => nl
+            else nl()
+          case None => nl()
         }
       }
-      else nl
+      else nl()
     }
   }
 
@@ -330,7 +330,7 @@
       val text1 =
         if (text_area.getSelectionCount == 0) {
           def pad(range: Text.Range): String =
-            if (JEdit_Lib.get_text(buffer, range) == Some("\n")) "" else "\n"
+            if (JEdit_Lib.get_text(buffer, range).contains("\n")) "" else "\n"
 
           val caret = JEdit_Lib.caret_range(text_area)
           val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)