# HG changeset patch
# User wenzelm
# Date 1467921487 -7200
# Node ID 5a573668ceae139a6977abf23b6a2583f9cb6b98
# Parent  e4e15bbfb3e2b885108bc52568b602344180b3a3
tuned;

diff -r e4e15bbfb3e2 -r 5a573668ceae src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Thu Jul 07 21:34:56 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Thu Jul 07 21:58:07 2016 +0200
@@ -17,25 +17,38 @@
 
 object Text_Structure
 {
+  /* token navigator */
+
+  class Navigator(syntax: Outer_Syntax, buffer: Buffer)
+  {
+    val limit = PIDE.options.value.int("jedit_structure_limit") max 0
+
+    def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
+      Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).
+        filter(_.info.is_proper)
+
+    def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
+      Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim).
+        filter(_.info.is_proper)
+  }
+
+
   /* indentation */
 
   object Indent_Rule extends IndentRule
   {
-    def apply(buffer0: JEditBuffer, line: Int, prev_line: Int, prev_prev_line: Int,
+    def apply(buffer: JEditBuffer, line: Int, prev_line: Int, prev_prev_line: Int,
       actions: java.util.List[IndentAction])
     {
-      buffer0 match {
-        case buffer: Buffer =>
-          Isabelle.buffer_syntax(buffer) match {
-            case Some(syntax) =>
-              val limit = PIDE.options.value.int("jedit_structure_limit") max 0
+      Isabelle.buffer_syntax(buffer) match {
+        case Some(syntax) if buffer.isInstanceOf[Buffer] =>
+          val keywords = syntax.keywords
+          val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer])
 
-              val indent = 0  // FIXME
+          val indent = 0  // FIXME
 
-              actions.clear()
-              actions.add(new IndentAction.AlignOffset(indent))
-            case _ =>
-          }
+          actions.clear()
+          actions.add(new IndentAction.AlignOffset(indent))
         case _ =>
       }
     }
@@ -71,25 +84,18 @@
       val caret = text_area.getCaretPosition
 
       Isabelle.buffer_syntax(text_area.getBuffer) match {
-        case Some(syntax) =>
+        case Some(syntax) if buffer.isInstanceOf[Buffer] =>
           val keywords = syntax.keywords
-          val limit = PIDE.options.value.int("jedit_structure_limit") max 0
 
-          def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
-            Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).
-              filter(_.info.is_proper)
-
-          def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
-            Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim).
-              filter(_.info.is_proper)
+          val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer])
 
           def caret_iterator(): Iterator[Text.Info[Token]] =
-            iterator(caret_line).dropWhile(info => !info.range.touches(caret))
+            nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret))
 
           def rev_caret_iterator(): Iterator[Text.Info[Token]] =
-            rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret))
+            nav.rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret))
 
-          iterator(caret_line, 1).find(info => info.range.touches(caret))
+          nav.iterator(caret_line, 1).find(info => info.range.touches(caret))
           match {
             case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.theory_goal) =>
               find_block(
@@ -154,7 +160,7 @@
 
             case _ => None
           }
-        case None => None
+        case _ => None
       }
     }