author | wenzelm |
Tue, 21 Oct 2014 15:21:44 +0200 | |
changeset 58748 | 8f92f17d8781 |
parent 58700 | 4717d18cc619 |
child 63454 | 08a1f61a49a6 |
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 |
|
58700 | 12 |
import javax.swing.text.Segment |
50542
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
13 |
|
58700 | 14 |
import scala.collection.convert.WrapAsJava |
15 |
||
16 |
import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler} |
|
50542
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
17 |
|
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 |
object Fold_Handling |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
20 |
{ |
58694 | 21 |
/* input: dynamic line context */ |
22 |
||
23 |
class Fold_Handler extends FoldHandler("isabelle") |
|
24 |
{ |
|
25 |
override def equals(other: Any): Boolean = |
|
26 |
other match { |
|
27 |
case that: Fold_Handler => true |
|
28 |
case _ => false |
|
29 |
} |
|
30 |
||
31 |
override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int = |
|
58748 | 32 |
Token_Markup.buffer_line_context(buffer, line).structure.depth max 0 |
58700 | 33 |
|
34 |
override def getPrecedingFoldLevels( |
|
35 |
buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] = |
|
36 |
{ |
|
58748 | 37 |
val struct = Token_Markup.buffer_line_context(buffer, line).structure |
58700 | 38 |
val result = |
39 |
if (line > 0 && struct.command) |
|
40 |
Range.inclusive(line - 1, 0, -1).iterator. |
|
58748 | 41 |
map(i => Token_Markup.buffer_line_context(buffer, i).structure). |
58700 | 42 |
takeWhile(_.improper).map(_ => struct.depth max 0).toList |
43 |
else Nil |
|
44 |
||
45 |
if (result.isEmpty) null |
|
46 |
else WrapAsJava.seqAsJavaList(result.map(i => new Integer(i))) |
|
47 |
} |
|
58694 | 48 |
} |
49 |
||
50 |
||
51 |
/* output: static document rendering */ |
|
52 |
||
50542
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
53 |
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
|
54 |
extends FoldHandler("isabelle-document") |
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 |
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
|
57 |
other match { |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
58 |
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
|
59 |
case _ => false |
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 |
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
|
63 |
{ |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
64 |
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
|
65 |
if (i < 0) 0 |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
66 |
else { |
58692 | 67 |
rendering.fold_depth(Text.Range(i, i + 1)) match { |
68 |
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
|
69 |
case _ => 0 |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
70 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
71 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
72 |
|
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
73 |
if (line <= 0) 0 |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
74 |
else { |
56589
71c5d1f516c0
more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
wenzelm
parents:
52900
diff
changeset
|
75 |
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
|
76 |
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
|
77 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
78 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
79 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
80 |
} |
58bd88159f8f
fold handling within Pretty_Text_Area, based on formal document content, which is static here;
wenzelm
parents:
diff
changeset
|
81 |