author | wenzelm |
Sun, 10 Jan 2010 17:10:32 +0100 | |
changeset 34854 | 64c2eb92df9f |
parent 34853 | 32b49207ca20 |
child 34856 | aa9e22d9f9a7 |
permissions | -rw-r--r-- |
34407 | 1 |
/* |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
2 |
* Document model connected to jEdit buffer |
34407 | 3 |
* |
4 |
* @author Fabian Immler, TU Munich |
|
34447 | 5 |
* @author Makarius |
34407 | 6 |
*/ |
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 |
|
34838 | 11 |
import isabelle.proofdocument.{Change, Command, Document, Session} |
34783
cb95d6bbf5f1
clarified BufferListener: use adapter, listen to contentInserted instead of preContentInserted;
wenzelm
parents:
34778
diff
changeset
|
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 |
{ |
34828 | 59 |
/* history */ |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
60 |
|
34833
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34830
diff
changeset
|
61 |
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
|
62 |
|
34830 | 63 |
@volatile private var history = // owned by Swing thread |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
64 |
new Change(document_0.id, None, Nil, Future.value(Nil, document_0)) |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
65 |
|
34830 | 66 |
def current_change(): Change = history |
34854 | 67 |
def recent_document(): Document = current_change().ancestors.find(_.is_assigned).get.join_document |
34654 | 68 |
|
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
69 |
|
34680 | 70 |
/* transforming offsets */ |
71 |
||
34838 | 72 |
private def changes_from(doc: Document): List[Text_Edit] = |
34828 | 73 |
{ |
74 |
Swing_Thread.assert() |
|
34833
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34830
diff
changeset
|
75 |
(edits_buffer.toList /: |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34830
diff
changeset
|
76 |
current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) => change.edits ::: edits) |
34828 | 77 |
} |
34680 | 78 |
|
34823 | 79 |
def from_current(doc: Document, offset: Int): Int = |
34718 | 80 |
(offset /: changes_from(doc).reverse) ((i, change) => change before i) |
34680 | 81 |
|
34823 | 82 |
def to_current(doc: Document, offset: Int): Int = |
34718 | 83 |
(offset /: changes_from(doc)) ((i, change) => change after i) |
34680 | 84 |
|
34834
df9af932e418
slightly more uniform/robust handling of visible document;
wenzelm
parents:
34833
diff
changeset
|
85 |
def lines_of_command(doc: Document, cmd: Command): (Int, Int) = |
34680 | 86 |
{ |
34834
df9af932e418
slightly more uniform/robust handling of visible document;
wenzelm
parents:
34833
diff
changeset
|
87 |
(buffer.getLineOfOffset(to_current(doc, cmd.start(doc))), |
df9af932e418
slightly more uniform/robust handling of visible document;
wenzelm
parents:
34833
diff
changeset
|
88 |
buffer.getLineOfOffset(to_current(doc, cmd.stop(doc)))) |
34680 | 89 |
} |
90 |
||
91 |
||
34828 | 92 |
/* text edits */ |
93 |
||
34838 | 94 |
private val edits_buffer = new mutable.ListBuffer[Text_Edit] // owned by Swing thread |
34828 | 95 |
|
96 |
private val edits_delay = Swing_Thread.delay_last(300) { |
|
97 |
if (!edits_buffer.isEmpty) { |
|
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
98 |
val new_change = current_change().edit(session, edits_buffer.toList) |
34828 | 99 |
edits_buffer.clear |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
100 |
history = new_change |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
101 |
new_change.result.map(_ => session.input(new_change)) |
34828 | 102 |
} |
103 |
} |
|
104 |
||
105 |
||
106 |
/* buffer listener */ |
|
107 |
||
108 |
private val buffer_listener: BufferListener = new BufferAdapter |
|
109 |
{ |
|
110 |
override def contentInserted(buffer: JEditBuffer, |
|
111 |
start_line: Int, offset: Int, num_lines: Int, length: Int) |
|
112 |
{ |
|
34838 | 113 |
edits_buffer += Text_Edit.Insert(offset, buffer.getText(offset, length)) |
34828 | 114 |
edits_delay() |
115 |
} |
|
116 |
||
117 |
override def preContentRemoved(buffer: JEditBuffer, |
|
118 |
start_line: Int, start: Int, num_lines: Int, removed_length: Int) |
|
119 |
{ |
|
34838 | 120 |
edits_buffer += Text_Edit.Remove(start, buffer.getText(start, removed_length)) |
34828 | 121 |
edits_delay() |
122 |
} |
|
123 |
} |
|
124 |
||
125 |
||
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
126 |
/* activation */ |
34680 | 127 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
128 |
def activate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
129 |
{ |
34828 | 130 |
buffer.setTokenMarker(new Isabelle_Token_Marker(this)) |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
131 |
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
|
132 |
buffer.propertiesChanged() |
34680 | 133 |
|
34838 | 134 |
edits_buffer += Text_Edit.Insert(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
|
135 |
edits_delay() |
34680 | 136 |
} |
137 |
||
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
138 |
def deactivate() |
34680 | 139 |
{ |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
140 |
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
|
141 |
buffer.removeBufferListener(buffer_listener) |
34680 | 142 |
} |
34447 | 143 |
} |