# HG changeset patch
# User wenzelm
# Date 1413449014 -7200
# Node ID 80832ae207adde6d7c3363962b8991d854b04b3b
# Parent  6a75a4c24339df7d26f1b4177f7ecddcadee888d
tuned;

diff -r 6a75a4c24339 -r 80832ae207ad 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
           }
         }