--- 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
}
}