# HG changeset patch
# User wenzelm
# Date 1498248432 -7200
# Node ID 1a4b6ae5e72bb5e98a36b54a9f8e71596210fcea
# Parent  33d7519fc35d38b6abf5266a22973deb918d4eb6
tuned;

diff -r 33d7519fc35d -r 1a4b6ae5e72b src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Fri Jun 23 22:04:14 2017 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Jun 23 22:07:12 2017 +0200
@@ -275,15 +275,16 @@
     if (!text_area.isEditable()) text_area.getToolkit().beep()
     else {
       val buffer = text_area.getBuffer
+      val line = text_area.getCaretLine
+      val caret = text_area.getCaretPosition
+
       def nl { text_area.userInput('\n') }
 
       if (indent_enabled(buffer, "jedit_indent_newline")) {
         buffer_syntax(buffer) match {
-          case Some(syntax) if buffer.isInstanceOf[Buffer] =>
+          case Some(syntax) =>
             val keywords = syntax.keywords
 
-            val line = text_area.getCaretLine
-            val caret = text_area.getCaretPosition
             val (toks1, toks2) = Text_Structure.split_line_content(buffer, keywords, line, caret)
 
             if (toks1.isEmpty) buffer.removeTrailingWhiteSpace(Array(line))
@@ -295,7 +296,7 @@
                 if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)
               }
             else nl
-          case _ => nl
+          case None => nl
         }
       }
       else nl