# HG changeset patch # User wenzelm # Date 1354632457 -3600 # Node ID 608265769ce02c594668dd4ced34b1f2bb8bb94d # Parent 0c65a7cfc0f3c815c92ed98e13c4982b7c3b8c35 emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads); diff -r 0c65a7cfc0f3 -r 608265769ce0 src/Pure/System/session.scala --- 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]) { diff -r 0c65a7cfc0f3 -r 608265769ce0 src/Tools/jEdit/src/document_model.scala --- 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) } diff -r 0c65a7cfc0f3 -r 608265769ce0 src/Tools/jEdit/src/plugin.scala --- 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() } }