src/Tools/jEdit/src/fold_handling.scala

--- a/src/Tools/jEdit/src/fold_handling.scala	Wed Oct 15 17:18:08 2014 +0200
+++ b/src/Tools/jEdit/src/fold_handling.scala	Thu Oct 16 10:43:34 2014 +0200
@@ -30,8 +30,8 @@
       def depth(i: Text.Offset): Int =
         if (i < 0) 0
         else {
-          rendering.fold_depth(Text.Range(i, i + 1)).map(_.info) match {
-            case d :: _ => d
+          rendering.fold_depth(Text.Range(i, i + 1)) match {
+            case Text.Info(_, d) :: _ => d
             case _ => 0
           }
         }