tuned signature;

--- a/src/Tools/jEdit/src/isabelle.scala	Fri Jun 23 22:07:12 2017 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Jun 23 22:21:11 2017 +0200
@@ -257,15 +257,15 @@
 
     if (text_area.isEditable && indent_enabled(buffer, "jedit_indent_input")) {
       buffer_syntax(buffer) match {
-        case Some(syntax) if buffer.isInstanceOf[Buffer] =>
-          val nav = new Text_Structure.Navigator(syntax, buffer.asInstanceOf[Buffer], true)
+        case Some(syntax) =>
+          val nav = new Text_Structure.Navigator(syntax, buffer, true)
           nav.iterator(line, 1).toStream.headOption match {
             case Some(Text.Info(range, tok))
             if range.stop == caret && syntax.keywords.is_indent_command(tok) =>
               buffer.indentLine(line, true)
             case _ =>
           }
-        case _ =>
+        case None =>
       }
     }
   }

--- a/src/Tools/jEdit/src/text_structure.scala	Fri Jun 23 22:07:12 2017 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Fri Jun 23 22:21:11 2017 +0200
@@ -19,7 +19,7 @@
 {
   /* token navigator */
 
-  class Navigator(syntax: Outer_Syntax, buffer: Buffer, comments: Boolean)
+  class Navigator(syntax: Outer_Syntax, buffer: JEditBuffer, comments: Boolean)
   {
     val limit = PIDE.options.value.int("jedit_structure_limit") max 0
 
@@ -48,9 +48,9 @@
       actions: java.util.List[IndentAction])
     {
       Isabelle.buffer_syntax(buffer) match {
-        case Some(syntax) if buffer.isInstanceOf[Buffer] =>
+        case Some(syntax) =>
           val keywords = syntax.keywords
-          val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], true)
+          val nav = new Navigator(syntax, buffer, true)
 
           val indent_size = buffer.getIndentSize
 
@@ -184,7 +184,7 @@
 
           actions.clear()
           actions.add(new IndentAction.AlignOffset(indent max 0))
-        case _ =>
+        case None =>
       }
     }
   }
@@ -238,10 +238,10 @@
       val caret = text_area.getCaretPosition
 
       Isabelle.buffer_syntax(text_area.getBuffer) match {
-        case Some(syntax) if buffer.isInstanceOf[Buffer] =>
+        case Some(syntax) =>
           val keywords = syntax.keywords
 
-          val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], false)
+          val nav = new Navigator(syntax, buffer, false)
 
           def caret_iterator(): Iterator[Text.Info[Token]] =
             nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret))
@@ -314,7 +314,7 @@
 
             case _ => None
           }
-        case _ => None
+        case None => None
       }
     }