author | wenzelm |
Thu, 16 Oct 2014 12:09:57 +0200 | |
changeset 58694 | 983e98da2a42 |
parent 58692 | 80832ae207ad |
child 58696 | 6b7445774ce3 |
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 |
{ |
58694 | 19 |
/* input: dynamic line context */ |
20 |
||
21 |
class Fold_Handler extends FoldHandler("isabelle") |
|
22 |
{ |
|
23 |
override def equals(other: Any): Boolean = |
|
24 |
other match { |
|
25 |
case that: Fold_Handler => true |
|
26 |
case _ => false |
|
27 |
} |
|
28 |
||
29 |
override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int = |
|
30 |
Token_Markup.buffer_line_depth(buffer, line) |
|
31 |
} |
|
32 |
||
33 |
||
34 |
/* output: static document rendering */ |
|
35 |
||
50542
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
36 |
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
|
37 |
extends FoldHandler("isabelle-document") |
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 |
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
|
40 |
other match { |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
41 |
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
|
42 |
case _ => false |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
43 |
} |
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 |
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
|
46 |
{ |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
47 |
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
|
48 |
if (i < 0) 0 |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
49 |
else { |
58692 | 50 |
rendering.fold_depth(Text.Range(i, i + 1)) match { |
51 |
case Text.Info(_, d) :: _ => d |
|
50542
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
52 |
case _ => 0 |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
53 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
54 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
55 |
|
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
56 |
if (line <= 0) 0 |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
57 |
else { |
56589
71c5d1f516c0
more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
wenzelm
parents:
52900
diff
changeset
|
58 |
val range = JEdit_Lib.line_range(buffer, line - 1) |
71c5d1f516c0
more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
wenzelm
parents:
52900
diff
changeset
|
59 |
buffer.getFoldLevel(line - 1) - depth(range.start - 1) + depth(range.stop - 1) |
50542
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
60 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
61 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
62 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
63 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
64 |