author | wenzelm |
Sat, 26 Jun 2010 22:44:25 +0200 | |
changeset 37557 | 1ae272fd4082 |
parent 37555 | d57d0f581d38 |
child 37685 | 305c326db33b |
permissions | -rw-r--r-- |
36760 | 1 |
/* Title: Tools/jEdit/src/jedit/document_model.scala |
2 |
Author: Fabian Immler, TU Munich |
|
3 |
Author: Makarius |
|
4 |
||
5 |
Document model connected to jEdit buffer. |
|
6 |
*/ |
|
34407 | 7 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
8 |
package isabelle.jedit |
34760 | 9 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
10 |
|
36015 | 11 |
import isabelle._ |
12 |
||
34703 | 13 |
import scala.actors.Actor, Actor._ |
34693 | 14 |
import scala.collection.mutable |
34446 | 15 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
16 |
import org.gjt.sp.jedit.Buffer |
34783
cb95d6bbf5f1
clarified BufferListener: use adapter, listen to contentInserted instead of preContentInserted;
wenzelm
parents:
34778
diff
changeset
|
17 |
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer} |
34649 | 18 |
import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
19 |
|
34760 | 20 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
21 |
object Document_Model |
34588 | 22 |
{ |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
23 |
/* document model of buffer */ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
24 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
25 |
private val key = "isabelle.document_model" |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
26 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
27 |
def init(session: Session, buffer: Buffer): Document_Model = |
34716 | 28 |
{ |
34789 | 29 |
Swing_Thread.assert() |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
30 |
val model = new Document_Model(session, buffer) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
31 |
buffer.setProperty(key, model) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
32 |
model.activate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
33 |
model |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
34 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
35 |
|
34788
3779c54a2d21
direct apply for Document_Model and Document_View;
wenzelm
parents:
34784
diff
changeset
|
36 |
def apply(buffer: Buffer): Option[Document_Model] = |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
37 |
{ |
34789 | 38 |
Swing_Thread.assert() |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
39 |
buffer.getProperty(key) match { |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
40 |
case model: Document_Model => Some(model) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
41 |
case _ => None |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
42 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
43 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
44 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
45 |
def exit(buffer: Buffer) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
46 |
{ |
34789 | 47 |
Swing_Thread.assert() |
34788
3779c54a2d21
direct apply for Document_Model and Document_View;
wenzelm
parents:
34784
diff
changeset
|
48 |
apply(buffer) match { |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
49 |
case None => error("No document model for buffer: " + buffer) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
50 |
case Some(model) => |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
51 |
model.deactivate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
52 |
buffer.unsetProperty(key) |
34653 | 53 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
54 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
55 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
56 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
57 |
class Document_Model(val session: Session, val buffer: Buffer) |
34588 | 58 |
{ |
37555
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
59 |
/* visible line end */ |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
60 |
|
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
61 |
// simplify slightly odd result of TextArea.getLineEndOffset |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
62 |
// NB: jEdit already normalizes \r\n and \r to \n |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
63 |
def visible_line_end(start: Int, end: Int): Int = |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
64 |
{ |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
65 |
val end1 = end - 1 |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
66 |
if (start <= end1 && end1 < buffer.getLength && |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
67 |
buffer.getSegment(end1, 1).charAt(0) == '\n') end1 |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
68 |
else end |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
69 |
} |
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
70 |
|
d57d0f581d38
simplified text_area_painter, with more precise treatment of visible line end;
wenzelm
parents:
37132
diff
changeset
|
71 |
|
34828 | 72 |
/* history */ |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
73 |
|
34833
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34830
diff
changeset
|
74 |
private val document_0 = session.begin_document(buffer.getName) |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34830
diff
changeset
|
75 |
|
34830 | 76 |
@volatile private var history = // owned by Swing thread |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
77 |
new Change(document_0.id, None, Nil, Future.value(Nil, document_0)) |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
78 |
|
34830 | 79 |
def current_change(): Change = history |
34854 | 80 |
def recent_document(): Document = current_change().ancestors.find(_.is_assigned).get.join_document |
34654 | 81 |
|
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
82 |
|
34680 | 83 |
/* transforming offsets */ |
84 |
||
34838 | 85 |
private def changes_from(doc: Document): List[Text_Edit] = |
34828 | 86 |
{ |
87 |
Swing_Thread.assert() |
|
34833
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34830
diff
changeset
|
88 |
(edits_buffer.toList /: |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34830
diff
changeset
|
89 |
current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) => change.edits ::: edits) |
34828 | 90 |
} |
34680 | 91 |
|
34823 | 92 |
def from_current(doc: Document, offset: Int): Int = |
34718 | 93 |
(offset /: changes_from(doc).reverse) ((i, change) => change before i) |
34680 | 94 |
|
34823 | 95 |
def to_current(doc: Document, offset: Int): Int = |
34718 | 96 |
(offset /: changes_from(doc)) ((i, change) => change after i) |
34680 | 97 |
|
34834
df9af932e418
slightly more uniform/robust handling of visible document;
wenzelm
parents:
34833
diff
changeset
|
98 |
def lines_of_command(doc: Document, cmd: Command): (Int, Int) = |
34680 | 99 |
{ |
34858 | 100 |
val start = doc.command_start(cmd).get // FIXME total? |
34856
aa9e22d9f9a7
eliminated Command.stop, which tends to case duplicate traversal of commands;
wenzelm
parents:
34854
diff
changeset
|
101 |
val stop = start + cmd.length |
aa9e22d9f9a7
eliminated Command.stop, which tends to case duplicate traversal of commands;
wenzelm
parents:
34854
diff
changeset
|
102 |
(buffer.getLineOfOffset(to_current(doc, start)), |
aa9e22d9f9a7
eliminated Command.stop, which tends to case duplicate traversal of commands;
wenzelm
parents:
34854
diff
changeset
|
103 |
buffer.getLineOfOffset(to_current(doc, stop))) |
34680 | 104 |
} |
105 |
||
106 |
||
34828 | 107 |
/* text edits */ |
108 |
||
34838 | 109 |
private val edits_buffer = new mutable.ListBuffer[Text_Edit] // owned by Swing thread |
34828 | 110 |
|
37132 | 111 |
private val edits_delay = Swing_Thread.delay_last(300) { // FIXME input_delay property |
34828 | 112 |
if (!edits_buffer.isEmpty) { |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
113 |
val new_change = current_change().edit(session, edits_buffer.toList) |
34828 | 114 |
edits_buffer.clear |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
115 |
history = new_change |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
116 |
new_change.result.map(_ => session.input(new_change)) |
34828 | 117 |
} |
118 |
} |
|
119 |
||
120 |
||
121 |
/* buffer listener */ |
|
122 |
||
123 |
private val buffer_listener: BufferListener = new BufferAdapter |
|
124 |
{ |
|
125 |
override def contentInserted(buffer: JEditBuffer, |
|
126 |
start_line: Int, offset: Int, num_lines: Int, length: Int) |
|
127 |
{ |
|
34864 | 128 |
edits_buffer += new Text_Edit(true, offset, buffer.getText(offset, length)) |
34828 | 129 |
edits_delay() |
130 |
} |
|
131 |
||
132 |
override def preContentRemoved(buffer: JEditBuffer, |
|
133 |
start_line: Int, start: Int, num_lines: Int, removed_length: Int) |
|
134 |
{ |
|
34864 | 135 |
edits_buffer += new Text_Edit(false, start, buffer.getText(start, removed_length)) |
34828 | 136 |
edits_delay() |
137 |
} |
|
138 |
} |
|
139 |
||
140 |
||
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
141 |
/* activation */ |
34680 | 142 |
|
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
143 |
private val token_marker = new Isabelle_Token_Marker(this) |
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
144 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
145 |
def activate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
146 |
{ |
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
147 |
buffer.setTokenMarker(token_marker) |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
148 |
buffer.addBufferListener(buffer_listener) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
149 |
buffer.propertiesChanged() |
34680 | 150 |
|
34864 | 151 |
edits_buffer += new Text_Edit(true, 0, buffer.getText(0, buffer.getLength)) |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
152 |
edits_delay() |
34680 | 153 |
} |
154 |
||
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
155 |
def refresh() |
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
156 |
{ |
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
157 |
buffer.setTokenMarker(token_marker) |
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
158 |
} |
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
159 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
160 |
def deactivate() |
34680 | 161 |
{ |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
162 |
buffer.setTokenMarker(buffer.getMode.getTokenMarker) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
163 |
buffer.removeBufferListener(buffer_listener) |
34680 | 164 |
} |
34447 | 165 |
} |