# HG changeset patch
# User wenzelm
# Date 1468314727 -7200
# Node ID 08a1f61a49a6d79273338fd29bc94d823007e915
# Parent  932a3d4702641f66368884a7eb28359d60690081
tuned signature;

diff -r 932a3d470264 -r 08a1f61a49a6 src/Tools/jEdit/src/fold_handling.scala
--- a/src/Tools/jEdit/src/fold_handling.scala	Mon Jul 11 22:07:02 2016 +0200
+++ b/src/Tools/jEdit/src/fold_handling.scala	Tue Jul 12 11:12:07 2016 +0200
@@ -29,16 +29,16 @@
       }
 
     override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
-      Token_Markup.buffer_line_context(buffer, line).structure.depth max 0
+      Token_Markup.Line_Context.next(buffer, line).structure.depth max 0
 
     override def getPrecedingFoldLevels(
       buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] =
     {
-      val struct = Token_Markup.buffer_line_context(buffer, line).structure
+      val struct = Token_Markup.Line_Context.next(buffer, line).structure
       val result =
         if (line > 0 && struct.command)
           Range.inclusive(line - 1, 0, -1).iterator.
-            map(i => Token_Markup.buffer_line_context(buffer, i).structure).
+            map(i => Token_Markup.Line_Context.next(buffer, i).structure).
             takeWhile(_.improper).map(_ => struct.depth max 0).toList
         else Nil
 
diff -r 932a3d470264 -r 08a1f61a49a6 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Mon Jul 11 22:07:02 2016 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Jul 12 11:12:07 2016 +0200
@@ -179,6 +179,24 @@
   {
     def init(mode: String): Line_Context =
       new Line_Context(mode, Some(Scan.Finished), Outer_Syntax.Line_Structure.init)
+
+    def prev(buffer: JEditBuffer, line: Int): Line_Context =
+      if (line == 0) init(JEdit_Lib.buffer_mode(buffer))
+      else next(buffer, line - 1)
+
+    def next(buffer: JEditBuffer, line: Int): Line_Context =
+    {
+      val line_mgr = JEdit_Lib.buffer_line_manager(buffer)
+      def context =
+        line_mgr.getLineContext(line) match {
+          case c: Line_Context => Some(c)
+          case _ => None
+        }
+      context getOrElse {
+        buffer.markTokens(line, DummyTokenHandler.INSTANCE)
+        context getOrElse init(JEdit_Lib.buffer_mode(buffer))
+      }
+    }
   }
 
   class Line_Context(
@@ -187,6 +205,8 @@
       val structure: Outer_Syntax.Line_Structure)
     extends TokenMarker.LineContext(new ParserRuleSet(mode, "MAIN"), null)
   {
+    def get_context: Scan.Line_Context = context.getOrElse(Scan.Finished)
+
     override def hashCode: Int = (mode, context, structure).hashCode
     override def equals(that: Any): Boolean =
       that match {
@@ -196,29 +216,13 @@
       }
   }
 
-  def buffer_line_context(buffer: JEditBuffer, line: Int): Line_Context =
-  {
-    val line_mgr = JEdit_Lib.buffer_line_manager(buffer)
-    def context =
-      line_mgr.getLineContext(line) match {
-        case c: Line_Context => Some(c)
-        case _ => None
-      }
-    context getOrElse {
-      buffer.markTokens(line, DummyTokenHandler.INSTANCE)
-      context getOrElse Line_Context.init(JEdit_Lib.buffer_mode(buffer))
-    }
-  }
-
 
   /* tokens from line (inclusive) */
 
   private def try_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int)
     : Option[List[Token]] =
   {
-    val line_context =
-      if (line == 0) Line_Context.init(JEdit_Lib.buffer_mode(buffer))
-      else buffer_line_context(buffer, line - 1)
+    val line_context = Line_Context.prev(buffer, line)
     for {
       ctxt <- line_context.context
       text <- JEdit_Lib.try_get_text(buffer, JEdit_Lib.line_range(buffer, line))