src/Tools/jEdit/src/text_structure.scala

 
 object Text_Structure
 {
   /* 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
 
     def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
     {

 
     def apply(buffer: JEditBuffer, current_line: Int, prev_line0: Int, prev_prev_line0: Int,
       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
 
 
           def line_indent(line: Int): Int =

               }
             }
 
           actions.clear()
           actions.add(new IndentAction.AlignOffset(indent max 0))
-        case _ =>
+        case None =>
       }
     }
   }
 
   def line_content(buffer: JEditBuffer, keywords: Keyword.Keywords,

       val buffer = text_area.getBuffer
       val caret_line = text_area.getCaretLine
       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))
 
           def reverse_caret_iterator(): Iterator[Text.Info[Token]] =

                 case None => None
               }
 
             case _ => None
           }
-        case _ => None
+        case None => None
       }
     }
 
     def getMatch(text_area: TextArea): StructureMatcher.Match =
       find_pair(text_area) match {