src/Tools/jEdit/src/document_model.scala
author wenzelm
Sun Nov 17 16:02:06 2013 +0100 (2013-11-17)
changeset 54461 6c360a6ade0e
parent 54441 3d37b2957a3e
child 54464 b0074321bf14
permissions -rw-r--r--
centralized management of pending buffer edits;
wenzelm@43282
     1
/*  Title:      Tools/jEdit/src/document_model.scala
wenzelm@36760
     2
    Author:     Fabian Immler, TU Munich
wenzelm@36760
     3
    Author:     Makarius
wenzelm@36760
     4
wenzelm@38222
     5
Document model connected to jEdit buffer -- single node in theory graph.
wenzelm@36760
     6
*/
wenzelm@34407
     7
wenzelm@34784
     8
package isabelle.jedit
wenzelm@34760
     9
wenzelm@34318
    10
wenzelm@36015
    11
import isabelle._
wenzelm@36015
    12
wenzelm@34693
    13
import scala.collection.mutable
wenzelm@34446
    14
wenzelm@34784
    15
import org.gjt.sp.jedit.Buffer
wenzelm@34783
    16
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
wenzelm@34318
    17
wenzelm@34760
    18
wenzelm@34784
    19
object Document_Model
wenzelm@34588
    20
{
wenzelm@34784
    21
  /* document model of buffer */
wenzelm@34784
    22
wenzelm@50565
    23
  private val key = "PIDE.document_model"
wenzelm@34784
    24
wenzelm@34788
    25
  def apply(buffer: Buffer): Option[Document_Model] =
wenzelm@34784
    26
  {
wenzelm@38223
    27
    Swing_Thread.require()
wenzelm@34784
    28
    buffer.getProperty(key) match {
wenzelm@34784
    29
      case model: Document_Model => Some(model)
wenzelm@34784
    30
      case _ => None
wenzelm@34784
    31
    }
wenzelm@34784
    32
  }
wenzelm@34784
    33
wenzelm@34784
    34
  def exit(buffer: Buffer)
wenzelm@34784
    35
  {
wenzelm@38223
    36
    Swing_Thread.require()
wenzelm@34788
    37
    apply(buffer) match {
wenzelm@39636
    38
      case None =>
wenzelm@34784
    39
      case Some(model) =>
wenzelm@34784
    40
        model.deactivate()
wenzelm@34784
    41
        buffer.unsetProperty(key)
wenzelm@47058
    42
        buffer.propertiesChanged
immler@34653
    43
    }
wenzelm@34318
    44
  }
wenzelm@43397
    45
wenzelm@52973
    46
  def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
wenzelm@43397
    47
  {
wenzelm@47058
    48
    Swing_Thread.require()
wenzelm@47058
    49
    apply(buffer).map(_.deactivate)
wenzelm@52973
    50
    val model = new Document_Model(session, buffer, node_name)
wenzelm@43397
    51
    buffer.setProperty(key, model)
wenzelm@43397
    52
    model.activate()
wenzelm@47058
    53
    buffer.propertiesChanged
wenzelm@43397
    54
    model
wenzelm@43397
    55
  }
wenzelm@34318
    56
}
wenzelm@34318
    57
wenzelm@38151
    58
wenzelm@52973
    59
class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name)
wenzelm@34588
    60
{
wenzelm@44385
    61
  /* header */
wenzelm@38222
    62
wenzelm@48707
    63
  def node_header(): Document.Node.Header =
wenzelm@46920
    64
  {
wenzelm@46920
    65
    Swing_Thread.require()
wenzelm@49406
    66
    JEdit_Lib.buffer_lock(buffer) {
wenzelm@46748
    67
      Exn.capture {
wenzelm@52973
    68
        PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
wenzelm@48707
    69
      } match {
wenzelm@48707
    70
        case Exn.Res(header) => header
wenzelm@48707
    71
        case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
wenzelm@46748
    72
      }
wenzelm@46748
    73
    }
wenzelm@46920
    74
  }
wenzelm@44385
    75
wenzelm@44385
    76
wenzelm@44385
    77
  /* perspective */
wenzelm@44385
    78
wenzelm@52849
    79
  // owned by Swing thread
wenzelm@52816
    80
  private var _node_required = false
wenzelm@52816
    81
  def node_required: Boolean = _node_required
wenzelm@52816
    82
  def node_required_=(b: Boolean)
wenzelm@52816
    83
  {
wenzelm@52816
    84
    Swing_Thread.require()
wenzelm@52816
    85
    if (_node_required != b) {
wenzelm@52816
    86
      _node_required = b
wenzelm@52816
    87
      PIDE.options_changed()
wenzelm@52974
    88
      PIDE.editor.flush()
wenzelm@52816
    89
    }
wenzelm@52816
    90
  }
wenzelm@52808
    91
wenzelm@52849
    92
  val empty_perspective: Document.Node.Perspective_Text =
wenzelm@52887
    93
    Document.Node.Perspective(false, Text.Perspective.empty, Document.Node.Overlays.empty)
wenzelm@52849
    94
wenzelm@52808
    95
  def node_perspective(): Document.Node.Perspective_Text =
wenzelm@44385
    96
  {
wenzelm@44385
    97
    Swing_Thread.require()
wenzelm@52759
    98
wenzelm@52849
    99
    if (Isabelle.continuous_checking) {
wenzelm@54325
   100
      val snapshot = this.snapshot()
wenzelm@52849
   101
      Document.Node.Perspective(node_required, Text.Perspective(
wenzelm@52849
   102
        for {
wenzelm@52849
   103
          doc_view <- PIDE.document_views(buffer)
wenzelm@54325
   104
          range <- doc_view.perspective(snapshot).ranges
wenzelm@52977
   105
        } yield range), PIDE.editor.node_overlays(node_name))
wenzelm@52849
   106
    }
wenzelm@52849
   107
    else empty_perspective
wenzelm@44385
   108
  }
wenzelm@44385
   109
wenzelm@44385
   110
wenzelm@50363
   111
  /* edits */
wenzelm@50344
   112
wenzelm@50344
   113
  def init_edits(): List[Document.Edit_Text] =
wenzelm@50344
   114
  {
wenzelm@50344
   115
    Swing_Thread.require()
wenzelm@52815
   116
wenzelm@50344
   117
    val header = node_header()
wenzelm@50344
   118
    val text = JEdit_Lib.buffer_text(buffer)
wenzelm@50344
   119
    val perspective = node_perspective()
wenzelm@50344
   120
wenzelm@52973
   121
    List(session.header_edit(node_name, header),
wenzelm@52973
   122
      node_name -> Document.Node.Clear(),
wenzelm@52973
   123
      node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
wenzelm@52973
   124
      node_name -> perspective)
wenzelm@50344
   125
  }
wenzelm@50344
   126
wenzelm@54461
   127
  def node_edits(
wenzelm@54461
   128
    clear: Boolean,
wenzelm@54461
   129
    text_edits: List[Text.Edit],
wenzelm@54461
   130
    perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
wenzelm@50363
   131
  {
wenzelm@50363
   132
    Swing_Thread.require()
wenzelm@52815
   133
wenzelm@54461
   134
    val header_edit = session.header_edit(node_name, node_header())
wenzelm@54461
   135
    if (clear)
wenzelm@54461
   136
      List(header_edit,
wenzelm@54461
   137
        node_name -> Document.Node.Clear(),
wenzelm@54461
   138
        node_name -> Document.Node.Edits(text_edits),
wenzelm@54461
   139
        node_name -> perspective)
wenzelm@54461
   140
    else
wenzelm@54461
   141
      List(header_edit,
wenzelm@54461
   142
        node_name -> Document.Node.Edits(text_edits),
wenzelm@54461
   143
        node_name -> perspective)
wenzelm@50363
   144
  }
wenzelm@50363
   145
wenzelm@50344
   146
wenzelm@50344
   147
  /* pending edits */
wenzelm@43648
   148
wenzelm@43644
   149
  private object pending_edits  // owned by Swing thread
wenzelm@38224
   150
  {
wenzelm@54461
   151
    private var pending_clear = false
wenzelm@38425
   152
    private val pending = new mutable.ListBuffer[Text.Edit]
wenzelm@52849
   153
    private var last_perspective = empty_perspective
wenzelm@44438
   154
wenzelm@38425
   155
    def snapshot(): List[Text.Edit] = pending.toList
wenzelm@38224
   156
wenzelm@52759
   157
    def flushed_edits(): List[Document.Edit_Text] =
wenzelm@38224
   158
    {
wenzelm@38224
   159
      Swing_Thread.require()
wenzelm@44438
   160
wenzelm@54461
   161
      val clear = pending_clear
wenzelm@47393
   162
      val edits = snapshot()
wenzelm@54461
   163
      val perspective = node_perspective()
wenzelm@54461
   164
      if (clear || !edits.isEmpty || last_perspective != perspective) {
wenzelm@54461
   165
        pending_clear = false
wenzelm@47393
   166
        pending.clear
wenzelm@54461
   167
        last_perspective = perspective
wenzelm@54461
   168
        node_edits(clear, edits, perspective)
wenzelm@43648
   169
      }
wenzelm@52759
   170
      else Nil
wenzelm@38224
   171
    }
wenzelm@38224
   172
wenzelm@54461
   173
    def edit(clear: Boolean, e: Text.Edit)
wenzelm@38224
   174
    {
wenzelm@38224
   175
      Swing_Thread.require()
wenzelm@44436
   176
wenzelm@54461
   177
      if (clear) {
wenzelm@54461
   178
        pending_clear = true
wenzelm@54461
   179
        pending.clear
wenzelm@54461
   180
      }
wenzelm@54461
   181
      pending += e
wenzelm@54461
   182
      PIDE.editor.invoke()
wenzelm@44436
   183
    }
wenzelm@44436
   184
  }
wenzelm@44436
   185
wenzelm@52759
   186
  def flushed_edits(): List[Document.Edit_Text] = pending_edits.flushed_edits()
wenzelm@52767
   187
wenzelm@38152
   188
wenzelm@38152
   189
  /* snapshot */
wenzelm@34731
   190
wenzelm@38417
   191
  def snapshot(): Document.Snapshot =
wenzelm@38417
   192
  {
wenzelm@38223
   193
    Swing_Thread.require()
wenzelm@52973
   194
    session.snapshot(node_name, pending_edits.snapshot())
wenzelm@38223
   195
  }
wenzelm@34828
   196
wenzelm@34828
   197
wenzelm@34828
   198
  /* buffer listener */
wenzelm@34828
   199
wenzelm@34828
   200
  private val buffer_listener: BufferListener = new BufferAdapter
wenzelm@34828
   201
  {
wenzelm@40478
   202
    override def bufferLoaded(buffer: JEditBuffer)
wenzelm@40478
   203
    {
wenzelm@54461
   204
      pending_edits.edit(true, Text.Edit.insert(0, buffer.getText(0, buffer.getLength)))
wenzelm@40478
   205
    }
wenzelm@40478
   206
wenzelm@34828
   207
    override def contentInserted(buffer: JEditBuffer,
wenzelm@34828
   208
      start_line: Int, offset: Int, num_lines: Int, length: Int)
wenzelm@34828
   209
    {
wenzelm@40478
   210
      if (!buffer.isLoading)
wenzelm@54461
   211
        pending_edits.edit(false, Text.Edit.insert(offset, buffer.getText(offset, length)))
wenzelm@34828
   212
    }
wenzelm@34828
   213
wenzelm@34828
   214
    override def preContentRemoved(buffer: JEditBuffer,
wenzelm@38426
   215
      start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
wenzelm@34828
   216
    {
wenzelm@40478
   217
      if (!buffer.isLoading)
wenzelm@54461
   218
        pending_edits.edit(false, Text.Edit.remove(offset, buffer.getText(offset, removed_length)))
wenzelm@34828
   219
    }
wenzelm@34828
   220
  }
wenzelm@34828
   221
wenzelm@34828
   222
wenzelm@38158
   223
  /* activation */
wenzelm@37557
   224
wenzelm@43512
   225
  private def activate()
wenzelm@34784
   226
  {
wenzelm@34784
   227
    buffer.addBufferListener(buffer_listener)
wenzelm@44358
   228
    Token_Markup.refresh_buffer(buffer)
immler@34680
   229
  }
immler@34680
   230
wenzelm@43512
   231
  private def deactivate()
immler@34680
   232
  {
wenzelm@34784
   233
    buffer.removeBufferListener(buffer_listener)
wenzelm@44358
   234
    Token_Markup.refresh_buffer(buffer)
immler@34680
   235
  }
wenzelm@34447
   236
}