wenzelm@43282
|
1 |
/* Title: Tools/jEdit/src/document_model.scala
|
wenzelm@36760
|
2 |
Author: Fabian Immler, TU Munich
|
wenzelm@36760
|
3 |
Author: Makarius
|
wenzelm@36760
|
4 |
|
wenzelm@55778
|
5 |
Document model connected to jEdit buffer (node in theory graph or
|
wenzelm@55778
|
6 |
auxiliary file).
|
wenzelm@36760
|
7 |
*/
|
wenzelm@34407
|
8 |
|
wenzelm@34784
|
9 |
package isabelle.jedit
|
wenzelm@34760
|
10 |
|
wenzelm@34318
|
11 |
|
wenzelm@36015
|
12 |
import isabelle._
|
wenzelm@36015
|
13 |
|
wenzelm@34693
|
14 |
import scala.collection.mutable
|
wenzelm@34446
|
15 |
|
wenzelm@34784
|
16 |
import org.gjt.sp.jedit.Buffer
|
wenzelm@34783
|
17 |
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
|
wenzelm@34318
|
18 |
|
wenzelm@34760
|
19 |
|
wenzelm@34784
|
20 |
object Document_Model
|
wenzelm@34588
|
21 |
{
|
wenzelm@34784
|
22 |
/* document model of buffer */
|
wenzelm@34784
|
23 |
|
wenzelm@50565
|
24 |
private val key = "PIDE.document_model"
|
wenzelm@34784
|
25 |
|
wenzelm@34788
|
26 |
def apply(buffer: Buffer): Option[Document_Model] =
|
wenzelm@34784
|
27 |
{
|
wenzelm@38223
|
28 |
Swing_Thread.require()
|
wenzelm@34784
|
29 |
buffer.getProperty(key) match {
|
wenzelm@34784
|
30 |
case model: Document_Model => Some(model)
|
wenzelm@34784
|
31 |
case _ => None
|
wenzelm@34784
|
32 |
}
|
wenzelm@34784
|
33 |
}
|
wenzelm@34784
|
34 |
|
wenzelm@34784
|
35 |
def exit(buffer: Buffer)
|
wenzelm@34784
|
36 |
{
|
wenzelm@38223
|
37 |
Swing_Thread.require()
|
wenzelm@34788
|
38 |
apply(buffer) match {
|
wenzelm@39636
|
39 |
case None =>
|
wenzelm@34784
|
40 |
case Some(model) =>
|
wenzelm@34784
|
41 |
model.deactivate()
|
wenzelm@34784
|
42 |
buffer.unsetProperty(key)
|
wenzelm@47058
|
43 |
buffer.propertiesChanged
|
immler@34653
|
44 |
}
|
wenzelm@34318
|
45 |
}
|
wenzelm@43397
|
46 |
|
wenzelm@52973
|
47 |
def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
|
wenzelm@43397
|
48 |
{
|
wenzelm@47058
|
49 |
Swing_Thread.require()
|
wenzelm@47058
|
50 |
apply(buffer).map(_.deactivate)
|
wenzelm@52973
|
51 |
val model = new Document_Model(session, buffer, node_name)
|
wenzelm@43397
|
52 |
buffer.setProperty(key, model)
|
wenzelm@43397
|
53 |
model.activate()
|
wenzelm@47058
|
54 |
buffer.propertiesChanged
|
wenzelm@43397
|
55 |
model
|
wenzelm@43397
|
56 |
}
|
wenzelm@34318
|
57 |
}
|
wenzelm@34318
|
58 |
|
wenzelm@38151
|
59 |
|
wenzelm@52973
|
60 |
class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name)
|
wenzelm@34588
|
61 |
{
|
wenzelm@44385
|
62 |
/* header */
|
wenzelm@38222
|
63 |
|
wenzelm@54509
|
64 |
def is_theory: Boolean = node_name.is_theory
|
wenzelm@54509
|
65 |
|
wenzelm@48707
|
66 |
def node_header(): Document.Node.Header =
|
wenzelm@46920
|
67 |
{
|
wenzelm@46920
|
68 |
Swing_Thread.require()
|
wenzelm@54509
|
69 |
|
wenzelm@54509
|
70 |
if (is_theory) {
|
wenzelm@54509
|
71 |
JEdit_Lib.buffer_lock(buffer) {
|
wenzelm@54509
|
72 |
Exn.capture {
|
wenzelm@54509
|
73 |
PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
|
wenzelm@54509
|
74 |
} match {
|
wenzelm@54509
|
75 |
case Exn.Res(header) => header
|
wenzelm@54509
|
76 |
case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
|
wenzelm@54509
|
77 |
}
|
wenzelm@46748
|
78 |
}
|
wenzelm@46748
|
79 |
}
|
wenzelm@54509
|
80 |
else Document.Node.no_header
|
wenzelm@46920
|
81 |
}
|
wenzelm@44385
|
82 |
|
wenzelm@44385
|
83 |
|
wenzelm@44385
|
84 |
/* perspective */
|
wenzelm@44385
|
85 |
|
wenzelm@52849
|
86 |
// owned by Swing thread
|
wenzelm@52816
|
87 |
private var _node_required = false
|
wenzelm@52816
|
88 |
def node_required: Boolean = _node_required
|
wenzelm@52816
|
89 |
def node_required_=(b: Boolean)
|
wenzelm@52816
|
90 |
{
|
wenzelm@52816
|
91 |
Swing_Thread.require()
|
wenzelm@54531
|
92 |
if (_node_required != b && is_theory) {
|
wenzelm@52816
|
93 |
_node_required = b
|
wenzelm@52816
|
94 |
PIDE.options_changed()
|
wenzelm@52974
|
95 |
PIDE.editor.flush()
|
wenzelm@52816
|
96 |
}
|
wenzelm@52816
|
97 |
}
|
wenzelm@52808
|
98 |
|
wenzelm@52849
|
99 |
val empty_perspective: Document.Node.Perspective_Text =
|
wenzelm@52887
|
100 |
Document.Node.Perspective(false, Text.Perspective.empty, Document.Node.Overlays.empty)
|
wenzelm@52849
|
101 |
|
wenzelm@55783
|
102 |
def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
|
wenzelm@44385
|
103 |
{
|
wenzelm@44385
|
104 |
Swing_Thread.require()
|
wenzelm@52759
|
105 |
|
wenzelm@54509
|
106 |
if (Isabelle.continuous_checking && is_theory) {
|
wenzelm@54325
|
107 |
val snapshot = this.snapshot()
|
wenzelm@54530
|
108 |
|
wenzelm@54530
|
109 |
val document_view_ranges =
|
wenzelm@55432
|
110 |
if (is_theory) {
|
wenzelm@55432
|
111 |
for {
|
wenzelm@55432
|
112 |
doc_view <- PIDE.document_views(buffer)
|
wenzelm@55432
|
113 |
range <- doc_view.perspective(snapshot).ranges
|
wenzelm@55432
|
114 |
} yield range
|
wenzelm@55432
|
115 |
}
|
wenzelm@55432
|
116 |
else Nil
|
wenzelm@54530
|
117 |
|
wenzelm@54530
|
118 |
val thy_load_ranges =
|
wenzelm@54530
|
119 |
for {
|
wenzelm@54530
|
120 |
cmd <- snapshot.node.thy_load_commands
|
wenzelm@54530
|
121 |
blob_name <- cmd.blobs_names
|
wenzelm@54530
|
122 |
blob_buffer <- JEdit_Lib.jedit_buffer(blob_name.node)
|
wenzelm@54530
|
123 |
if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
|
wenzelm@54530
|
124 |
start <- snapshot.node.command_start(cmd)
|
wenzelm@54530
|
125 |
range = snapshot.convert(cmd.proper_range + start)
|
wenzelm@54530
|
126 |
} yield range
|
wenzelm@54530
|
127 |
|
wenzelm@55785
|
128 |
val reparse = snapshot.node.thy_load_commands.exists(_.blobs_changed(doc_blobs))
|
wenzelm@55781
|
129 |
|
wenzelm@55781
|
130 |
(reparse,
|
wenzelm@55781
|
131 |
Document.Node.Perspective(node_required,
|
wenzelm@55781
|
132 |
Text.Perspective(document_view_ranges ::: thy_load_ranges),
|
wenzelm@55781
|
133 |
PIDE.editor.node_overlays(node_name)))
|
wenzelm@52849
|
134 |
}
|
wenzelm@55781
|
135 |
else (false, empty_perspective)
|
wenzelm@44385
|
136 |
}
|
wenzelm@44385
|
137 |
|
wenzelm@44385
|
138 |
|
wenzelm@54509
|
139 |
/* blob */
|
wenzelm@54509
|
140 |
|
wenzelm@55431
|
141 |
private var _blob: Option[(Bytes, Command.File)] = None // owned by Swing thread
|
wenzelm@54511
|
142 |
|
wenzelm@54511
|
143 |
private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
|
wenzelm@54511
|
144 |
|
wenzelm@55783
|
145 |
def get_blob(): Option[Document.Blob] =
|
wenzelm@54511
|
146 |
Swing_Thread.require {
|
wenzelm@55783
|
147 |
if (is_theory) None
|
wenzelm@55783
|
148 |
else {
|
wenzelm@55783
|
149 |
val (bytes, file) =
|
wenzelm@55783
|
150 |
_blob match {
|
wenzelm@55783
|
151 |
case Some(x) => x
|
wenzelm@55783
|
152 |
case None =>
|
wenzelm@55783
|
153 |
val bytes = PIDE.thy_load.file_content(buffer)
|
wenzelm@55783
|
154 |
val file = new Command.File(node_name.node, buffer.getSegment(0, buffer.getLength))
|
wenzelm@55783
|
155 |
_blob = Some((bytes, file))
|
wenzelm@55783
|
156 |
(bytes, file)
|
wenzelm@55783
|
157 |
}
|
wenzelm@55783
|
158 |
val changed = pending_edits.is_pending()
|
wenzelm@55783
|
159 |
Some(Document.Blob(bytes, file, changed))
|
wenzelm@54511
|
160 |
}
|
wenzelm@54511
|
161 |
}
|
wenzelm@54509
|
162 |
|
wenzelm@54509
|
163 |
|
wenzelm@50363
|
164 |
/* edits */
|
wenzelm@50344
|
165 |
|
wenzelm@54461
|
166 |
def node_edits(
|
wenzelm@54461
|
167 |
clear: Boolean,
|
wenzelm@54461
|
168 |
text_edits: List[Text.Edit],
|
wenzelm@54461
|
169 |
perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
|
wenzelm@50363
|
170 |
{
|
wenzelm@50363
|
171 |
Swing_Thread.require()
|
wenzelm@52815
|
172 |
|
wenzelm@54509
|
173 |
if (is_theory) {
|
wenzelm@54509
|
174 |
val header_edit = session.header_edit(node_name, node_header())
|
wenzelm@54509
|
175 |
if (clear)
|
wenzelm@54509
|
176 |
List(header_edit,
|
wenzelm@54509
|
177 |
node_name -> Document.Node.Clear(),
|
wenzelm@54509
|
178 |
node_name -> Document.Node.Edits(text_edits),
|
wenzelm@54509
|
179 |
node_name -> perspective)
|
wenzelm@54509
|
180 |
else
|
wenzelm@54509
|
181 |
List(header_edit,
|
wenzelm@54509
|
182 |
node_name -> Document.Node.Edits(text_edits),
|
wenzelm@54509
|
183 |
node_name -> perspective)
|
wenzelm@54509
|
184 |
}
|
wenzelm@54461
|
185 |
else
|
wenzelm@55435
|
186 |
List(node_name -> Document.Node.Blob(),
|
wenzelm@55435
|
187 |
node_name -> Document.Node.Edits(text_edits))
|
wenzelm@50363
|
188 |
}
|
wenzelm@50363
|
189 |
|
wenzelm@50344
|
190 |
|
wenzelm@50344
|
191 |
/* pending edits */
|
wenzelm@43648
|
192 |
|
wenzelm@43644
|
193 |
private object pending_edits // owned by Swing thread
|
wenzelm@38224
|
194 |
{
|
wenzelm@54461
|
195 |
private var pending_clear = false
|
wenzelm@38425
|
196 |
private val pending = new mutable.ListBuffer[Text.Edit]
|
wenzelm@52849
|
197 |
private var last_perspective = empty_perspective
|
wenzelm@44438
|
198 |
|
wenzelm@55781
|
199 |
def is_pending(): Boolean = pending_clear || !pending.isEmpty
|
wenzelm@38425
|
200 |
def snapshot(): List[Text.Edit] = pending.toList
|
wenzelm@38224
|
201 |
|
wenzelm@55783
|
202 |
def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
|
wenzelm@38224
|
203 |
{
|
wenzelm@54461
|
204 |
val clear = pending_clear
|
wenzelm@47393
|
205 |
val edits = snapshot()
|
wenzelm@55783
|
206 |
val (reparse, perspective) = node_perspective(doc_blobs)
|
wenzelm@55781
|
207 |
if (clear || reparse || !edits.isEmpty || last_perspective != perspective) {
|
wenzelm@54461
|
208 |
pending_clear = false
|
wenzelm@47393
|
209 |
pending.clear
|
wenzelm@54461
|
210 |
last_perspective = perspective
|
wenzelm@54461
|
211 |
node_edits(clear, edits, perspective)
|
wenzelm@43648
|
212 |
}
|
wenzelm@52759
|
213 |
else Nil
|
wenzelm@38224
|
214 |
}
|
wenzelm@38224
|
215 |
|
wenzelm@54461
|
216 |
def edit(clear: Boolean, e: Text.Edit)
|
wenzelm@38224
|
217 |
{
|
wenzelm@54511
|
218 |
reset_blob()
|
wenzelm@54511
|
219 |
|
wenzelm@54461
|
220 |
if (clear) {
|
wenzelm@54461
|
221 |
pending_clear = true
|
wenzelm@54461
|
222 |
pending.clear
|
wenzelm@54461
|
223 |
}
|
wenzelm@54461
|
224 |
pending += e
|
wenzelm@54461
|
225 |
PIDE.editor.invoke()
|
wenzelm@44436
|
226 |
}
|
wenzelm@44436
|
227 |
}
|
wenzelm@44436
|
228 |
|
wenzelm@54464
|
229 |
def snapshot(): Document.Snapshot =
|
wenzelm@54464
|
230 |
Swing_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) }
|
wenzelm@34731
|
231 |
|
wenzelm@55783
|
232 |
def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
|
wenzelm@55783
|
233 |
Swing_Thread.require { pending_edits.flushed_edits(doc_blobs) }
|
wenzelm@34828
|
234 |
|
wenzelm@34828
|
235 |
|
wenzelm@34828
|
236 |
/* buffer listener */
|
wenzelm@34828
|
237 |
|
wenzelm@34828
|
238 |
private val buffer_listener: BufferListener = new BufferAdapter
|
wenzelm@34828
|
239 |
{
|
wenzelm@40478
|
240 |
override def bufferLoaded(buffer: JEditBuffer)
|
wenzelm@40478
|
241 |
{
|
wenzelm@55791
|
242 |
pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
|
wenzelm@40478
|
243 |
}
|
wenzelm@40478
|
244 |
|
wenzelm@34828
|
245 |
override def contentInserted(buffer: JEditBuffer,
|
wenzelm@34828
|
246 |
start_line: Int, offset: Int, num_lines: Int, length: Int)
|
wenzelm@34828
|
247 |
{
|
wenzelm@40478
|
248 |
if (!buffer.isLoading)
|
wenzelm@54461
|
249 |
pending_edits.edit(false, Text.Edit.insert(offset, buffer.getText(offset, length)))
|
wenzelm@34828
|
250 |
}
|
wenzelm@34828
|
251 |
|
wenzelm@34828
|
252 |
override def preContentRemoved(buffer: JEditBuffer,
|
wenzelm@38426
|
253 |
start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
|
wenzelm@34828
|
254 |
{
|
wenzelm@40478
|
255 |
if (!buffer.isLoading)
|
wenzelm@54461
|
256 |
pending_edits.edit(false, Text.Edit.remove(offset, buffer.getText(offset, removed_length)))
|
wenzelm@34828
|
257 |
}
|
wenzelm@34828
|
258 |
}
|
wenzelm@34828
|
259 |
|
wenzelm@34828
|
260 |
|
wenzelm@38158
|
261 |
/* activation */
|
wenzelm@37557
|
262 |
|
wenzelm@43512
|
263 |
private def activate()
|
wenzelm@34784
|
264 |
{
|
wenzelm@55791
|
265 |
pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
|
wenzelm@34784
|
266 |
buffer.addBufferListener(buffer_listener)
|
wenzelm@44358
|
267 |
Token_Markup.refresh_buffer(buffer)
|
immler@34680
|
268 |
}
|
immler@34680
|
269 |
|
wenzelm@43512
|
270 |
private def deactivate()
|
immler@34680
|
271 |
{
|
wenzelm@34784
|
272 |
buffer.removeBufferListener(buffer_listener)
|
wenzelm@44358
|
273 |
Token_Markup.refresh_buffer(buffer)
|
immler@34680
|
274 |
}
|
wenzelm@34447
|
275 |
}
|