src/Tools/jEdit/src/document_model.scala
author wenzelm
Mon Nov 18 19:56:34 2013 +0100 (2013-11-18)
changeset 54511 1fd24c96ce9b
parent 54509 1f77110c94ef
child 54513 5545aff878b1
permissions -rw-r--r--
caching of blob;
precise file content according to jEdit IO;
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@54509
    63
  def is_theory: Boolean = node_name.is_theory
wenzelm@54509
    64
wenzelm@48707
    65
  def node_header(): Document.Node.Header =
wenzelm@46920
    66
  {
wenzelm@46920
    67
    Swing_Thread.require()
wenzelm@54509
    68
wenzelm@54509
    69
    if (is_theory) {
wenzelm@54509
    70
      JEdit_Lib.buffer_lock(buffer) {
wenzelm@54509
    71
        Exn.capture {
wenzelm@54509
    72
          PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
wenzelm@54509
    73
        } match {
wenzelm@54509
    74
          case Exn.Res(header) => header
wenzelm@54509
    75
          case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
wenzelm@54509
    76
        }
wenzelm@46748
    77
      }
wenzelm@46748
    78
    }
wenzelm@54509
    79
    else Document.Node.no_header
wenzelm@46920
    80
  }
wenzelm@44385
    81
wenzelm@44385
    82
wenzelm@44385
    83
  /* perspective */
wenzelm@44385
    84
wenzelm@52849
    85
  // owned by Swing thread
wenzelm@52816
    86
  private var _node_required = false
wenzelm@52816
    87
  def node_required: Boolean = _node_required
wenzelm@52816
    88
  def node_required_=(b: Boolean)
wenzelm@52816
    89
  {
wenzelm@52816
    90
    Swing_Thread.require()
wenzelm@52816
    91
    if (_node_required != b) {
wenzelm@52816
    92
      _node_required = b
wenzelm@52816
    93
      PIDE.options_changed()
wenzelm@52974
    94
      PIDE.editor.flush()
wenzelm@52816
    95
    }
wenzelm@52816
    96
  }
wenzelm@52808
    97
wenzelm@52849
    98
  val empty_perspective: Document.Node.Perspective_Text =
wenzelm@52887
    99
    Document.Node.Perspective(false, Text.Perspective.empty, Document.Node.Overlays.empty)
wenzelm@52849
   100
wenzelm@52808
   101
  def node_perspective(): Document.Node.Perspective_Text =
wenzelm@44385
   102
  {
wenzelm@44385
   103
    Swing_Thread.require()
wenzelm@52759
   104
wenzelm@54509
   105
    if (Isabelle.continuous_checking && is_theory) {
wenzelm@54325
   106
      val snapshot = this.snapshot()
wenzelm@52849
   107
      Document.Node.Perspective(node_required, Text.Perspective(
wenzelm@52849
   108
        for {
wenzelm@52849
   109
          doc_view <- PIDE.document_views(buffer)
wenzelm@54325
   110
          range <- doc_view.perspective(snapshot).ranges
wenzelm@52977
   111
        } yield range), PIDE.editor.node_overlays(node_name))
wenzelm@52849
   112
    }
wenzelm@52849
   113
    else empty_perspective
wenzelm@44385
   114
  }
wenzelm@44385
   115
wenzelm@44385
   116
wenzelm@54509
   117
  /* blob */
wenzelm@54509
   118
wenzelm@54511
   119
  private var _blob: Option[Bytes] = None  // owned by Swing thread
wenzelm@54511
   120
wenzelm@54511
   121
  private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
wenzelm@54511
   122
wenzelm@54509
   123
  def blob(): Bytes =
wenzelm@54511
   124
    Swing_Thread.require {
wenzelm@54511
   125
      _blob match {
wenzelm@54511
   126
        case Some(b) => b
wenzelm@54511
   127
        case None =>
wenzelm@54511
   128
          val b = PIDE.thy_load.file_content(buffer)
wenzelm@54511
   129
          _blob = Some(b)
wenzelm@54511
   130
          b
wenzelm@54511
   131
      }
wenzelm@54511
   132
    }
wenzelm@54509
   133
wenzelm@54509
   134
wenzelm@50363
   135
  /* edits */
wenzelm@50344
   136
wenzelm@50344
   137
  def init_edits(): List[Document.Edit_Text] =
wenzelm@50344
   138
  {
wenzelm@50344
   139
    Swing_Thread.require()
wenzelm@52815
   140
wenzelm@50344
   141
    val header = node_header()
wenzelm@50344
   142
    val text = JEdit_Lib.buffer_text(buffer)
wenzelm@50344
   143
    val perspective = node_perspective()
wenzelm@50344
   144
wenzelm@54509
   145
    if (is_theory)
wenzelm@54509
   146
      List(session.header_edit(node_name, header),
wenzelm@54509
   147
        node_name -> Document.Node.Clear(),
wenzelm@54509
   148
        node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
wenzelm@54509
   149
        node_name -> perspective)
wenzelm@54509
   150
    else
wenzelm@54509
   151
      List(node_name -> Document.Node.Blob(blob()))
wenzelm@50344
   152
  }
wenzelm@50344
   153
wenzelm@54461
   154
  def node_edits(
wenzelm@54461
   155
    clear: Boolean,
wenzelm@54461
   156
    text_edits: List[Text.Edit],
wenzelm@54461
   157
    perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
wenzelm@50363
   158
  {
wenzelm@50363
   159
    Swing_Thread.require()
wenzelm@52815
   160
wenzelm@54509
   161
    if (is_theory) {
wenzelm@54509
   162
      val header_edit = session.header_edit(node_name, node_header())
wenzelm@54509
   163
      if (clear)
wenzelm@54509
   164
        List(header_edit,
wenzelm@54509
   165
          node_name -> Document.Node.Clear(),
wenzelm@54509
   166
          node_name -> Document.Node.Edits(text_edits),
wenzelm@54509
   167
          node_name -> perspective)
wenzelm@54509
   168
      else
wenzelm@54509
   169
        List(header_edit,
wenzelm@54509
   170
          node_name -> Document.Node.Edits(text_edits),
wenzelm@54509
   171
          node_name -> perspective)
wenzelm@54509
   172
    }
wenzelm@54461
   173
    else
wenzelm@54509
   174
      List(node_name -> Document.Node.Blob(blob()))
wenzelm@50363
   175
  }
wenzelm@50363
   176
wenzelm@50344
   177
wenzelm@50344
   178
  /* pending edits */
wenzelm@43648
   179
wenzelm@43644
   180
  private object pending_edits  // owned by Swing thread
wenzelm@38224
   181
  {
wenzelm@54461
   182
    private var pending_clear = false
wenzelm@38425
   183
    private val pending = new mutable.ListBuffer[Text.Edit]
wenzelm@52849
   184
    private var last_perspective = empty_perspective
wenzelm@44438
   185
wenzelm@38425
   186
    def snapshot(): List[Text.Edit] = pending.toList
wenzelm@38224
   187
wenzelm@52759
   188
    def flushed_edits(): List[Document.Edit_Text] =
wenzelm@38224
   189
    {
wenzelm@54461
   190
      val clear = pending_clear
wenzelm@47393
   191
      val edits = snapshot()
wenzelm@54461
   192
      val perspective = node_perspective()
wenzelm@54461
   193
      if (clear || !edits.isEmpty || last_perspective != perspective) {
wenzelm@54461
   194
        pending_clear = false
wenzelm@47393
   195
        pending.clear
wenzelm@54461
   196
        last_perspective = perspective
wenzelm@54461
   197
        node_edits(clear, edits, perspective)
wenzelm@43648
   198
      }
wenzelm@52759
   199
      else Nil
wenzelm@38224
   200
    }
wenzelm@38224
   201
wenzelm@54461
   202
    def edit(clear: Boolean, e: Text.Edit)
wenzelm@38224
   203
    {
wenzelm@54511
   204
      reset_blob()
wenzelm@54511
   205
wenzelm@54461
   206
      if (clear) {
wenzelm@54461
   207
        pending_clear = true
wenzelm@54461
   208
        pending.clear
wenzelm@54461
   209
      }
wenzelm@54461
   210
      pending += e
wenzelm@54461
   211
      PIDE.editor.invoke()
wenzelm@44436
   212
    }
wenzelm@44436
   213
  }
wenzelm@44436
   214
wenzelm@54464
   215
  def snapshot(): Document.Snapshot =
wenzelm@54464
   216
    Swing_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) }
wenzelm@34731
   217
wenzelm@54464
   218
  def flushed_edits(): List[Document.Edit_Text] =
wenzelm@54464
   219
    Swing_Thread.require { pending_edits.flushed_edits() }
wenzelm@34828
   220
wenzelm@34828
   221
wenzelm@34828
   222
  /* buffer listener */
wenzelm@34828
   223
wenzelm@34828
   224
  private val buffer_listener: BufferListener = new BufferAdapter
wenzelm@34828
   225
  {
wenzelm@40478
   226
    override def bufferLoaded(buffer: JEditBuffer)
wenzelm@40478
   227
    {
wenzelm@54461
   228
      pending_edits.edit(true, Text.Edit.insert(0, buffer.getText(0, buffer.getLength)))
wenzelm@40478
   229
    }
wenzelm@40478
   230
wenzelm@34828
   231
    override def contentInserted(buffer: JEditBuffer,
wenzelm@34828
   232
      start_line: Int, offset: Int, num_lines: Int, length: Int)
wenzelm@34828
   233
    {
wenzelm@40478
   234
      if (!buffer.isLoading)
wenzelm@54461
   235
        pending_edits.edit(false, Text.Edit.insert(offset, buffer.getText(offset, length)))
wenzelm@34828
   236
    }
wenzelm@34828
   237
wenzelm@34828
   238
    override def preContentRemoved(buffer: JEditBuffer,
wenzelm@38426
   239
      start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
wenzelm@34828
   240
    {
wenzelm@40478
   241
      if (!buffer.isLoading)
wenzelm@54461
   242
        pending_edits.edit(false, Text.Edit.remove(offset, buffer.getText(offset, removed_length)))
wenzelm@34828
   243
    }
wenzelm@34828
   244
  }
wenzelm@34828
   245
wenzelm@34828
   246
wenzelm@38158
   247
  /* activation */
wenzelm@37557
   248
wenzelm@43512
   249
  private def activate()
wenzelm@34784
   250
  {
wenzelm@34784
   251
    buffer.addBufferListener(buffer_listener)
wenzelm@44358
   252
    Token_Markup.refresh_buffer(buffer)
immler@34680
   253
  }
immler@34680
   254
wenzelm@43512
   255
  private def deactivate()
immler@34680
   256
  {
wenzelm@34784
   257
    buffer.removeBufferListener(buffer_listener)
wenzelm@44358
   258
    Token_Markup.refresh_buffer(buffer)
immler@34680
   259
  }
wenzelm@34447
   260
}