centralized management of pending buffer edits;
authorwenzelm
Sun Nov 17 16:02:06 2013 +0100 (2013-11-17)
changeset 544616c360a6ade0e
parent 54460 949a612097fb
child 54462 c9bb76303348
centralized management of pending buffer edits;
src/Pure/PIDE/editor.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/editor.scala	Sun Nov 17 09:30:13 2013 +0100
     1.2 +++ b/src/Pure/PIDE/editor.scala	Sun Nov 17 16:02:06 2013 +0100
     1.3 @@ -11,6 +11,7 @@
     1.4  {
     1.5    def session: Session
     1.6    def flush(): Unit
     1.7 +  def invoke(): Unit
     1.8    def current_context: Context
     1.9    def current_node(context: Context): Option[Document.Node.Name]
    1.10    def current_node_snapshot(context: Context): Option[Document.Snapshot]
     2.1 --- a/src/Tools/jEdit/src/document_model.scala	Sun Nov 17 09:30:13 2013 +0100
     2.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sun Nov 17 16:02:06 2013 +0100
     2.3 @@ -124,16 +124,23 @@
     2.4        node_name -> perspective)
     2.5    }
     2.6  
     2.7 -  def node_edits(perspective: Document.Node.Perspective_Text, text_edits: List[Text.Edit])
     2.8 -    : List[Document.Edit_Text] =
     2.9 +  def node_edits(
    2.10 +    clear: Boolean,
    2.11 +    text_edits: List[Text.Edit],
    2.12 +    perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
    2.13    {
    2.14      Swing_Thread.require()
    2.15  
    2.16 -    val header = node_header()
    2.17 -
    2.18 -    List(session.header_edit(node_name, header),
    2.19 -      node_name -> Document.Node.Edits(text_edits),
    2.20 -      node_name -> perspective)
    2.21 +    val header_edit = session.header_edit(node_name, node_header())
    2.22 +    if (clear)
    2.23 +      List(header_edit,
    2.24 +        node_name -> Document.Node.Clear(),
    2.25 +        node_name -> Document.Node.Edits(text_edits),
    2.26 +        node_name -> perspective)
    2.27 +    else
    2.28 +      List(header_edit,
    2.29 +        node_name -> Document.Node.Edits(text_edits),
    2.30 +        node_name -> perspective)
    2.31    }
    2.32  
    2.33  
    2.34 @@ -141,6 +148,7 @@
    2.35  
    2.36    private object pending_edits  // owned by Swing thread
    2.37    {
    2.38 +    private var pending_clear = false
    2.39      private val pending = new mutable.ListBuffer[Text.Edit]
    2.40      private var last_perspective = empty_perspective
    2.41  
    2.42 @@ -150,45 +158,33 @@
    2.43      {
    2.44        Swing_Thread.require()
    2.45  
    2.46 +      val clear = pending_clear
    2.47        val edits = snapshot()
    2.48 -      val new_perspective = node_perspective()
    2.49 -      if (!edits.isEmpty || last_perspective != new_perspective) {
    2.50 +      val perspective = node_perspective()
    2.51 +      if (clear || !edits.isEmpty || last_perspective != perspective) {
    2.52 +        pending_clear = false
    2.53          pending.clear
    2.54 -        last_perspective = new_perspective
    2.55 -        node_edits(new_perspective, edits)
    2.56 +        last_perspective = perspective
    2.57 +        node_edits(clear, edits, perspective)
    2.58        }
    2.59        else Nil
    2.60      }
    2.61  
    2.62 -    def flush(): Unit = session.update(flushed_edits())
    2.63 -
    2.64 -    val delay_flush =
    2.65 -      Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
    2.66 -
    2.67 -    def +=(edit: Text.Edit)
    2.68 +    def edit(clear: Boolean, e: Text.Edit)
    2.69      {
    2.70        Swing_Thread.require()
    2.71 -      pending += edit
    2.72 -      delay_flush.invoke()
    2.73 -    }
    2.74  
    2.75 -    def init()
    2.76 -    {
    2.77 -      flush()
    2.78 -      session.update(init_edits())
    2.79 -    }
    2.80 -
    2.81 -    def exit()
    2.82 -    {
    2.83 -      delay_flush.revoke()
    2.84 -      flush()
    2.85 +      if (clear) {
    2.86 +        pending_clear = true
    2.87 +        pending.clear
    2.88 +      }
    2.89 +      pending += e
    2.90 +      PIDE.editor.invoke()
    2.91      }
    2.92    }
    2.93  
    2.94    def flushed_edits(): List[Document.Edit_Text] = pending_edits.flushed_edits()
    2.95  
    2.96 -  def update_perspective(): Unit = pending_edits.delay_flush.invoke()
    2.97 -
    2.98  
    2.99    /* snapshot */
   2.100  
   2.101 @@ -205,21 +201,21 @@
   2.102    {
   2.103      override def bufferLoaded(buffer: JEditBuffer)
   2.104      {
   2.105 -      pending_edits.init()
   2.106 +      pending_edits.edit(true, Text.Edit.insert(0, buffer.getText(0, buffer.getLength)))
   2.107      }
   2.108  
   2.109      override def contentInserted(buffer: JEditBuffer,
   2.110        start_line: Int, offset: Int, num_lines: Int, length: Int)
   2.111      {
   2.112        if (!buffer.isLoading)
   2.113 -        pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
   2.114 +        pending_edits.edit(false, Text.Edit.insert(offset, buffer.getText(offset, length)))
   2.115      }
   2.116  
   2.117      override def preContentRemoved(buffer: JEditBuffer,
   2.118        start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
   2.119      {
   2.120        if (!buffer.isLoading)
   2.121 -        pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
   2.122 +        pending_edits.edit(false, Text.Edit.remove(offset, buffer.getText(offset, removed_length)))
   2.123      }
   2.124    }
   2.125  
   2.126 @@ -229,13 +225,11 @@
   2.127    private def activate()
   2.128    {
   2.129      buffer.addBufferListener(buffer_listener)
   2.130 -    pending_edits.flush()
   2.131      Token_Markup.refresh_buffer(buffer)
   2.132    }
   2.133  
   2.134    private def deactivate()
   2.135    {
   2.136 -    pending_edits.exit()
   2.137      buffer.removeBufferListener(buffer_listener)
   2.138      Token_Markup.refresh_buffer(buffer)
   2.139    }
     3.1 --- a/src/Tools/jEdit/src/document_view.scala	Sun Nov 17 09:30:13 2013 +0100
     3.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sun Nov 17 16:02:06 2013 +0100
     3.3 @@ -106,14 +106,14 @@
     3.4      Text.Perspective(active_command ::: visible_lines)
     3.5    }
     3.6  
     3.7 -  private def update_perspective = new TextAreaExtension
     3.8 +  private def update_view = new TextAreaExtension
     3.9    {
    3.10      override def paintScreenLineRange(gfx: Graphics2D,
    3.11        first_line: Int, last_line: Int, physical_lines: Array[Int],
    3.12        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    3.13      {
    3.14        // no robust_body
    3.15 -      model.update_perspective()
    3.16 +      PIDE.editor.invoke()
    3.17      }
    3.18    }
    3.19  
    3.20 @@ -251,7 +251,7 @@
    3.21    {
    3.22      val painter = text_area.getPainter
    3.23  
    3.24 -    painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
    3.25 +    painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_view)
    3.26      rich_text_area.activate()
    3.27      text_area.getGutter.addExtension(gutter_painter)
    3.28      text_area.addKeyListener(key_listener)
    3.29 @@ -272,6 +272,6 @@
    3.30      text_area.removeKeyListener(key_listener)
    3.31      text_area.getGutter.removeExtension(gutter_painter)
    3.32      rich_text_area.deactivate()
    3.33 -    painter.removeExtension(update_perspective)
    3.34 +    painter.removeExtension(update_view)
    3.35    }
    3.36  }
     4.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Nov 17 09:30:13 2013 +0100
     4.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Nov 17 16:02:06 2013 +0100
     4.3 @@ -36,6 +36,11 @@
     4.4      )
     4.5    }
     4.6  
     4.7 +  private val delay_flush =
     4.8 +    Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
     4.9 +
    4.10 +  def invoke(): Unit = Swing_Thread.require { delay_flush.invoke() }
    4.11 +
    4.12  
    4.13    /* current situation */
    4.14  
     5.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Nov 17 09:30:13 2013 +0100
     5.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Nov 17 16:02:06 2013 +0100
     5.3 @@ -80,6 +80,7 @@
     5.4    def exit_models(buffers: List[Buffer])
     5.5    {
     5.6      Swing_Thread.now {
     5.7 +      PIDE.editor.flush()
     5.8        buffers.foreach(buffer =>
     5.9          JEdit_Lib.buffer_lock(buffer) {
    5.10            JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
    5.11 @@ -91,6 +92,7 @@
    5.12    def init_models(buffers: List[Buffer])
    5.13    {
    5.14      Swing_Thread.now {
    5.15 +      PIDE.editor.flush()
    5.16        val init_edits =
    5.17          (List.empty[Document.Edit_Text] /: buffers) { case (edits, buffer) =>
    5.18            JEdit_Lib.buffer_lock(buffer) {