| changeset 52900 | d29bf6db8a2d |
| parent 51240 | a7a04b449e8b |
| child 56589 | 71c5d1f516c0 |
| 52899:3ff23987f316 | 52900:d29bf6db8a2d |
|---|---|
29 { |
29 { |
30 def depth(i: Text.Offset): Int = |
30 def depth(i: Text.Offset): Int = |
31 if (i < 0) 0 |
31 if (i < 0) 0 |
32 else { |
32 else { |
33 rendering.fold_depth(Text.Range(i, i + 1)).map(_.info) match { |
33 rendering.fold_depth(Text.Range(i, i + 1)).map(_.info) match { |
34 case d #:: _ => d |
34 case d :: _ => d |
35 case _ => 0 |
35 case _ => 0 |
36 } |
36 } |
37 } |
37 } |
38 |
38 |
39 if (line <= 0) 0 |
39 if (line <= 0) 0 |