# HG changeset patch # User wenzelm # Date 1384700526 -3600 # Node ID 6c360a6ade0e35dc46a293b8a67a62d3e4a58fe4 # Parent 949a612097fb2a87ce437ebc6a92bcb43f6681fb centralized management of pending buffer edits; diff -r 949a612097fb -r 6c360a6ade0e src/Pure/PIDE/editor.scala --- a/src/Pure/PIDE/editor.scala Sun Nov 17 09:30:13 2013 +0100 +++ b/src/Pure/PIDE/editor.scala Sun Nov 17 16:02:06 2013 +0100 @@ -11,6 +11,7 @@ { def session: Session def flush(): Unit + def invoke(): Unit def current_context: Context def current_node(context: Context): Option[Document.Node.Name] def current_node_snapshot(context: Context): Option[Document.Snapshot] diff -r 949a612097fb -r 6c360a6ade0e src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Sun Nov 17 09:30:13 2013 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Sun Nov 17 16:02:06 2013 +0100 @@ -124,16 +124,23 @@ node_name -> perspective) } - def node_edits(perspective: Document.Node.Perspective_Text, text_edits: List[Text.Edit]) - : List[Document.Edit_Text] = + def node_edits( + clear: Boolean, + text_edits: List[Text.Edit], + perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] = { Swing_Thread.require() - val header = node_header() - - List(session.header_edit(node_name, header), - node_name -> Document.Node.Edits(text_edits), - node_name -> perspective) + val header_edit = session.header_edit(node_name, node_header()) + if (clear) + List(header_edit, + node_name -> Document.Node.Clear(), + node_name -> Document.Node.Edits(text_edits), + node_name -> perspective) + else + List(header_edit, + node_name -> Document.Node.Edits(text_edits), + node_name -> perspective) } @@ -141,6 +148,7 @@ private object pending_edits // owned by Swing thread { + private var pending_clear = false private val pending = new mutable.ListBuffer[Text.Edit] private var last_perspective = empty_perspective @@ -150,45 +158,33 @@ { Swing_Thread.require() + val clear = pending_clear val edits = snapshot() - val new_perspective = node_perspective() - if (!edits.isEmpty || last_perspective != new_perspective) { + val perspective = node_perspective() + if (clear || !edits.isEmpty || last_perspective != perspective) { + pending_clear = false pending.clear - last_perspective = new_perspective - node_edits(new_perspective, edits) + last_perspective = perspective + node_edits(clear, edits, perspective) } else Nil } - def flush(): Unit = session.update(flushed_edits()) - - val delay_flush = - Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } - - def +=(edit: Text.Edit) + def edit(clear: Boolean, e: Text.Edit) { Swing_Thread.require() - pending += edit - delay_flush.invoke() - } - def init() - { - flush() - session.update(init_edits()) - } - - def exit() - { - delay_flush.revoke() - flush() + if (clear) { + pending_clear = true + pending.clear + } + pending += e + PIDE.editor.invoke() } } def flushed_edits(): List[Document.Edit_Text] = pending_edits.flushed_edits() - def update_perspective(): Unit = pending_edits.delay_flush.invoke() - /* snapshot */ @@ -205,21 +201,21 @@ { override def bufferLoaded(buffer: JEditBuffer) { - pending_edits.init() + pending_edits.edit(true, Text.Edit.insert(0, buffer.getText(0, buffer.getLength))) } override def contentInserted(buffer: JEditBuffer, start_line: Int, offset: Int, num_lines: Int, length: Int) { if (!buffer.isLoading) - pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length)) + pending_edits.edit(false, Text.Edit.insert(offset, buffer.getText(offset, length))) } override def preContentRemoved(buffer: JEditBuffer, start_line: Int, offset: Int, num_lines: Int, removed_length: Int) { if (!buffer.isLoading) - pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length)) + pending_edits.edit(false, Text.Edit.remove(offset, buffer.getText(offset, removed_length))) } } @@ -229,13 +225,11 @@ private def activate() { buffer.addBufferListener(buffer_listener) - pending_edits.flush() Token_Markup.refresh_buffer(buffer) } private def deactivate() { - pending_edits.exit() buffer.removeBufferListener(buffer_listener) Token_Markup.refresh_buffer(buffer) } diff -r 949a612097fb -r 6c360a6ade0e src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Sun Nov 17 09:30:13 2013 +0100 +++ b/src/Tools/jEdit/src/document_view.scala Sun Nov 17 16:02:06 2013 +0100 @@ -106,14 +106,14 @@ Text.Perspective(active_command ::: visible_lines) } - private def update_perspective = new TextAreaExtension + private def update_view = new TextAreaExtension { override def paintScreenLineRange(gfx: Graphics2D, first_line: Int, last_line: Int, physical_lines: Array[Int], start: Array[Int], end: Array[Int], y: Int, line_height: Int) { // no robust_body - model.update_perspective() + PIDE.editor.invoke() } } @@ -251,7 +251,7 @@ { val painter = text_area.getPainter - painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective) + painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_view) rich_text_area.activate() text_area.getGutter.addExtension(gutter_painter) text_area.addKeyListener(key_listener) @@ -272,6 +272,6 @@ text_area.removeKeyListener(key_listener) text_area.getGutter.removeExtension(gutter_painter) rich_text_area.deactivate() - painter.removeExtension(update_perspective) + painter.removeExtension(update_view) } } diff -r 949a612097fb -r 6c360a6ade0e src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Sun Nov 17 09:30:13 2013 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Sun Nov 17 16:02:06 2013 +0100 @@ -36,6 +36,11 @@ ) } + private val delay_flush = + Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } + + def invoke(): Unit = Swing_Thread.require { delay_flush.invoke() } + /* current situation */ diff -r 949a612097fb -r 6c360a6ade0e src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Sun Nov 17 09:30:13 2013 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Sun Nov 17 16:02:06 2013 +0100 @@ -80,6 +80,7 @@ def exit_models(buffers: List[Buffer]) { Swing_Thread.now { + PIDE.editor.flush() buffers.foreach(buffer => JEdit_Lib.buffer_lock(buffer) { JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit) @@ -91,6 +92,7 @@ def init_models(buffers: List[Buffer]) { Swing_Thread.now { + PIDE.editor.flush() val init_edits = (List.empty[Document.Edit_Text] /: buffers) { case (edits, buffer) => JEdit_Lib.buffer_lock(buffer) {