src/Tools/jEdit/src/document_model.scala
author wenzelm
Thu Feb 27 14:07:04 2014 +0100 (2014-02-27)
changeset 55783 da0513d95155
parent 55781 b3a4207fb9a6
child 55784 9b243afbbe83
permissions -rw-r--r--
more formal Document.Blobs;
removed junk;
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@55778
     5
Document model connected to jEdit buffer (node in theory graph or
wenzelm@55778
     6
auxiliary file).
wenzelm@36760
     7
*/
wenzelm@34407
     8
wenzelm@34784
     9
package isabelle.jedit
wenzelm@34760
    10
wenzelm@34318
    11
wenzelm@36015
    12
import isabelle._
wenzelm@36015
    13
wenzelm@34693
    14
import scala.collection.mutable
wenzelm@34446
    15
wenzelm@34784
    16
import org.gjt.sp.jedit.Buffer
wenzelm@34783
    17
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
wenzelm@34318
    18
wenzelm@34760
    19
wenzelm@34784
    20
object Document_Model
wenzelm@34588
    21
{
wenzelm@34784
    22
  /* document model of buffer */
wenzelm@34784
    23
wenzelm@50565
    24
  private val key = "PIDE.document_model"
wenzelm@34784
    25
wenzelm@34788
    26
  def apply(buffer: Buffer): Option[Document_Model] =
wenzelm@34784
    27
  {
wenzelm@38223
    28
    Swing_Thread.require()
wenzelm@34784
    29
    buffer.getProperty(key) match {
wenzelm@34784
    30
      case model: Document_Model => Some(model)
wenzelm@34784
    31
      case _ => None
wenzelm@34784
    32
    }
wenzelm@34784
    33
  }
wenzelm@34784
    34
wenzelm@34784
    35
  def exit(buffer: Buffer)
wenzelm@34784
    36
  {
wenzelm@38223
    37
    Swing_Thread.require()
wenzelm@34788
    38
    apply(buffer) match {
wenzelm@39636
    39
      case None =>
wenzelm@34784
    40
      case Some(model) =>
wenzelm@34784
    41
        model.deactivate()
wenzelm@34784
    42
        buffer.unsetProperty(key)
wenzelm@47058
    43
        buffer.propertiesChanged
immler@34653
    44
    }
wenzelm@34318
    45
  }
wenzelm@43397
    46
wenzelm@52973
    47
  def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
wenzelm@43397
    48
  {
wenzelm@47058
    49
    Swing_Thread.require()
wenzelm@47058
    50
    apply(buffer).map(_.deactivate)
wenzelm@52973
    51
    val model = new Document_Model(session, buffer, node_name)
wenzelm@43397
    52
    buffer.setProperty(key, model)
wenzelm@43397
    53
    model.activate()
wenzelm@47058
    54
    buffer.propertiesChanged
wenzelm@43397
    55
    model
wenzelm@43397
    56
  }
wenzelm@34318
    57
}
wenzelm@34318
    58
wenzelm@38151
    59
wenzelm@52973
    60
class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name)
wenzelm@34588
    61
{
wenzelm@44385
    62
  /* header */
wenzelm@38222
    63
wenzelm@54509
    64
  def is_theory: Boolean = node_name.is_theory
wenzelm@54509
    65
wenzelm@48707
    66
  def node_header(): Document.Node.Header =
wenzelm@46920
    67
  {
wenzelm@46920
    68
    Swing_Thread.require()
wenzelm@54509
    69
wenzelm@54509
    70
    if (is_theory) {
wenzelm@54509
    71
      JEdit_Lib.buffer_lock(buffer) {
wenzelm@54509
    72
        Exn.capture {
wenzelm@54509
    73
          PIDE.thy_load.check_thy_text(node_name, buffer.getSegment(0, buffer.getLength))
wenzelm@54509
    74
        } match {
wenzelm@54509
    75
          case Exn.Res(header) => header
wenzelm@54509
    76
          case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
wenzelm@54509
    77
        }
wenzelm@46748
    78
      }
wenzelm@46748
    79
    }
wenzelm@54509
    80
    else Document.Node.no_header
wenzelm@46920
    81
  }
wenzelm@44385
    82
wenzelm@44385
    83
wenzelm@44385
    84
  /* perspective */
wenzelm@44385
    85
wenzelm@52849
    86
  // owned by Swing thread
wenzelm@52816
    87
  private var _node_required = false
wenzelm@52816
    88
  def node_required: Boolean = _node_required
wenzelm@52816
    89
  def node_required_=(b: Boolean)
wenzelm@52816
    90
  {
wenzelm@52816
    91
    Swing_Thread.require()
wenzelm@54531
    92
    if (_node_required != b && is_theory) {
wenzelm@52816
    93
      _node_required = b
wenzelm@52816
    94
      PIDE.options_changed()
wenzelm@52974
    95
      PIDE.editor.flush()
wenzelm@52816
    96
    }
wenzelm@52816
    97
  }
wenzelm@52808
    98
wenzelm@52849
    99
  val empty_perspective: Document.Node.Perspective_Text =
wenzelm@52887
   100
    Document.Node.Perspective(false, Text.Perspective.empty, Document.Node.Overlays.empty)
wenzelm@52849
   101
wenzelm@55783
   102
  def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
wenzelm@44385
   103
  {
wenzelm@44385
   104
    Swing_Thread.require()
wenzelm@52759
   105
wenzelm@54509
   106
    if (Isabelle.continuous_checking && is_theory) {
wenzelm@54325
   107
      val snapshot = this.snapshot()
wenzelm@54530
   108
wenzelm@54530
   109
      val document_view_ranges =
wenzelm@55432
   110
        if (is_theory) {
wenzelm@55432
   111
          for {
wenzelm@55432
   112
            doc_view <- PIDE.document_views(buffer)
wenzelm@55432
   113
            range <- doc_view.perspective(snapshot).ranges
wenzelm@55432
   114
          } yield range
wenzelm@55432
   115
        }
wenzelm@55432
   116
        else Nil
wenzelm@54530
   117
wenzelm@54530
   118
      val thy_load_ranges =
wenzelm@54530
   119
        for {
wenzelm@54530
   120
          cmd <- snapshot.node.thy_load_commands
wenzelm@54530
   121
          blob_name <- cmd.blobs_names
wenzelm@54530
   122
          blob_buffer <- JEdit_Lib.jedit_buffer(blob_name.node)
wenzelm@54530
   123
          if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
wenzelm@54530
   124
          start <- snapshot.node.command_start(cmd)
wenzelm@54530
   125
          range = snapshot.convert(cmd.proper_range + start)
wenzelm@54530
   126
        } yield range
wenzelm@54530
   127
wenzelm@55781
   128
      val reparse =
wenzelm@55783
   129
        snapshot.node.thy_load_commands.exists(cmd => cmd.blobs_names.exists(doc_blobs.changed))
wenzelm@55781
   130
wenzelm@55781
   131
      (reparse,
wenzelm@55781
   132
        Document.Node.Perspective(node_required,
wenzelm@55781
   133
          Text.Perspective(document_view_ranges ::: thy_load_ranges),
wenzelm@55781
   134
          PIDE.editor.node_overlays(node_name)))
wenzelm@52849
   135
    }
wenzelm@55781
   136
    else (false, empty_perspective)
wenzelm@44385
   137
  }
wenzelm@44385
   138
wenzelm@44385
   139
wenzelm@54509
   140
  /* blob */
wenzelm@54509
   141
wenzelm@55431
   142
  private var _blob: Option[(Bytes, Command.File)] = None  // owned by Swing thread
wenzelm@54511
   143
wenzelm@54511
   144
  private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
wenzelm@54511
   145
wenzelm@55783
   146
  def get_blob(): Option[Document.Blob] =
wenzelm@54511
   147
    Swing_Thread.require {
wenzelm@55783
   148
      if (is_theory) None
wenzelm@55783
   149
      else {
wenzelm@55783
   150
        val (bytes, file) =
wenzelm@55783
   151
          _blob match {
wenzelm@55783
   152
            case Some(x) => x
wenzelm@55783
   153
            case None =>
wenzelm@55783
   154
              val bytes = PIDE.thy_load.file_content(buffer)
wenzelm@55783
   155
              val file = new Command.File(node_name.node, buffer.getSegment(0, buffer.getLength))
wenzelm@55783
   156
              _blob = Some((bytes, file))
wenzelm@55783
   157
              (bytes, file)
wenzelm@55783
   158
          }
wenzelm@55783
   159
        val changed = pending_edits.is_pending()
wenzelm@55783
   160
        Some(Document.Blob(bytes, file, changed))
wenzelm@54511
   161
      }
wenzelm@54511
   162
    }
wenzelm@54509
   163
wenzelm@54509
   164
wenzelm@50363
   165
  /* edits */
wenzelm@50344
   166
wenzelm@50344
   167
  def init_edits(): List[Document.Edit_Text] =
wenzelm@50344
   168
  {
wenzelm@50344
   169
    Swing_Thread.require()
wenzelm@52815
   170
wenzelm@50344
   171
    val header = node_header()
wenzelm@50344
   172
    val text = JEdit_Lib.buffer_text(buffer)
wenzelm@55783
   173
    val (_, perspective) = node_perspective(Document.Blobs.empty)
wenzelm@50344
   174
wenzelm@54509
   175
    if (is_theory)
wenzelm@54509
   176
      List(session.header_edit(node_name, header),
wenzelm@54509
   177
        node_name -> Document.Node.Clear(),
wenzelm@54509
   178
        node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
wenzelm@54509
   179
        node_name -> perspective)
wenzelm@54509
   180
    else
wenzelm@55435
   181
      List(node_name -> Document.Node.Blob(),
wenzelm@55435
   182
        node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))))
wenzelm@50344
   183
  }
wenzelm@50344
   184
wenzelm@54461
   185
  def node_edits(
wenzelm@54461
   186
    clear: Boolean,
wenzelm@54461
   187
    text_edits: List[Text.Edit],
wenzelm@54461
   188
    perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
wenzelm@50363
   189
  {
wenzelm@50363
   190
    Swing_Thread.require()
wenzelm@52815
   191
wenzelm@54509
   192
    if (is_theory) {
wenzelm@54509
   193
      val header_edit = session.header_edit(node_name, node_header())
wenzelm@54509
   194
      if (clear)
wenzelm@54509
   195
        List(header_edit,
wenzelm@54509
   196
          node_name -> Document.Node.Clear(),
wenzelm@54509
   197
          node_name -> Document.Node.Edits(text_edits),
wenzelm@54509
   198
          node_name -> perspective)
wenzelm@54509
   199
      else
wenzelm@54509
   200
        List(header_edit,
wenzelm@54509
   201
          node_name -> Document.Node.Edits(text_edits),
wenzelm@54509
   202
          node_name -> perspective)
wenzelm@54509
   203
    }
wenzelm@54461
   204
    else
wenzelm@55435
   205
      List(node_name -> Document.Node.Blob(),
wenzelm@55435
   206
        node_name -> Document.Node.Edits(text_edits))
wenzelm@50363
   207
  }
wenzelm@50363
   208
wenzelm@50344
   209
wenzelm@50344
   210
  /* pending edits */
wenzelm@43648
   211
wenzelm@43644
   212
  private object pending_edits  // owned by Swing thread
wenzelm@38224
   213
  {
wenzelm@54461
   214
    private var pending_clear = false
wenzelm@38425
   215
    private val pending = new mutable.ListBuffer[Text.Edit]
wenzelm@52849
   216
    private var last_perspective = empty_perspective
wenzelm@44438
   217
wenzelm@55781
   218
    def is_pending(): Boolean = pending_clear || !pending.isEmpty
wenzelm@38425
   219
    def snapshot(): List[Text.Edit] = pending.toList
wenzelm@38224
   220
wenzelm@55783
   221
    def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
wenzelm@38224
   222
    {
wenzelm@54461
   223
      val clear = pending_clear
wenzelm@47393
   224
      val edits = snapshot()
wenzelm@55783
   225
      val (reparse, perspective) = node_perspective(doc_blobs)
wenzelm@55781
   226
      if (clear || reparse || !edits.isEmpty || last_perspective != perspective) {
wenzelm@54461
   227
        pending_clear = false
wenzelm@47393
   228
        pending.clear
wenzelm@54461
   229
        last_perspective = perspective
wenzelm@54461
   230
        node_edits(clear, edits, perspective)
wenzelm@43648
   231
      }
wenzelm@52759
   232
      else Nil
wenzelm@38224
   233
    }
wenzelm@38224
   234
wenzelm@54461
   235
    def edit(clear: Boolean, e: Text.Edit)
wenzelm@38224
   236
    {
wenzelm@54511
   237
      reset_blob()
wenzelm@54511
   238
wenzelm@54461
   239
      if (clear) {
wenzelm@54461
   240
        pending_clear = true
wenzelm@54461
   241
        pending.clear
wenzelm@54461
   242
      }
wenzelm@54461
   243
      pending += e
wenzelm@54461
   244
      PIDE.editor.invoke()
wenzelm@44436
   245
    }
wenzelm@44436
   246
  }
wenzelm@44436
   247
wenzelm@54464
   248
  def snapshot(): Document.Snapshot =
wenzelm@54464
   249
    Swing_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) }
wenzelm@34731
   250
wenzelm@55783
   251
  def flushed_edits(doc_blobs: Document.Blobs): List[Document.Edit_Text] =
wenzelm@55783
   252
    Swing_Thread.require { pending_edits.flushed_edits(doc_blobs) }
wenzelm@34828
   253
wenzelm@34828
   254
wenzelm@34828
   255
  /* buffer listener */
wenzelm@34828
   256
wenzelm@34828
   257
  private val buffer_listener: BufferListener = new BufferAdapter
wenzelm@34828
   258
  {
wenzelm@40478
   259
    override def bufferLoaded(buffer: JEditBuffer)
wenzelm@40478
   260
    {
wenzelm@54461
   261
      pending_edits.edit(true, Text.Edit.insert(0, buffer.getText(0, buffer.getLength)))
wenzelm@40478
   262
    }
wenzelm@40478
   263
wenzelm@34828
   264
    override def contentInserted(buffer: JEditBuffer,
wenzelm@34828
   265
      start_line: Int, offset: Int, num_lines: Int, length: Int)
wenzelm@34828
   266
    {
wenzelm@40478
   267
      if (!buffer.isLoading)
wenzelm@54461
   268
        pending_edits.edit(false, Text.Edit.insert(offset, buffer.getText(offset, length)))
wenzelm@34828
   269
    }
wenzelm@34828
   270
wenzelm@34828
   271
    override def preContentRemoved(buffer: JEditBuffer,
wenzelm@38426
   272
      start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
wenzelm@34828
   273
    {
wenzelm@40478
   274
      if (!buffer.isLoading)
wenzelm@54461
   275
        pending_edits.edit(false, Text.Edit.remove(offset, buffer.getText(offset, removed_length)))
wenzelm@34828
   276
    }
wenzelm@34828
   277
  }
wenzelm@34828
   278
wenzelm@34828
   279
wenzelm@38158
   280
  /* activation */
wenzelm@37557
   281
wenzelm@43512
   282
  private def activate()
wenzelm@34784
   283
  {
wenzelm@34784
   284
    buffer.addBufferListener(buffer_listener)
wenzelm@44358
   285
    Token_Markup.refresh_buffer(buffer)
immler@34680
   286
  }
immler@34680
   287
wenzelm@43512
   288
  private def deactivate()
immler@34680
   289
  {
wenzelm@34784
   290
    buffer.removeBufferListener(buffer_listener)
wenzelm@44358
   291
    Token_Markup.refresh_buffer(buffer)
immler@34680
   292
  }
wenzelm@34447
   293
}