author | wenzelm |
Wed, 23 Jul 2014 10:02:19 +0200 | |
changeset 57610 | 518e28a7c74b |
parent 56823 | 37be55461dbe |
child 57612 | 990ffb84489b |
permissions | -rw-r--r-- |
43282
5d294220ca43
moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents:
40851
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/document_model.scala |
36760 | 2 |
Author: Fabian Immler, TU Munich |
3 |
Author: Makarius |
|
4 |
||
55778 | 5 |
Document model connected to jEdit buffer (node in theory graph or |
6 |
auxiliary file). |
|
36760 | 7 |
*/ |
34407 | 8 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
9 |
package isabelle.jedit |
34760 | 10 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
11 |
|
36015 | 12 |
import isabelle._ |
13 |
||
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} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
18 |
|
34760 | 19 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
20 |
object Document_Model |
34588 | 21 |
{ |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
22 |
/* 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
|
23 |
|
50565 | 24 |
private val key = "PIDE.document_model" |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
25 |
|
34788
3779c54a2d21
direct apply for Document_Model and Document_View;
wenzelm
parents:
34784
diff
changeset
|
26 |
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
|
27 |
{ |
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
56473
diff
changeset
|
28 |
Swing_Thread.require {} |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
29 |
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
|
30 |
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
|
31 |
case _ => None |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
32 |
} |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
33 |
} |
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 |
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
|
36 |
{ |
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
56473
diff
changeset
|
37 |
Swing_Thread.require {} |
34788
3779c54a2d21
direct apply for Document_Model and Document_View;
wenzelm
parents:
34784
diff
changeset
|
38 |
apply(buffer) match { |
39636 | 39 |
case None => |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
40 |
case Some(model) => |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
41 |
model.deactivate() |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
42 |
buffer.unsetProperty(key) |
47058
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46920
diff
changeset
|
43 |
buffer.propertiesChanged |
34653 | 44 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
45 |
} |
43397 | 46 |
|
52973 | 47 |
def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model = |
43397 | 48 |
{ |
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
56473
diff
changeset
|
49 |
Swing_Thread.require {} |
47058
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46920
diff
changeset
|
50 |
apply(buffer).map(_.deactivate) |
52973 | 51 |
val model = new Document_Model(session, buffer, node_name) |
43397 | 52 |
buffer.setProperty(key, model) |
53 |
model.activate() |
|
47058
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46920
diff
changeset
|
54 |
buffer.propertiesChanged |
43397 | 55 |
model |
56 |
} |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
57 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
58 |
|
38151 | 59 |
|
52973 | 60 |
class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name) |
34588 | 61 |
{ |
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
62 |
/* header */ |
38222
dac5fa0ac971
replaced individual Document_Model history by all-inclusive one in Session;
wenzelm
parents:
38158
diff
changeset
|
63 |
|
54509
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
64 |
def is_theory: Boolean = node_name.is_theory |
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
65 |
|
48707
ba531af91148
simplified Document.Node.Header -- internalized errors;
wenzelm
parents:
47393
diff
changeset
|
66 |
def node_header(): Document.Node.Header = |
46920
5f44c8bea84e
more explicit indication of swing thread context;
wenzelm
parents:
46750
diff
changeset
|
67 |
{ |
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
56473
diff
changeset
|
68 |
Swing_Thread.require {} |
54509
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
69 |
|
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
70 |
if (is_theory) { |
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
71 |
JEdit_Lib.buffer_lock(buffer) { |
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
72 |
Exn.capture { |
56823
37be55461dbe
more frugal access to theory text via Reader, reduced costs for I/O text decoding;
wenzelm
parents:
56801
diff
changeset
|
73 |
PIDE.resources.check_thy_reader("", node_name, JEdit_Lib.buffer_reader(buffer)) |
54509
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
74 |
} match { |
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
75 |
case Exn.Res(header) => header |
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
76 |
case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn)) |
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
77 |
} |
46748
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46740
diff
changeset
|
78 |
} |
8f3ae4d04a2d
refined node_header -- more direct buffer access (again);
wenzelm
parents:
46740
diff
changeset
|
79 |
} |
54509
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
80 |
else Document.Node.no_header |
46920
5f44c8bea84e
more explicit indication of swing thread context;
wenzelm
parents:
46750
diff
changeset
|
81 |
} |
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
82 |
|
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
83 |
|
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
84 |
/* perspective */ |
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
85 |
|
52849 | 86 |
// owned by Swing thread |
52816
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
87 |
private var _node_required = false |
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
88 |
def node_required: Boolean = _node_required |
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
89 |
def node_required_=(b: Boolean) |
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
90 |
{ |
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
56473
diff
changeset
|
91 |
Swing_Thread.require {} |
54531
8330faaeebd5
restrict node_required status and Theories panel to actual theories;
wenzelm
parents:
54530
diff
changeset
|
92 |
if (_node_required != b && is_theory) { |
52816
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
93 |
_node_required = b |
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
94 |
PIDE.options_changed() |
52974 | 95 |
PIDE.editor.flush() |
52816
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
96 |
} |
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
97 |
} |
52808
143f225e50f5
allow explicit indication of required node: full eval, no prints;
wenzelm
parents:
52807
diff
changeset
|
98 |
|
55783 | 99 |
def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) = |
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
100 |
{ |
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
56473
diff
changeset
|
101 |
Swing_Thread.require {} |
52759
a20631db9c8a
support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents:
50565
diff
changeset
|
102 |
|
54509
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
103 |
if (Isabelle.continuous_checking && is_theory) { |
54325
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
52977
diff
changeset
|
104 |
val snapshot = this.snapshot() |
54530
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54521
diff
changeset
|
105 |
|
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54521
diff
changeset
|
106 |
val document_view_ranges = |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
107 |
if (is_theory) { |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
108 |
for { |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
109 |
doc_view <- PIDE.document_views(buffer) |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
110 |
range <- doc_view.perspective(snapshot).ranges |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
111 |
} yield range |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
112 |
} |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
55431
diff
changeset
|
113 |
else Nil |
54530
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54521
diff
changeset
|
114 |
|
56314 | 115 |
val load_ranges = |
54530
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54521
diff
changeset
|
116 |
for { |
56314 | 117 |
cmd <- snapshot.node.load_commands |
54530
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54521
diff
changeset
|
118 |
blob_name <- cmd.blobs_names |
56457
eea4bbe15745
tuned signature -- prefer static type Document.Node.Name;
wenzelm
parents:
56335
diff
changeset
|
119 |
blob_buffer <- JEdit_Lib.jedit_buffer(blob_name) |
54530
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54521
diff
changeset
|
120 |
if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty |
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54521
diff
changeset
|
121 |
start <- snapshot.node.command_start(cmd) |
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54521
diff
changeset
|
122 |
range = snapshot.convert(cmd.proper_range + start) |
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54521
diff
changeset
|
123 |
} yield range |
2c1440f70028
ranges of thy_load commands count as visible within perspective;
wenzelm
parents:
54521
diff
changeset
|
124 |
|
56314 | 125 |
val reparse = snapshot.node.load_commands.exists(_.blobs_changed(doc_blobs)) |
55781
b3a4207fb9a6
proper update of text perspective for nodes with changed blobs, which is important to refresh the corresponding command perspective (otherwise it might refer to invalid thy_load commands and cause full execution of the node by the prover);
wenzelm
parents:
55778
diff
changeset
|
126 |
|
b3a4207fb9a6
proper update of text perspective for nodes with changed blobs, which is important to refresh the corresponding command perspective (otherwise it might refer to invalid thy_load commands and cause full execution of the node by the prover);
wenzelm
parents:
55778
diff
changeset
|
127 |
(reparse, |
b3a4207fb9a6
proper update of text perspective for nodes with changed blobs, which is important to refresh the corresponding command perspective (otherwise it might refer to invalid thy_load commands and cause full execution of the node by the prover);
wenzelm
parents:
55778
diff
changeset
|
128 |
Document.Node.Perspective(node_required, |
56314 | 129 |
Text.Perspective(document_view_ranges ::: load_ranges), |
55781
b3a4207fb9a6
proper update of text perspective for nodes with changed blobs, which is important to refresh the corresponding command perspective (otherwise it might refer to invalid thy_load commands and cause full execution of the node by the prover);
wenzelm
parents:
55778
diff
changeset
|
130 |
PIDE.editor.node_overlays(node_name))) |
52849 | 131 |
} |
57610 | 132 |
else (false, Document.Node.empty_perspective_text) |
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
133 |
} |
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
134 |
|
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44379
diff
changeset
|
135 |
|
54509
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
136 |
/* blob */ |
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
137 |
|
56746 | 138 |
private var _blob: Option[(Bytes, Symbol.Text_Chunk)] = None // owned by Swing thread |
54511 | 139 |
|
140 |
private def reset_blob(): Unit = Swing_Thread.require { _blob = None } |
|
141 |
||
55783 | 142 |
def get_blob(): Option[Document.Blob] = |
54511 | 143 |
Swing_Thread.require { |
55783 | 144 |
if (is_theory) None |
145 |
else { |
|
56473 | 146 |
val (bytes, chunk) = |
55783 | 147 |
_blob match { |
148 |
case Some(x) => x |
|
149 |
case None => |
|
56208 | 150 |
val bytes = PIDE.resources.file_content(buffer) |
56746 | 151 |
val chunk = Symbol.Text_Chunk(buffer.getSegment(0, buffer.getLength)) |
56473 | 152 |
_blob = Some((bytes, chunk)) |
153 |
(bytes, chunk) |
|
55783 | 154 |
} |
155 |
val changed = pending_edits.is_pending() |
|
56473 | 156 |
Some(Document.Blob(bytes, chunk, changed)) |
54511 | 157 |
} |
158 |
} |
|
54509
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
159 |
|
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
160 |
|
50363
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50344
diff
changeset
|
161 |
/* edits */ |
50344
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50207
diff
changeset
|
162 |
|
54461 | 163 |
def node_edits( |
56335
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
164 |
clear: Boolean, |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
165 |
text_edits: List[Text.Edit], |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
166 |
perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] = |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
167 |
get_blob() match { |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
168 |
case None => |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
169 |
val header_edit = session.header_edit(node_name, node_header()) |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
170 |
if (clear) |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
171 |
List(header_edit, |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
172 |
node_name -> Document.Node.Clear(), |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
173 |
node_name -> Document.Node.Edits(text_edits), |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
174 |
node_name -> perspective) |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
175 |
else |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
176 |
List(header_edit, |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
177 |
node_name -> Document.Node.Edits(text_edits), |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
178 |
node_name -> perspective) |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
179 |
case Some(blob) => |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
180 |
List(node_name -> Document.Node.Blob(blob), |
8953d4cc060a
store blob content within document node: aux. files that were once open are made persistent;
wenzelm
parents:
56314
diff
changeset
|
181 |
node_name -> Document.Node.Edits(text_edits)) |
54509
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54464
diff
changeset
|
182 |
} |
50363
2f8dc9e65401
tuned signature in accordance to document operations;
wenzelm
parents:
50344
diff
changeset
|
183 |
|
50344
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50207
diff
changeset
|
184 |
|
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50207
diff
changeset
|
185 |
/* pending edits */ |
43648 | 186 |
|
43644 | 187 |
private object pending_edits // owned by Swing thread |
38224 | 188 |
{ |
54461 | 189 |
private var pending_clear = false |
38425 | 190 |
private val pending = new mutable.ListBuffer[Text.Edit] |
57610 | 191 |
private var last_perspective = Document.Node.empty_perspective_text |
44438 | 192 |
|
55781
b3a4207fb9a6
proper update of text perspective for nodes with changed blobs, which is important to refresh the corresponding command perspective (otherwise it might refer to invalid thy_load commands and cause full execution of the node by the prover);
wenzelm
parents:
55778
diff
changeset
|
193 |
def is_pending(): Boolean = pending_clear || !pending.isEmpty |
38425 | 194 |
def snapshot(): List[Text.Edit] = pending.toList |
38224 | 195 |
|
55783 | 196 |
def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] = |
38224 | 197 |
{ |
54461 | 198 |
val clear = pending_clear |
47393
d760049b2d18
more robust update_perspective, e.g. required after reload of buffer that is not at start position;
wenzelm
parents:
47058
diff
changeset
|
199 |
val edits = snapshot() |
55783 | 200 |
val (reparse, perspective) = node_perspective(doc_blobs) |
55781
b3a4207fb9a6
proper update of text perspective for nodes with changed blobs, which is important to refresh the corresponding command perspective (otherwise it might refer to invalid thy_load commands and cause full execution of the node by the prover);
wenzelm
parents:
55778
diff
changeset
|
201 |
if (clear || reparse || !edits.isEmpty || last_perspective != perspective) { |
54461 | 202 |
pending_clear = false |
47393
d760049b2d18
more robust update_perspective, e.g. required after reload of buffer that is not at start position;
wenzelm
parents:
47058
diff
changeset
|
203 |
pending.clear |
54461 | 204 |
last_perspective = perspective |
205 |
node_edits(clear, edits, perspective) |
|
43648 | 206 |
} |
52759
a20631db9c8a
support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents:
50565
diff
changeset
|
207 |
else Nil |
38224 | 208 |
} |
209 |
||
54461 | 210 |
def edit(clear: Boolean, e: Text.Edit) |
38224 | 211 |
{ |
54511 | 212 |
reset_blob() |
213 |
||
54461 | 214 |
if (clear) { |
215 |
pending_clear = true |
|
216 |
pending.clear |
|
217 |
} |
|
218 |
pending += e |
|
219 |
PIDE.editor.invoke() |
|
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44385
diff
changeset
|
220 |
} |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44385
diff
changeset
|
221 |
} |
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44385
diff
changeset
|
222 |
|
54464 | 223 |
def snapshot(): Document.Snapshot = |
224 |
Swing_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) } |
|
34731
c0cb6bd10eec
keep BufferListener and TextAreaExtension private;
wenzelm
parents:
34724
diff
changeset
|
225 |
|
55783 | 226 |
def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] = |
227 |
Swing_Thread.require { pending_edits.flushed_edits(doc_blobs) } |
|
34828 | 228 |
|
229 |
||
230 |
/* buffer listener */ |
|
231 |
||
232 |
private val buffer_listener: BufferListener = new BufferAdapter |
|
233 |
{ |
|
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
234 |
override def bufferLoaded(buffer: JEditBuffer) |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
235 |
{ |
55791
5821b1937fa5
clarified init_models: simultaneous initialization of all document models, before flushing edits by regular means (via PIDE.editor.invoke) -- important for consolidated doc_blobs when determining initial edits;
wenzelm
parents:
55785
diff
changeset
|
236 |
pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))) |
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
237 |
} |
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
238 |
|
34828 | 239 |
override def contentInserted(buffer: JEditBuffer, |
240 |
start_line: Int, offset: Int, num_lines: Int, length: Int) |
|
241 |
{ |
|
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
242 |
if (!buffer.isLoading) |
54461 | 243 |
pending_edits.edit(false, Text.Edit.insert(offset, buffer.getText(offset, length))) |
34828 | 244 |
} |
245 |
||
246 |
override def preContentRemoved(buffer: JEditBuffer, |
|
38426 | 247 |
start_line: Int, offset: Int, num_lines: Int, removed_length: Int) |
34828 | 248 |
{ |
40478
4bae781b8f7c
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
wenzelm
parents:
40474
diff
changeset
|
249 |
if (!buffer.isLoading) |
54461 | 250 |
pending_edits.edit(false, Text.Edit.remove(offset, buffer.getText(offset, removed_length))) |
34828 | 251 |
} |
252 |
} |
|
253 |
||
254 |
||
38158 | 255 |
/* activation */ |
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37555
diff
changeset
|
256 |
|
43512 | 257 |
private def activate() |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
258 |
{ |
55791
5821b1937fa5
clarified init_models: simultaneous initialization of all document models, before flushing edits by regular means (via PIDE.editor.invoke) -- important for consolidated doc_blobs when determining initial edits;
wenzelm
parents:
55785
diff
changeset
|
259 |
pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))) |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
260 |
buffer.addBufferListener(buffer_listener) |
44358
2a2df4de1bbe
more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents:
44182
diff
changeset
|
261 |
Token_Markup.refresh_buffer(buffer) |
34680 | 262 |
} |
263 |
||
43512 | 264 |
private def deactivate() |
34680 | 265 |
{ |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34783
diff
changeset
|
266 |
buffer.removeBufferListener(buffer_listener) |
44358
2a2df4de1bbe
more robust initialization of token marker and line context wrt. session startup;
wenzelm
parents:
44182
diff
changeset
|
267 |
Token_Markup.refresh_buffer(buffer) |
34680 | 268 |
} |
34447 | 269 |
} |