author | wenzelm |
Sat, 13 Jul 2013 13:25:42 +0200 | |
changeset 52643 | 34c29356930e |
parent 51240 | a7a04b449e8b |
child 52900 | d29bf6db8a2d |
permissions | -rw-r--r-- |
51240 | 1 |
/* Title: Tools/jEdit/src/fold_handling.scala |
50542
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
3 |
|
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
4 |
Handling of folds within the text structure. |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
6 |
|
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
8 |
|
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
9 |
|
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
10 |
import isabelle._ |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
11 |
|
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
12 |
import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
13 |
|
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
14 |
import javax.swing.text.Segment |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
15 |
|
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
16 |
|
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
17 |
object Fold_Handling |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
18 |
{ |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
19 |
class Document_Fold_Handler(private val rendering: Rendering) |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
20 |
extends FoldHandler("isabelle-document") |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
21 |
{ |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
22 |
override def equals(other: Any): Boolean = |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
23 |
other match { |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
24 |
case that: Document_Fold_Handler => this.rendering == that.rendering |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
25 |
case _ => false |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
26 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
27 |
|
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
28 |
override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int = |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
29 |
{ |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
30 |
def depth(i: Text.Offset): Int = |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
31 |
if (i < 0) 0 |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
32 |
else { |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
33 |
rendering.fold_depth(Text.Range(i, i + 1)).map(_.info) match { |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
34 |
case d #:: _ => d |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
35 |
case _ => 0 |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
36 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
37 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
38 |
|
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
39 |
if (line <= 0) 0 |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
40 |
else { |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
41 |
val start = buffer.getLineStartOffset(line - 1) |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
42 |
val end = buffer.getLineEndOffset(line - 1) |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
43 |
buffer.getFoldLevel(line - 1) - depth(start - 1) + depth(end - 1) |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
44 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
45 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
46 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
47 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
48 |