author | wenzelm |
Mon, 04 Jan 2010 19:08:10 +0100 | |
changeset 34835 | 67733fd0e3fa |
parent 34834 | df9af932e418 |
child 34838 | 08a72dc4868e |
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 |
|
34823 | 11 |
import isabelle.proofdocument.{Change, Command, Edit, Insert, Remove, 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 |
34833
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34830
diff
changeset
|
64 |
new Change(None, Nil, document_0.id, Future.value(document_0, Nil)) |
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
65 |
|
34830 | 66 |
def current_change(): Change = history |
34660 | 67 |
|
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
68 |
def recent_document(): Document = |
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
69 |
{ |
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
70 |
def find(change: Change): Document = |
34835
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34834
diff
changeset
|
71 |
if (change.result.is_finished && change.document.is_assigned || !change.parent.isDefined) |
67733fd0e3fa
back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
wenzelm
parents:
34834
diff
changeset
|
72 |
change.document |
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
73 |
else find(change.parent.get) |
34829 | 74 |
find(current_change()) |
34824
ac35eee85f5c
renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents:
34823
diff
changeset
|
75 |
} |
34654 | 76 |
|
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
77 |
|
34680 | 78 |
/* transforming offsets */ |
79 |
||
34823 | 80 |
private def changes_from(doc: Document): List[Edit] = |
34828 | 81 |
{ |
82 |
Swing_Thread.assert() |
|
34833
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34830
diff
changeset
|
83 |
(edits_buffer.toList /: |
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34830
diff
changeset
|
84 |
current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) => change.edits ::: edits) |
34828 | 85 |
} |
34680 | 86 |
|
34823 | 87 |
def from_current(doc: Document, offset: Int): Int = |
34718 | 88 |
(offset /: changes_from(doc).reverse) ((i, change) => change before i) |
34680 | 89 |
|
34823 | 90 |
def to_current(doc: Document, offset: Int): Int = |
34718 | 91 |
(offset /: changes_from(doc)) ((i, change) => change after i) |
34680 | 92 |
|
34834
df9af932e418
slightly more uniform/robust handling of visible document;
wenzelm
parents:
34833
diff
changeset
|
93 |
def lines_of_command(doc: Document, cmd: Command): (Int, Int) = |
34680 | 94 |
{ |
34834
df9af932e418
slightly more uniform/robust handling of visible document;
wenzelm
parents:
34833
diff
changeset
|
95 |
(buffer.getLineOfOffset(to_current(doc, cmd.start(doc))), |
df9af932e418
slightly more uniform/robust handling of visible document;
wenzelm
parents:
34833
diff
changeset
|
96 |
buffer.getLineOfOffset(to_current(doc, cmd.stop(doc)))) |
34680 | 97 |
} |
98 |
||
99 |
||
34828 | 100 |
/* text edits */ |
101 |
||
102 |
private val edits_buffer = new mutable.ListBuffer[Edit] // owned by Swing thread |
|
103 |
||
104 |
private val edits_delay = Swing_Thread.delay_last(300) { |
|
105 |
if (!edits_buffer.isEmpty) { |
|
106 |
val edits = edits_buffer.toList |
|
34829 | 107 |
val change1 = current_change() |
34833
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34830
diff
changeset
|
108 |
val result_id = session.create_id() |
34828 | 109 |
val result: Future[Document.Result] = Future.fork { |
34833
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34830
diff
changeset
|
110 |
Document.text_edits(session, change1.document, result_id, edits) |
34828 | 111 |
} |
34833
683ddf358698
recovered explicit Changed.id (copy of future document) -- avoids premature joining of result;
wenzelm
parents:
34830
diff
changeset
|
112 |
val change2 = new Change(Some(change1), edits, result_id, result) |
34830 | 113 |
history = change2 |
34828 | 114 |
result.map(_ => session.input(change2)) |
115 |
edits_buffer.clear |
|
116 |
} |
|
117 |
} |
|
118 |
||
119 |
||
120 |
/* buffer listener */ |
|
121 |
||
122 |
private val buffer_listener: BufferListener = new BufferAdapter |
|
123 |
{ |
|
124 |
override def contentInserted(buffer: JEditBuffer, |
|
125 |
start_line: Int, offset: Int, num_lines: Int, length: Int) |
|
126 |
{ |
|
127 |
edits_buffer += Insert(offset, buffer.getText(offset, length)) |
|
128 |
edits_delay() |
|
129 |
} |
|
130 |
||
131 |
override def preContentRemoved(buffer: JEditBuffer, |
|
132 |
start_line: Int, start: Int, num_lines: Int, removed_length: Int) |
|
133 |
{ |
|
134 |
edits_buffer += Remove(start, buffer.getText(start, removed_length)) |
|
135 |
edits_delay() |
|
136 |
} |
|
137 |
} |
|
138 |
||
139 |
||
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
140 |
/* activation */ |
34680 | 141 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
142 |
def activate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
143 |
{ |
34828 | 144 |
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
|
145 |
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
|
146 |
buffer.propertiesChanged() |
34680 | 147 |
|
34828 | 148 |
edits_buffer += 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
|
149 |
edits_delay() |
34680 | 150 |
} |
151 |
||
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
152 |
def deactivate() |
34680 | 153 |
{ |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
154 |
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
|
155 |
buffer.removeBufferListener(buffer_listener) |
34680 | 156 |
} |
34447 | 157 |
} |