src/Tools/jEdit/src/document_model.scala
author wenzelm
Fri Aug 02 14:26:09 2013 +0200 (2013-08-02)
changeset 52849 199e9fa5a5c2
parent 52816 c608e0ade554
child 52858 863581a704a6
permissions -rw-r--r--
maintain overlays within node perspective;
tuned signature;
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@38158
    17
import org.gjt.sp.jedit.textarea.TextArea
wenzelm@38158
    18
wenzelm@38158
    19
import java.awt.font.TextAttribute
wenzelm@34318
    20
wenzelm@34760
    21
wenzelm@34784
    22
object Document_Model
wenzelm@34588
    23
{
wenzelm@34784
    24
  /* document model of buffer */
wenzelm@34784
    25
wenzelm@50565
    26
  private val key = "PIDE.document_model"
wenzelm@34784
    27
wenzelm@34788
    28
  def apply(buffer: Buffer): Option[Document_Model] =
wenzelm@34784
    29
  {
wenzelm@38223
    30
    Swing_Thread.require()
wenzelm@34784
    31
    buffer.getProperty(key) match {
wenzelm@34784
    32
      case model: Document_Model => Some(model)
wenzelm@34784
    33
      case _ => None
wenzelm@34784
    34
    }
wenzelm@34784
    35
  }
wenzelm@34784
    36
wenzelm@34784
    37
  def exit(buffer: Buffer)
wenzelm@34784
    38
  {
wenzelm@38223
    39
    Swing_Thread.require()
wenzelm@34788
    40
    apply(buffer) match {
wenzelm@39636
    41
      case None =>
wenzelm@34784
    42
      case Some(model) =>
wenzelm@34784
    43
        model.deactivate()
wenzelm@34784
    44
        buffer.unsetProperty(key)
wenzelm@47058
    45
        buffer.propertiesChanged
immler@34653
    46
    }
wenzelm@34318
    47
  }
wenzelm@43397
    48
wenzelm@44615
    49
  def init(session: Session, buffer: Buffer, name: Document.Node.Name): Document_Model =
wenzelm@43397
    50
  {
wenzelm@47058
    51
    Swing_Thread.require()
wenzelm@47058
    52
    apply(buffer).map(_.deactivate)
wenzelm@44615
    53
    val model = new Document_Model(session, buffer, name)
wenzelm@43397
    54
    buffer.setProperty(key, model)
wenzelm@43397
    55
    model.activate()
wenzelm@47058
    56
    buffer.propertiesChanged
wenzelm@43397
    57
    model
wenzelm@43397
    58
  }
wenzelm@34318
    59
}
wenzelm@34318
    60
wenzelm@38151
    61
wenzelm@44615
    62
class Document_Model(val session: Session, val buffer: Buffer, val name: Document.Node.Name)
wenzelm@34588
    63
{
wenzelm@44385
    64
  /* header */
wenzelm@38222
    65
wenzelm@48707
    66
  def node_header(): Document.Node.Header =
wenzelm@46920
    67
  {
wenzelm@46920
    68
    Swing_Thread.require()
wenzelm@49406
    69
    JEdit_Lib.buffer_lock(buffer) {
wenzelm@46748
    70
      Exn.capture {
wenzelm@50205
    71
        PIDE.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
wenzelm@48707
    72
      } match {
wenzelm@48707
    73
        case Exn.Res(header) => header
wenzelm@48707
    74
        case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
wenzelm@46748
    75
      }
wenzelm@46748
    76
    }
wenzelm@46920
    77
  }
wenzelm@44385
    78
wenzelm@44385
    79
wenzelm@52849
    80
  /* overlays */
wenzelm@52849
    81
wenzelm@52849
    82
  private var overlays = Document.Overlays.empty
wenzelm@52849
    83
wenzelm@52849
    84
  def add_overlay(command: Command, name: String, args: List[String])
wenzelm@52849
    85
  {
wenzelm@52849
    86
    Swing_Thread.required()
wenzelm@52849
    87
    overlays += ((command, name, args))
wenzelm@52849
    88
    PIDE.flush_buffers()
wenzelm@52849
    89
  }
wenzelm@52849
    90
wenzelm@52849
    91
  def remove_overlay(command: Command, name: String, args: List[String])
wenzelm@52849
    92
  {
wenzelm@52849
    93
    Swing_Thread.required()
wenzelm@52849
    94
    overlays -= ((command, name, args))
wenzelm@52849
    95
    PIDE.flush_buffers()
wenzelm@52849
    96
  }
wenzelm@52849
    97
wenzelm@52849
    98
wenzelm@44385
    99
  /* perspective */
wenzelm@44385
   100
wenzelm@52849
   101
  // owned by Swing thread
wenzelm@52816
   102
  private var _node_required = false
wenzelm@52816
   103
  def node_required: Boolean = _node_required
wenzelm@52816
   104
  def node_required_=(b: Boolean)
wenzelm@52816
   105
  {
wenzelm@52816
   106
    Swing_Thread.require()
wenzelm@52816
   107
    if (_node_required != b) {
wenzelm@52816
   108
      _node_required = b
wenzelm@52816
   109
      PIDE.options_changed()
wenzelm@52816
   110
      PIDE.flush_buffers()
wenzelm@52816
   111
    }
wenzelm@52816
   112
  }
wenzelm@52808
   113
wenzelm@52849
   114
  val empty_perspective: Document.Node.Perspective_Text =
wenzelm@52849
   115
    Document.Node.Perspective(false, Text.Perspective.empty, Document.Overlays.empty)
wenzelm@52849
   116
wenzelm@52808
   117
  def node_perspective(): Document.Node.Perspective_Text =
wenzelm@44385
   118
  {
wenzelm@44385
   119
    Swing_Thread.require()
wenzelm@52759
   120
wenzelm@52849
   121
    if (Isabelle.continuous_checking) {
wenzelm@52849
   122
      Document.Node.Perspective(node_required, Text.Perspective(
wenzelm@52849
   123
        for {
wenzelm@52849
   124
          doc_view <- PIDE.document_views(buffer)
wenzelm@52849
   125
          range <- doc_view.perspective().ranges
wenzelm@52849
   126
        } yield range), overlays)
wenzelm@52849
   127
    }
wenzelm@52849
   128
    else empty_perspective
wenzelm@44385
   129
  }
wenzelm@44385
   130
wenzelm@44385
   131
wenzelm@50363
   132
  /* edits */
wenzelm@50344
   133
wenzelm@50344
   134
  def init_edits(): List[Document.Edit_Text] =
wenzelm@50344
   135
  {
wenzelm@50344
   136
    Swing_Thread.require()
wenzelm@52815
   137
wenzelm@50344
   138
    val header = node_header()
wenzelm@50344
   139
    val text = JEdit_Lib.buffer_text(buffer)
wenzelm@50344
   140
    val perspective = node_perspective()
wenzelm@50344
   141
wenzelm@50344
   142
    List(session.header_edit(name, header),
wenzelm@50344
   143
      name -> Document.Node.Clear(),
wenzelm@50344
   144
      name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
wenzelm@52808
   145
      name -> perspective)
wenzelm@50344
   146
  }
wenzelm@50344
   147
wenzelm@52808
   148
  def node_edits(perspective: Document.Node.Perspective_Text, text_edits: List[Text.Edit])
wenzelm@50363
   149
    : List[Document.Edit_Text] =
wenzelm@50363
   150
  {
wenzelm@50363
   151
    Swing_Thread.require()
wenzelm@52815
   152
wenzelm@50363
   153
    val header = node_header()
wenzelm@50363
   154
wenzelm@50363
   155
    List(session.header_edit(name, header),
wenzelm@50363
   156
      name -> Document.Node.Edits(text_edits),
wenzelm@52808
   157
      name -> perspective)
wenzelm@50363
   158
  }
wenzelm@50363
   159
wenzelm@50344
   160
wenzelm@50344
   161
  /* pending edits */
wenzelm@43648
   162
wenzelm@43644
   163
  private object pending_edits  // owned by Swing thread
wenzelm@38224
   164
  {
wenzelm@38425
   165
    private val pending = new mutable.ListBuffer[Text.Edit]
wenzelm@52849
   166
    private var last_perspective = empty_perspective
wenzelm@44438
   167
wenzelm@38425
   168
    def snapshot(): List[Text.Edit] = pending.toList
wenzelm@38224
   169
wenzelm@52759
   170
    def flushed_edits(): List[Document.Edit_Text] =
wenzelm@38224
   171
    {
wenzelm@38224
   172
      Swing_Thread.require()
wenzelm@44438
   173
wenzelm@47393
   174
      val edits = snapshot()
wenzelm@50344
   175
      val new_perspective = node_perspective()
wenzelm@47393
   176
      if (!edits.isEmpty || last_perspective != new_perspective) {
wenzelm@47393
   177
        pending.clear
wenzelm@47393
   178
        last_perspective = new_perspective
wenzelm@52759
   179
        node_edits(new_perspective, edits)
wenzelm@43648
   180
      }
wenzelm@52759
   181
      else Nil
wenzelm@38224
   182
    }
wenzelm@38224
   183
wenzelm@52759
   184
    def flush(): Unit = session.update(flushed_edits())
wenzelm@52759
   185
wenzelm@52767
   186
    val delay_flush =
wenzelm@50207
   187
      Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() }
wenzelm@40478
   188
wenzelm@38425
   189
    def +=(edit: Text.Edit)
wenzelm@38224
   190
    {
wenzelm@38224
   191
      Swing_Thread.require()
wenzelm@38224
   192
      pending += edit
wenzelm@49195
   193
      delay_flush.invoke()
wenzelm@38222
   194
    }
wenzelm@44436
   195
wenzelm@46740
   196
    def init()
wenzelm@46740
   197
    {
wenzelm@46740
   198
      flush()
wenzelm@50363
   199
      session.update(init_edits())
wenzelm@46740
   200
    }
wenzelm@46740
   201
wenzelm@46740
   202
    def exit()
wenzelm@46740
   203
    {
wenzelm@49195
   204
      delay_flush.revoke()
wenzelm@46740
   205
      flush()
wenzelm@44436
   206
    }
wenzelm@44436
   207
  }
wenzelm@44436
   208
wenzelm@52759
   209
  def flushed_edits(): List[Document.Edit_Text] = pending_edits.flushed_edits()
wenzelm@52767
   210
wenzelm@52767
   211
  def update_perspective(): Unit = pending_edits.delay_flush.invoke()
wenzelm@44776
   212
wenzelm@38152
   213
wenzelm@38152
   214
  /* snapshot */
wenzelm@34731
   215
wenzelm@38417
   216
  def snapshot(): Document.Snapshot =
wenzelm@38417
   217
  {
wenzelm@38223
   218
    Swing_Thread.require()
wenzelm@44615
   219
    session.snapshot(name, pending_edits.snapshot())
wenzelm@38223
   220
  }
wenzelm@34828
   221
wenzelm@34828
   222
wenzelm@34828
   223
  /* buffer listener */
wenzelm@34828
   224
wenzelm@34828
   225
  private val buffer_listener: BufferListener = new BufferAdapter
wenzelm@34828
   226
  {
wenzelm@40478
   227
    override def bufferLoaded(buffer: JEditBuffer)
wenzelm@40478
   228
    {
wenzelm@40478
   229
      pending_edits.init()
wenzelm@40478
   230
    }
wenzelm@40478
   231
wenzelm@34828
   232
    override def contentInserted(buffer: JEditBuffer,
wenzelm@34828
   233
      start_line: Int, offset: Int, num_lines: Int, length: Int)
wenzelm@34828
   234
    {
wenzelm@40478
   235
      if (!buffer.isLoading)
wenzelm@40478
   236
        pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
wenzelm@34828
   237
    }
wenzelm@34828
   238
wenzelm@34828
   239
    override def preContentRemoved(buffer: JEditBuffer,
wenzelm@38426
   240
      start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
wenzelm@34828
   241
    {
wenzelm@40478
   242
      if (!buffer.isLoading)
wenzelm@40478
   243
        pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
wenzelm@34828
   244
    }
wenzelm@34828
   245
  }
wenzelm@34828
   246
wenzelm@34828
   247
wenzelm@38158
   248
  /* activation */
wenzelm@37557
   249
wenzelm@43512
   250
  private def activate()
wenzelm@34784
   251
  {
wenzelm@34784
   252
    buffer.addBufferListener(buffer_listener)
wenzelm@50344
   253
    pending_edits.flush()
wenzelm@44358
   254
    Token_Markup.refresh_buffer(buffer)
immler@34680
   255
  }
immler@34680
   256
wenzelm@43512
   257
  private def deactivate()
immler@34680
   258
  {
wenzelm@46740
   259
    pending_edits.exit()
wenzelm@34784
   260
    buffer.removeBufferListener(buffer_listener)
wenzelm@44358
   261
    Token_Markup.refresh_buffer(buffer)
immler@34680
   262
  }
wenzelm@34447
   263
}