| changeset 56589 | 71c5d1f516c0 |
| parent 52900 | d29bf6db8a2d |
| child 58692 | 80832ae207ad |
| 56588:272d173cd398 | 56589:71c5d1f516c0 |
|---|---|
36 } |
36 } |
37 } |
37 } |
38 |
38 |
39 if (line <= 0) 0 |
39 if (line <= 0) 0 |
40 else { |
40 else { |
41 val start = buffer.getLineStartOffset(line - 1) |
41 val range = JEdit_Lib.line_range(buffer, line - 1) |
42 val end = buffer.getLineEndOffset(line - 1) |
42 buffer.getFoldLevel(line - 1) - depth(range.start - 1) + depth(range.stop - 1) |
43 buffer.getFoldLevel(line - 1) - depth(start - 1) + depth(end - 1) |
|
44 } |
43 } |
45 } |
44 } |
46 } |
45 } |
47 } |
46 } |
48 |
47 |