author | wenzelm |
Thu, 27 May 2010 12:35:40 +0200 | |
changeset 37132 | 10ef4da1c314 |
parent 36760 | b82a698ef6c9 |
child 37555 | d57d0f581d38 |
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 |
{ |
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 |
{ |
34858 | 87 |
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
|
88 |
val stop = start + cmd.length |
aa9e22d9f9a7
eliminated Command.stop, which tends to case duplicate traversal of commands;
wenzelm
parents:
34854
diff
changeset
|
89 |
(buffer.getLineOfOffset(to_current(doc, start)), |
aa9e22d9f9a7
eliminated Command.stop, which tends to case duplicate traversal of commands;
wenzelm
parents:
34854
diff
changeset
|
90 |
buffer.getLineOfOffset(to_current(doc, stop))) |
34680 | 91 |
} |
92 |
||
93 |
||
34828 | 94 |
/* text edits */ |
95 |
||
34838 | 96 |
private val edits_buffer = new mutable.ListBuffer[Text_Edit] // owned by Swing thread |
34828 | 97 |
|
37132 | 98 |
private val edits_delay = Swing_Thread.delay_last(300) { // FIXME input_delay property |
34828 | 99 |
if (!edits_buffer.isEmpty) { |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
100 |
val new_change = current_change().edit(session, edits_buffer.toList) |
34828 | 101 |
edits_buffer.clear |
34853
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
102 |
history = new_change |
32b49207ca20
misc tuning and clarification of Document/Change;
wenzelm
parents:
34840
diff
changeset
|
103 |
new_change.result.map(_ => session.input(new_change)) |
34828 | 104 |
} |
105 |
} |
|
106 |
||
107 |
||
108 |
/* buffer listener */ |
|
109 |
||
110 |
private val buffer_listener: BufferListener = new BufferAdapter |
|
111 |
{ |
|
112 |
override def contentInserted(buffer: JEditBuffer, |
|
113 |
start_line: Int, offset: Int, num_lines: Int, length: Int) |
|
114 |
{ |
|
34864 | 115 |
edits_buffer += new Text_Edit(true, offset, buffer.getText(offset, length)) |
34828 | 116 |
edits_delay() |
117 |
} |
|
118 |
||
119 |
override def preContentRemoved(buffer: JEditBuffer, |
|
120 |
start_line: Int, start: Int, num_lines: Int, removed_length: Int) |
|
121 |
{ |
|
34864 | 122 |
edits_buffer += new Text_Edit(false, start, buffer.getText(start, removed_length)) |
34828 | 123 |
edits_delay() |
124 |
} |
|
125 |
} |
|
126 |
||
127 |
||
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
128 |
/* activation */ |
34680 | 129 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
130 |
def activate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
131 |
{ |
34828 | 132 |
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
|
133 |
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
|
134 |
buffer.propertiesChanged() |
34680 | 135 |
|
34864 | 136 |
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
|
137 |
edits_delay() |
34680 | 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 |
def deactivate() |
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 |
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
|
143 |
buffer.removeBufferListener(buffer_listener) |
34680 | 144 |
} |
34447 | 145 |
} |