src/Tools/jEdit/src/document_model.scala
author wenzelm
Wed Nov 20 15:53:59 2013 +0100 (2013-11-20)
changeset 54530 2c1440f70028
parent 54521 744ea0025e11
child 54531 8330faaeebd5
permissions -rw-r--r--
ranges of thy_load commands count as visible within perspective;
convert ranges wrt. snapshot -- relevant for outdated situation;
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@54530
   107
wenzelm@54530
   108
      val document_view_ranges =
wenzelm@52849
   109
        for {
wenzelm@52849
   110
          doc_view <- PIDE.document_views(buffer)
wenzelm@54325
   111
          range <- doc_view.perspective(snapshot).ranges
wenzelm@54530
   112
        } yield range
wenzelm@54530
   113
wenzelm@54530
   114
      val thy_load_ranges =
wenzelm@54530
   115
        for {
wenzelm@54530
   116
          cmd <- snapshot.node.thy_load_commands
wenzelm@54530
   117
          blob_name <- cmd.blobs_names
wenzelm@54530
   118
          blob_buffer <- JEdit_Lib.jedit_buffer(blob_name.node)
wenzelm@54530
   119
          if !JEdit_Lib.jedit_text_areas(blob_buffer).isEmpty
wenzelm@54530
   120
          start <- snapshot.node.command_start(cmd)
wenzelm@54530
   121
          range = snapshot.convert(cmd.proper_range + start)
wenzelm@54530
   122
        } yield range
wenzelm@54530
   123
wenzelm@54530
   124
      Document.Node.Perspective(node_required,
wenzelm@54530
   125
        Text.Perspective(document_view_ranges ::: thy_load_ranges),
wenzelm@54530
   126
        PIDE.editor.node_overlays(node_name))
wenzelm@52849
   127
    }
wenzelm@52849
   128
    else empty_perspective
wenzelm@44385
   129
  }
wenzelm@44385
   130
wenzelm@44385
   131
wenzelm@54509
   132
  /* blob */
wenzelm@54509
   133
wenzelm@54511
   134
  private var _blob: Option[Bytes] = None  // owned by Swing thread
wenzelm@54511
   135
wenzelm@54511
   136
  private def reset_blob(): Unit = Swing_Thread.require { _blob = None }
wenzelm@54511
   137
wenzelm@54509
   138
  def blob(): Bytes =
wenzelm@54511
   139
    Swing_Thread.require {
wenzelm@54511
   140
      _blob match {
wenzelm@54511
   141
        case Some(b) => b
wenzelm@54511
   142
        case None =>
wenzelm@54511
   143
          val b = PIDE.thy_load.file_content(buffer)
wenzelm@54511
   144
          _blob = Some(b)
wenzelm@54511
   145
          b
wenzelm@54511
   146
      }
wenzelm@54511
   147
    }
wenzelm@54509
   148
wenzelm@54509
   149
wenzelm@50363
   150
  /* edits */
wenzelm@50344
   151
wenzelm@50344
   152
  def init_edits(): List[Document.Edit_Text] =
wenzelm@50344
   153
  {
wenzelm@50344
   154
    Swing_Thread.require()
wenzelm@52815
   155
wenzelm@50344
   156
    val header = node_header()
wenzelm@50344
   157
    val text = JEdit_Lib.buffer_text(buffer)
wenzelm@50344
   158
    val perspective = node_perspective()
wenzelm@50344
   159
wenzelm@54509
   160
    if (is_theory)
wenzelm@54509
   161
      List(session.header_edit(node_name, header),
wenzelm@54509
   162
        node_name -> Document.Node.Clear(),
wenzelm@54509
   163
        node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text))),
wenzelm@54509
   164
        node_name -> perspective)
wenzelm@54509
   165
    else
wenzelm@54521
   166
      List(node_name -> Document.Node.Blob())
wenzelm@50344
   167
  }
wenzelm@50344
   168
wenzelm@54461
   169
  def node_edits(
wenzelm@54461
   170
    clear: Boolean,
wenzelm@54461
   171
    text_edits: List[Text.Edit],
wenzelm@54461
   172
    perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] =
wenzelm@50363
   173
  {
wenzelm@50363
   174
    Swing_Thread.require()
wenzelm@52815
   175
wenzelm@54509
   176
    if (is_theory) {
wenzelm@54509
   177
      val header_edit = session.header_edit(node_name, node_header())
wenzelm@54509
   178
      if (clear)
wenzelm@54509
   179
        List(header_edit,
wenzelm@54509
   180
          node_name -> Document.Node.Clear(),
wenzelm@54509
   181
          node_name -> Document.Node.Edits(text_edits),
wenzelm@54509
   182
          node_name -> perspective)
wenzelm@54509
   183
      else
wenzelm@54509
   184
        List(header_edit,
wenzelm@54509
   185
          node_name -> Document.Node.Edits(text_edits),
wenzelm@54509
   186
          node_name -> perspective)
wenzelm@54509
   187
    }
wenzelm@54461
   188
    else
wenzelm@54521
   189
      List(node_name -> Document.Node.Blob())
wenzelm@50363
   190
  }
wenzelm@50363
   191
wenzelm@50344
   192
wenzelm@50344
   193
  /* pending edits */
wenzelm@43648
   194
wenzelm@43644
   195
  private object pending_edits  // owned by Swing thread
wenzelm@38224
   196
  {
wenzelm@54461
   197
    private var pending_clear = false
wenzelm@38425
   198
    private val pending = new mutable.ListBuffer[Text.Edit]
wenzelm@52849
   199
    private var last_perspective = empty_perspective
wenzelm@44438
   200
wenzelm@38425
   201
    def snapshot(): List[Text.Edit] = pending.toList
wenzelm@38224
   202
wenzelm@52759
   203
    def flushed_edits(): List[Document.Edit_Text] =
wenzelm@38224
   204
    {
wenzelm@54461
   205
      val clear = pending_clear
wenzelm@47393
   206
      val edits = snapshot()
wenzelm@54461
   207
      val perspective = node_perspective()
wenzelm@54521
   208
      if (clear || !edits.isEmpty || last_perspective != perspective) {
wenzelm@54461
   209
        pending_clear = false
wenzelm@47393
   210
        pending.clear
wenzelm@54461
   211
        last_perspective = perspective
wenzelm@54461
   212
        node_edits(clear, edits, perspective)
wenzelm@43648
   213
      }
wenzelm@52759
   214
      else Nil
wenzelm@38224
   215
    }
wenzelm@38224
   216
wenzelm@54461
   217
    def edit(clear: Boolean, e: Text.Edit)
wenzelm@38224
   218
    {
wenzelm@54511
   219
      reset_blob()
wenzelm@54511
   220
wenzelm@54461
   221
      if (clear) {
wenzelm@54461
   222
        pending_clear = true
wenzelm@54461
   223
        pending.clear
wenzelm@54461
   224
      }
wenzelm@54461
   225
      pending += e
wenzelm@54461
   226
      PIDE.editor.invoke()
wenzelm@44436
   227
    }
wenzelm@44436
   228
  }
wenzelm@44436
   229
wenzelm@54464
   230
  def snapshot(): Document.Snapshot =
wenzelm@54464
   231
    Swing_Thread.require { session.snapshot(node_name, pending_edits.snapshot()) }
wenzelm@34731
   232
wenzelm@54464
   233
  def flushed_edits(): List[Document.Edit_Text] =
wenzelm@54464
   234
    Swing_Thread.require { pending_edits.flushed_edits() }
wenzelm@34828
   235
wenzelm@34828
   236
wenzelm@34828
   237
  /* buffer listener */
wenzelm@34828
   238
wenzelm@34828
   239
  private val buffer_listener: BufferListener = new BufferAdapter
wenzelm@34828
   240
  {
wenzelm@40478
   241
    override def bufferLoaded(buffer: JEditBuffer)
wenzelm@40478
   242
    {
wenzelm@54461
   243
      pending_edits.edit(true, Text.Edit.insert(0, buffer.getText(0, buffer.getLength)))
wenzelm@40478
   244
    }
wenzelm@40478
   245
wenzelm@34828
   246
    override def contentInserted(buffer: JEditBuffer,
wenzelm@34828
   247
      start_line: Int, offset: Int, num_lines: Int, length: Int)
wenzelm@34828
   248
    {
wenzelm@40478
   249
      if (!buffer.isLoading)
wenzelm@54461
   250
        pending_edits.edit(false, Text.Edit.insert(offset, buffer.getText(offset, length)))
wenzelm@34828
   251
    }
wenzelm@34828
   252
wenzelm@34828
   253
    override def preContentRemoved(buffer: JEditBuffer,
wenzelm@38426
   254
      start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
wenzelm@34828
   255
    {
wenzelm@40478
   256
      if (!buffer.isLoading)
wenzelm@54461
   257
        pending_edits.edit(false, Text.Edit.remove(offset, buffer.getText(offset, removed_length)))
wenzelm@34828
   258
    }
wenzelm@34828
   259
  }
wenzelm@34828
   260
wenzelm@34828
   261
wenzelm@38158
   262
  /* activation */
wenzelm@37557
   263
wenzelm@43512
   264
  private def activate()
wenzelm@34784
   265
  {
wenzelm@34784
   266
    buffer.addBufferListener(buffer_listener)
wenzelm@44358
   267
    Token_Markup.refresh_buffer(buffer)
immler@34680
   268
  }
immler@34680
   269
wenzelm@43512
   270
  private def deactivate()
immler@34680
   271
  {
wenzelm@34784
   272
    buffer.removeBufferListener(buffer_listener)
wenzelm@44358
   273
    Token_Markup.refresh_buffer(buffer)
immler@34680
   274
  }
wenzelm@34447
   275
}