clarified buffer events: exit model while loading;
authorwenzelm
Sat Jan 07 15:16:36 2017 +0100 (2017-01-07)
changeset 6481867a0a563d2b3
parent 64817 0bb6b582bb4f
child 64819 bebe7a164068
clarified buffer events: exit model while loading;
misc tuning;
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 14:34:53 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 15:16:36 2017 +0100
     1.3 @@ -279,11 +279,11 @@
     1.4          get_blob match {
     1.5            case None =>
     1.6              List(session.header_edit(node_name, node_header),
     1.7 -              node_name -> Document.Node.Edits(pending_edits.toList),
     1.8 +              node_name -> Document.Node.Edits(pending_edits),
     1.9                node_name -> perspective)
    1.10            case Some(blob) =>
    1.11              List(node_name -> Document.Node.Blob(blob),
    1.12 -              node_name -> Document.Node.Edits(pending_edits.toList))
    1.13 +              node_name -> Document.Node.Edits(pending_edits))
    1.14          }
    1.15        Some((edits, copy(last_perspective = perspective, pending_edits = Nil)))
    1.16      }
    1.17 @@ -294,7 +294,7 @@
    1.18    /* snapshot */
    1.19  
    1.20    def is_stable: Boolean = pending_edits.isEmpty
    1.21 -  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.toList)
    1.22 +  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
    1.23  }
    1.24  
    1.25  case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer)
    1.26 @@ -368,7 +368,7 @@
    1.27                _blob = Some((bytes, chunk))
    1.28                (bytes, chunk)
    1.29            }
    1.30 -        val changed = pending_edits.is_pending()
    1.31 +        val changed = pending_edits.nonEmpty
    1.32          Some(Document.Blob(bytes, chunk, changed))
    1.33        }
    1.34      }
    1.35 @@ -398,24 +398,15 @@
    1.36  
    1.37    /* edits */
    1.38  
    1.39 -  def node_edits(
    1.40 -      clear: Boolean,
    1.41 -      text_edits: List[Text.Edit],
    1.42 -      perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
    1.43 +  def node_edits(text_edits: List[Text.Edit], perspective: Document.Node.Perspective_Text)
    1.44 +    : List[Document.Edit_Text] =
    1.45    {
    1.46      val edits: List[Document.Edit_Text] =
    1.47        get_blob match {
    1.48          case None =>
    1.49 -          val header_edit = session.header_edit(node_name, node_header())
    1.50 -          if (clear)
    1.51 -            List(header_edit,
    1.52 -              node_name -> Document.Node.Clear(),
    1.53 -              node_name -> Document.Node.Edits(text_edits),
    1.54 -              node_name -> perspective)
    1.55 -          else
    1.56 -            List(header_edit,
    1.57 -              node_name -> Document.Node.Edits(text_edits),
    1.58 -              node_name -> perspective)
    1.59 +          List(session.header_edit(node_name, node_header()),
    1.60 +            node_name -> Document.Node.Edits(text_edits),
    1.61 +            node_name -> perspective)
    1.62          case Some(blob) =>
    1.63            List(node_name -> Document.Node.Blob(blob),
    1.64              node_name -> Document.Node.Edits(text_edits))
    1.65 @@ -428,12 +419,11 @@
    1.66  
    1.67    private object pending_edits
    1.68    {
    1.69 -    private var pending_clear = false
    1.70      private val pending = new mutable.ListBuffer[Text.Edit]
    1.71      private var last_perspective = Document.Node.no_perspective_text
    1.72  
    1.73 -    def is_pending(): Boolean = synchronized { pending_clear || pending.nonEmpty }
    1.74 -    def get_edits(): List[Text.Edit] = synchronized { pending.toList }
    1.75 +    def nonEmpty: Boolean = synchronized { pending.nonEmpty }
    1.76 +    def get_edits: List[Text.Edit] = synchronized { pending.toList }
    1.77      def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective }
    1.78      def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit =
    1.79        synchronized { last_perspective = perspective }
    1.80 @@ -442,19 +432,17 @@
    1.81        synchronized {
    1.82          GUI_Thread.require {}
    1.83  
    1.84 -        val clear = pending_clear
    1.85 -        val edits = get_edits()
    1.86 +        val edits = get_edits
    1.87          val (reparse, perspective) = node_perspective(doc_blobs, hidden)
    1.88 -        if (clear || reparse || edits.nonEmpty || last_perspective != perspective) {
    1.89 -          pending_clear = false
    1.90 +        if (reparse || edits.nonEmpty || last_perspective != perspective) {
    1.91            pending.clear
    1.92            last_perspective = perspective
    1.93 -          node_edits(clear, edits, perspective)
    1.94 +          node_edits(edits, perspective)
    1.95          }
    1.96          else Nil
    1.97        }
    1.98  
    1.99 -    def edit(clear: Boolean, e: Text.Edit): Unit = synchronized
   1.100 +    def edit(edits: List[Text.Edit]): Unit = synchronized
   1.101      {
   1.102        GUI_Thread.require {}
   1.103  
   1.104 @@ -464,17 +452,13 @@
   1.105        for (doc_view <- PIDE.document_views(buffer))
   1.106          doc_view.rich_text_area.active_reset()
   1.107  
   1.108 -      if (clear) {
   1.109 -        pending_clear = true
   1.110 -        pending.clear
   1.111 -      }
   1.112 -      pending += e
   1.113 +      pending ++= edits
   1.114        PIDE.editor.invoke()
   1.115      }
   1.116    }
   1.117  
   1.118 -  def is_stable(): Boolean = !pending_edits.is_pending();
   1.119 -  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits())
   1.120 +  def is_stable(): Boolean = !pending_edits.nonEmpty
   1.121 +  def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits)
   1.122  
   1.123    def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
   1.124      pending_edits.flush_edits(doc_blobs, hidden)
   1.125 @@ -484,23 +468,16 @@
   1.126  
   1.127    private val buffer_listener: BufferListener = new BufferAdapter
   1.128    {
   1.129 -    override def bufferLoaded(buffer: JEditBuffer)
   1.130 -    {
   1.131 -      pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
   1.132 -    }
   1.133 -
   1.134      override def contentInserted(buffer: JEditBuffer,
   1.135        start_line: Int, offset: Int, num_lines: Int, length: Int)
   1.136      {
   1.137 -      if (!buffer.isLoading)
   1.138 -        pending_edits.edit(false, Text.Edit.insert(offset, buffer.getText(offset, length)))
   1.139 +      pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length))))
   1.140      }
   1.141  
   1.142      override def preContentRemoved(buffer: JEditBuffer,
   1.143        start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
   1.144      {
   1.145 -      if (!buffer.isLoading)
   1.146 -        pending_edits.edit(false, Text.Edit.remove(offset, buffer.getText(offset, removed_length)))
   1.147 +      pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
   1.148      }
   1.149    }
   1.150  
   1.151 @@ -535,15 +512,13 @@
   1.152  
   1.153      old_model match {
   1.154        case None =>
   1.155 -        pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
   1.156 +        pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
   1.157        case Some(file_model) =>
   1.158          set_node_required(file_model.node_required)
   1.159          pending_edits.set_last_perspective(file_model.last_perspective)
   1.160 -        for {
   1.161 -          edit <-
   1.162 -            file_model.pending_edits :::
   1.163 -              Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer))
   1.164 -        } pending_edits.edit(false, edit)
   1.165 +        pending_edits.edit(
   1.166 +          file_model.pending_edits :::
   1.167 +            Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer)))
   1.168      }
   1.169  
   1.170      buffer.addBufferListener(buffer_listener)
   1.171 @@ -564,6 +539,6 @@
   1.172  
   1.173      val content = Document_Model.File_Content(JEdit_Lib.buffer_text(buffer))
   1.174      File_Model(session, node_name, content, node_required,
   1.175 -      pending_edits.get_last_perspective, pending_edits.get_edits())
   1.176 +      pending_edits.get_last_perspective, pending_edits.get_edits)
   1.177    }
   1.178  }
     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Jan 07 14:34:53 2017 +0100
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Jan 07 15:16:36 2017 +0100
     2.3 @@ -322,13 +322,11 @@
     2.4              JEdit_Sessions.session_info().open_root).foreach(_.follow(view))
     2.5  
     2.6          case msg: BufferUpdate
     2.7 -        if msg.getWhat == BufferUpdate.LOADED ||
     2.8 -          msg.getWhat == BufferUpdate.PROPERTIES_CHANGED ||
     2.9 -          msg.getWhat == BufferUpdate.CLOSING =>
    2.10 +        if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
    2.11 +          if (msg.getBuffer != null) PIDE.exit_models(List(msg.getBuffer))
    2.12  
    2.13 -          if (msg.getWhat == BufferUpdate.CLOSING && msg.getBuffer != null)
    2.14 -            PIDE.exit_models(List(msg.getBuffer))
    2.15 -
    2.16 +        case msg: BufferUpdate
    2.17 +        if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || msg.getWhat == BufferUpdate.LOADED =>
    2.18            if (PIDE.session.is_ready) {
    2.19              delay_init.invoke()
    2.20              delay_load.invoke()