equal
deleted
inserted
replaced
9 |
9 |
10 import isabelle._ |
10 import isabelle._ |
11 |
11 |
12 import javax.swing.text.Segment |
12 import javax.swing.text.Segment |
13 |
13 |
14 import scala.collection.JavaConverters |
14 import scala.jdk.CollectionConverters._ |
15 |
15 |
16 import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler} |
16 import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler} |
17 |
17 |
18 |
18 |
19 object Fold_Handling |
19 object Fold_Handling |
40 Range.inclusive(line - 1, 0, -1).iterator. |
40 Range.inclusive(line - 1, 0, -1).iterator. |
41 map(i => Token_Markup.Line_Context.after(buffer, i).structure). |
41 map(i => Token_Markup.Line_Context.after(buffer, i).structure). |
42 takeWhile(_.improper).map(_ => structure.depth max 0).toList |
42 takeWhile(_.improper).map(_ => structure.depth max 0).toList |
43 else Nil |
43 else Nil |
44 |
44 |
45 if (result.isEmpty) null |
45 if (result.isEmpty) null else result.map(Integer.valueOf).asJava |
46 else JavaConverters.seqAsJavaList(result.map(Integer.valueOf)) |
|
47 } |
46 } |
48 } |
47 } |
49 |
48 |
50 |
49 |
51 /* output: static document rendering */ |
50 /* output: static document rendering */ |