# HG changeset patch # User wenzelm # Date 1498221512 -7200 # Node ID b51a40281016a2163796a9d3defaa85258d53944 # Parent 09fe6ae943312c22b70e8f348e4ee8c9ed9304e3 tuned signature; diff -r 09fe6ae94331 -r b51a40281016 src/Tools/jEdit/src/fold_handling.scala --- a/src/Tools/jEdit/src/fold_handling.scala Fri Jun 23 14:24:48 2017 +0200 +++ b/src/Tools/jEdit/src/fold_handling.scala Fri Jun 23 14:38:32 2017 +0200 @@ -29,16 +29,16 @@ } override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int = - Token_Markup.Line_Context.next(buffer, line).structure.depth max 0 + Token_Markup.Line_Context.after(buffer, line).structure.depth max 0 override def getPrecedingFoldLevels( buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] = { - val structure = Token_Markup.Line_Context.next(buffer, line).structure + val structure = Token_Markup.Line_Context.after(buffer, line).structure val result = if (line > 0 && structure.command) Range.inclusive(line - 1, 0, -1).iterator. - map(i => Token_Markup.Line_Context.next(buffer, i).structure). + map(i => Token_Markup.Line_Context.after(buffer, i).structure). takeWhile(_.improper).map(_ => structure.depth max 0).toList else Nil diff -r 09fe6ae94331 -r b51a40281016 src/Tools/jEdit/src/text_structure.scala --- a/src/Tools/jEdit/src/text_structure.scala Fri Jun 23 14:24:48 2017 +0200 +++ b/src/Tools/jEdit/src/text_structure.scala Fri Jun 23 14:38:32 2017 +0200 @@ -70,8 +70,8 @@ val prev_line: Int = Range.inclusive(current_line - 1, 0, -1).find(line => - Token_Markup.Line_Context.prev(buffer, line).get_context == Scan.Finished && - !Token_Markup.Line_Context.next(buffer, line).structure.improper) getOrElse -1 + Token_Markup.Line_Context.before(buffer, line).get_context == Scan.Finished && + !Token_Markup.Line_Context.after(buffer, line).structure.improper) getOrElse -1 def prev_line_command: Option[Token] = nav.reverse_iterator(prev_line, 1). @@ -140,7 +140,8 @@ else 0 val indent = - if (Token_Markup.Line_Context.prev(buffer, current_line).get_context == Scan.Finished) { + if (Token_Markup.Line_Context.before(buffer, current_line).get_context == Scan.Finished) + { line_head(current_line) match { case Some(info @ Text.Info(range, tok)) => if (tok.is_begin || @@ -199,7 +200,7 @@ : (List[Token], List[Token]) = { val line_range = JEdit_Lib.line_range(buffer, line) - val ctxt0 = Token_Markup.Line_Context.prev(buffer, line).get_context + val ctxt0 = Token_Markup.Line_Context.before(buffer, line).get_context val (toks1, ctxt1) = line_content(buffer, keywords, Text.Range(line_range.start, caret), ctxt0) val (toks2, _) = line_content(buffer, keywords, Text.Range(caret, line_range.stop), ctxt1) (toks1, toks2) diff -r 09fe6ae94331 -r b51a40281016 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Fri Jun 23 14:24:48 2017 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Fri Jun 23 14:38:32 2017 +0200 @@ -29,11 +29,11 @@ def init(mode: String): Line_Context = new Line_Context(mode, Some(Scan.Finished), Line_Structure.init) - def prev(buffer: JEditBuffer, line: Int): Line_Context = + def before(buffer: JEditBuffer, line: Int): Line_Context = if (line == 0) init(JEdit_Lib.buffer_mode(buffer)) - else next(buffer, line - 1) + else after(buffer, line - 1) - def next(buffer: JEditBuffer, line: Int): Line_Context = + def after(buffer: JEditBuffer, line: Int): Line_Context = { val line_mgr = JEdit_Lib.buffer_line_manager(buffer) def context = @@ -71,7 +71,7 @@ private def try_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int) : Option[List[Token]] = { - val line_context = Line_Context.prev(buffer, line) + val line_context = Line_Context.before(buffer, line) for { ctxt <- line_context.context text <- JEdit_Lib.try_get_text(buffer, JEdit_Lib.line_range(buffer, line))