emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
--- a/src/Pure/System/session.scala Tue Dec 04 11:06:51 2012 +0100
+++ b/src/Pure/System/session.scala Tue Dec 04 15:47:37 2012 +0100
@@ -468,15 +468,6 @@
def edit(edits: List[Document.Edit_Text])
{ session_actor !? Session.Raw_Edits(edits) }
- def init_node(name: Document.Node.Name,
- header: Document.Node.Header, perspective: Text.Perspective, text: String)
- {
- edit(List(header_edit(name, header),
- name -> Document.Node.Clear(),
- name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
- name -> Document.Node.Perspective(perspective)))
- }
-
def edit_node(name: Document.Node.Name,
header: Document.Node.Header, perspective: Text.Perspective, text_edits: List[Text.Edit])
{
--- a/src/Tools/jEdit/src/document_model.scala Tue Dec 04 11:06:51 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Tue Dec 04 15:47:37 2012 +0100
@@ -81,7 +81,7 @@
def buffer_range(): Text.Range = Text.Range(0, (buffer.getLength - 1) max 0)
- def perspective(): Text.Perspective =
+ def node_perspective(): Text.Perspective =
{
Swing_Thread.require()
Text.Perspective(
@@ -92,7 +92,23 @@
}
- /* pending text edits */
+ /* initial edits */
+
+ def init_edits(): List[Document.Edit_Text] =
+ {
+ Swing_Thread.require()
+ val header = node_header()
+ val text = JEdit_Lib.buffer_text(buffer)
+ val perspective = node_perspective()
+
+ List(session.header_edit(name, header),
+ name -> Document.Node.Clear(),
+ name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
+ name -> Document.Node.Perspective(perspective))
+ }
+
+
+ /* pending edits */
private object pending_edits // owned by Swing thread
{
@@ -106,7 +122,7 @@
Swing_Thread.require()
val edits = snapshot()
- val new_perspective = perspective()
+ val new_perspective = node_perspective()
if (!edits.isEmpty || last_perspective != new_perspective) {
pending.clear
last_perspective = new_perspective
@@ -132,7 +148,7 @@
def init()
{
flush()
- session.init_node(name, node_header(), perspective(), JEdit_Lib.buffer_text(buffer))
+ session.edit(init_edits())
}
def exit()
@@ -194,7 +210,7 @@
private def activate()
{
buffer.addBufferListener(buffer_listener)
- pending_edits.init()
+ pending_edits.flush()
Token_Markup.refresh_buffer(buffer)
}
--- a/src/Tools/jEdit/src/plugin.scala Tue Dec 04 11:06:51 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Tue Dec 04 15:47:37 2012 +0100
@@ -58,32 +58,44 @@
if doc_view.isDefined
} yield doc_view.get
- def exit_model(buffer: Buffer)
+ def exit_models(buffers: List[Buffer])
{
- JEdit_Lib.swing_buffer_lock(buffer) {
- JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
- Document_Model.exit(buffer)
- }
+ Swing_Thread.now {
+ buffers.foreach(buffer =>
+ JEdit_Lib.buffer_lock(buffer) {
+ JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
+ Document_Model.exit(buffer)
+ })
+ }
}
- def init_model(buffer: Buffer)
+ def init_models(buffers: List[Buffer])
{
- JEdit_Lib.swing_buffer_lock(buffer) {
- val opt_model =
- JEdit_Lib.buffer_node_name(buffer) match {
- case Some(node_name) =>
- document_model(buffer) match {
- case Some(model) if model.name == node_name => Some(model)
- case _ => Some(Document_Model.init(session, buffer, node_name))
+ Swing_Thread.now {
+ val init_edits =
+ (List.empty[Document.Edit_Text] /: buffers) { case (edits, buffer) =>
+ JEdit_Lib.buffer_lock(buffer) {
+ val (model_edits, opt_model) =
+ JEdit_Lib.buffer_node_name(buffer) match {
+ case Some(node_name) =>
+ document_model(buffer) match {
+ case Some(model) if model.name == node_name => (Nil, Some(model))
+ case _ =>
+ val model = Document_Model.init(session, buffer, node_name)
+ (model.init_edits(), Some(model))
+ }
+ case None => (Nil, None)
+ }
+ if (opt_model.isDefined) {
+ for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
+ if (document_view(text_area).map(_.model) != opt_model)
+ Document_View.init(opt_model.get, text_area)
+ }
}
- case None => None
+ model_edits ::: edits
+ }
}
- if (opt_model.isDefined) {
- for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
- if (document_view(text_area).map(_.model) != opt_model)
- Document_View.init(opt_model.get, text_area)
- }
- }
+ PIDE.session.edit(init_edits)
}
}
@@ -123,6 +135,12 @@
{
/* theory files */
+ private lazy val delay_init =
+ Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
+ {
+ PIDE.init_models(JEdit_Lib.jedit_buffers().toList)
+ }
+
private lazy val delay_load =
Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay"))
{
@@ -179,11 +197,11 @@
case Session.Ready =>
PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
- JEdit_Lib.jedit_buffers.foreach(PIDE.init_model)
+ PIDE.init_models(JEdit_Lib.jedit_buffers().toList)
Swing_Thread.later { delay_load.invoke() }
case Session.Shutdown =>
- JEdit_Lib.jedit_buffers.foreach(PIDE.exit_model)
+ PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
Swing_Thread.later { delay_load.revoke() }
case _ =>
@@ -221,7 +239,7 @@
if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
if (PIDE.session.is_ready) {
val buffer = msg.getBuffer
- if (buffer != null && !buffer.isLoading) PIDE.init_model(buffer)
+ if (buffer != null && !buffer.isLoading) delay_init.invoke()
Swing_Thread.later { delay_load.invoke() }
}
@@ -289,7 +307,7 @@
PIDE.options.value.save_prefs()
PIDE.session.phase_changed -= session_manager
- JEdit_Lib.jedit_buffers.foreach(PIDE.exit_model)
+ PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
PIDE.session.stop()
}
}