tuned signature;

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

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

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