# HG changeset patch
# User wenzelm
# Date 1468321133 -7200
# Node ID be6ceddff1020943475f5248c55565893e36f471
# Parent  019856db2bb625f6011bd7ec75a55388a94c2349
tuned;

diff -r 019856db2bb6 -r be6ceddff102 src/Tools/jEdit/src/fold_handling.scala
--- a/src/Tools/jEdit/src/fold_handling.scala	Tue Jul 12 11:51:05 2016 +0200
+++ b/src/Tools/jEdit/src/fold_handling.scala	Tue Jul 12 12:58:53 2016 +0200
@@ -34,12 +34,12 @@
     override def getPrecedingFoldLevels(
       buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] =
     {
-      val struct = Token_Markup.Line_Context.next(buffer, line).structure
+      val structure = Token_Markup.Line_Context.next(buffer, line).structure
       val result =
-        if (line > 0 && struct.command)
+        if (line > 0 && structure.command)
           Range.inclusive(line - 1, 0, -1).iterator.
             map(i => Token_Markup.Line_Context.next(buffer, i).structure).
-            takeWhile(_.improper).map(_ => struct.depth max 0).toList
+            takeWhile(_.improper).map(_ => structure.depth max 0).toList
         else Nil
 
       if (result.isEmpty) null