# HG changeset patch # User wenzelm # Date 1467964253 -7200 # Node ID 88d62f8b5f6e0b2e9ce4d609331de6fcb182ea42 # Parent 2e4de628201fae69764a2a0cc0ed07b065f139d5 tuned; diff -r 2e4de628201f -r 88d62f8b5f6e src/Tools/jEdit/src/text_structure.scala --- a/src/Tools/jEdit/src/text_structure.scala Fri Jul 08 09:47:51 2016 +0200 +++ b/src/Tools/jEdit/src/text_structure.scala Fri Jul 08 09:50:53 2016 +0200 @@ -27,7 +27,7 @@ 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]] = + def reverse_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) } @@ -92,8 +92,8 @@ def caret_iterator(): Iterator[Text.Info[Token]] = nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret)) - def rev_caret_iterator(): Iterator[Text.Info[Token]] = - nav.rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret)) + def reverse_caret_iterator(): Iterator[Text.Info[Token]] = + nav.reverse_iterator(caret_line).dropWhile(info => !info.range.touches(caret)) nav.iterator(caret_line, 1).find(info => info.range.touches(caret)) match { @@ -118,7 +118,7 @@ caret_iterator()) case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed_global) => - rev_caret_iterator().find(info => keywords.is_command(info.info, Keyword.theory)) + reverse_caret_iterator().find(info => keywords.is_command(info.info, Keyword.theory)) match { case Some(Text.Info(range2, tok)) if keywords.is_command(tok, Keyword.theory_goal) => Some((range1, range2)) @@ -136,16 +136,16 @@ keywords.is_command(t, Keyword.diag) || keywords.is_command(t, Keyword.proof) || keywords.is_command(t, Keyword.theory_goal), - rev_caret_iterator()) + reverse_caret_iterator()) case Some(Text.Info(range1, tok)) if tok.is_begin => find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator()) case Some(Text.Info(range1, tok)) if tok.is_end => - find_block(_.is_end, _.is_begin, _ => false, _ => true, rev_caret_iterator()) + find_block(_.is_end, _.is_begin, _ => false, _ => true, reverse_caret_iterator()) match { case Some((_, range2)) => - rev_caret_iterator(). + reverse_caret_iterator(). dropWhile(info => info.range != range2). dropWhile(info => info.range == range2). find(info => info.info.is_command || info.info.is_begin)