src/Tools/jEdit/src/document_model.scala
author wenzelm
Wed Mar 14 15:37:51 2012 +0100 (2012-03-14)
changeset 46920 5f44c8bea84e
parent 46750 69efe9b2994c
child 47058 34761733526c
permissions -rw-r--r--
more explicit indication of swing thread context;
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@34784
    26
  private val key = "isabelle.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)
immler@34653
    45
    }
wenzelm@34318
    46
  }
wenzelm@43397
    47
wenzelm@44615
    48
  def init(session: Session, buffer: Buffer, name: Document.Node.Name): Document_Model =
wenzelm@43397
    49
  {
wenzelm@43397
    50
    exit(buffer)
wenzelm@44615
    51
    val model = new Document_Model(session, buffer, name)
wenzelm@43397
    52
    buffer.setProperty(key, model)
wenzelm@43397
    53
    model.activate()
wenzelm@43397
    54
    model
wenzelm@43397
    55
  }
wenzelm@34318
    56
}
wenzelm@34318
    57
wenzelm@38151
    58
wenzelm@44615
    59
class Document_Model(val session: Session, val buffer: Buffer, val name: Document.Node.Name)
wenzelm@34588
    60
{
wenzelm@44385
    61
  /* header */
wenzelm@38222
    62
wenzelm@46737
    63
  def node_header(): Document.Node_Header =
wenzelm@46920
    64
  {
wenzelm@46920
    65
    Swing_Thread.require()
wenzelm@46920
    66
    Isabelle.buffer_lock(buffer) {
wenzelm@46748
    67
      Exn.capture {
wenzelm@46748
    68
        Isabelle.thy_load.check_header(name,
wenzelm@46748
    69
          Thy_Header.read(buffer.getSegment(0, buffer.getLength)))
wenzelm@46748
    70
      }
wenzelm@46748
    71
    }
wenzelm@46920
    72
  }
wenzelm@44385
    73
wenzelm@44385
    74
wenzelm@44385
    75
  /* perspective */
wenzelm@44385
    76
wenzelm@44776
    77
  def buffer_range(): Text.Range = Text.Range(0, (buffer.getLength - 1) max 0)
wenzelm@44776
    78
wenzelm@44385
    79
  def perspective(): Text.Perspective =
wenzelm@44385
    80
  {
wenzelm@44385
    81
    Swing_Thread.require()
wenzelm@44473
    82
    Text.Perspective(
wenzelm@44385
    83
      for {
wenzelm@44385
    84
        doc_view <- Isabelle.document_views(buffer)
wenzelm@44473
    85
        range <- doc_view.perspective().ranges
wenzelm@44385
    86
      } yield range)
wenzelm@44385
    87
  }
wenzelm@44385
    88
wenzelm@44385
    89
wenzelm@44385
    90
  /* pending text edits */
wenzelm@43648
    91
wenzelm@43644
    92
  private object pending_edits  // owned by Swing thread
wenzelm@38224
    93
  {
wenzelm@38425
    94
    private val pending = new mutable.ListBuffer[Text.Edit]
wenzelm@44436
    95
    private var pending_perspective = false
wenzelm@44473
    96
    private var last_perspective: Text.Perspective = Text.Perspective.empty
wenzelm@44438
    97
wenzelm@38425
    98
    def snapshot(): List[Text.Edit] = pending.toList
wenzelm@38224
    99
wenzelm@43648
   100
    def flush()
wenzelm@38224
   101
    {
wenzelm@38224
   102
      Swing_Thread.require()
wenzelm@44438
   103
wenzelm@44438
   104
      val new_perspective =
wenzelm@44438
   105
        if (pending_perspective) { pending_perspective = false; perspective() }
wenzelm@44438
   106
        else last_perspective
wenzelm@44438
   107
wenzelm@43648
   108
      snapshot() match {
wenzelm@44479
   109
        case Nil if last_perspective == new_perspective =>
wenzelm@43648
   110
        case edits =>
wenzelm@43648
   111
          pending.clear
wenzelm@44438
   112
          last_perspective = new_perspective
wenzelm@44615
   113
          session.edit_node(name, node_header(), new_perspective, edits)
wenzelm@43648
   114
      }
wenzelm@38224
   115
    }
wenzelm@38224
   116
wenzelm@40478
   117
    private val delay_flush =
wenzelm@40478
   118
      Swing_Thread.delay_last(session.input_delay) { flush() }
wenzelm@40478
   119
wenzelm@38425
   120
    def +=(edit: Text.Edit)
wenzelm@38224
   121
    {
wenzelm@38224
   122
      Swing_Thread.require()
wenzelm@38224
   123
      pending += edit
wenzelm@46740
   124
      delay_flush(true)
wenzelm@38222
   125
    }
wenzelm@44436
   126
wenzelm@44436
   127
    def update_perspective()
wenzelm@44436
   128
    {
wenzelm@44436
   129
      pending_perspective = true
wenzelm@46740
   130
      delay_flush(true)
wenzelm@46740
   131
    }
wenzelm@46740
   132
wenzelm@46740
   133
    def init()
wenzelm@46740
   134
    {
wenzelm@46740
   135
      flush()
wenzelm@46740
   136
      session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
wenzelm@46740
   137
    }
wenzelm@46740
   138
wenzelm@46740
   139
    def exit()
wenzelm@46740
   140
    {
wenzelm@46740
   141
      delay_flush(false)
wenzelm@46740
   142
      flush()
wenzelm@44436
   143
    }
wenzelm@44436
   144
  }
wenzelm@44436
   145
wenzelm@44436
   146
  def update_perspective()
wenzelm@44436
   147
  {
wenzelm@44436
   148
    Swing_Thread.require()
wenzelm@44436
   149
    pending_edits.update_perspective()
wenzelm@38222
   150
  }
wenzelm@38152
   151
wenzelm@44776
   152
  def full_perspective()
wenzelm@44776
   153
  {
wenzelm@44776
   154
    pending_edits.flush()
wenzelm@44776
   155
    session.edit_node(name, node_header(), Text.Perspective(List(buffer_range())), Nil)
wenzelm@44776
   156
  }
wenzelm@44776
   157
wenzelm@38152
   158
wenzelm@38152
   159
  /* snapshot */
wenzelm@34731
   160
wenzelm@38417
   161
  def snapshot(): Document.Snapshot =
wenzelm@38417
   162
  {
wenzelm@38223
   163
    Swing_Thread.require()
wenzelm@44615
   164
    session.snapshot(name, pending_edits.snapshot())
wenzelm@38223
   165
  }
wenzelm@34828
   166
wenzelm@34828
   167
wenzelm@34828
   168
  /* buffer listener */
wenzelm@34828
   169
wenzelm@34828
   170
  private val buffer_listener: BufferListener = new BufferAdapter
wenzelm@34828
   171
  {
wenzelm@40478
   172
    override def bufferLoaded(buffer: JEditBuffer)
wenzelm@40478
   173
    {
wenzelm@40478
   174
      pending_edits.init()
wenzelm@40478
   175
    }
wenzelm@40478
   176
wenzelm@34828
   177
    override def contentInserted(buffer: JEditBuffer,
wenzelm@34828
   178
      start_line: Int, offset: Int, num_lines: Int, length: Int)
wenzelm@34828
   179
    {
wenzelm@40478
   180
      if (!buffer.isLoading)
wenzelm@40478
   181
        pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
wenzelm@34828
   182
    }
wenzelm@34828
   183
wenzelm@34828
   184
    override def preContentRemoved(buffer: JEditBuffer,
wenzelm@38426
   185
      start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
wenzelm@34828
   186
    {
wenzelm@40478
   187
      if (!buffer.isLoading)
wenzelm@40478
   188
        pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
wenzelm@34828
   189
    }
wenzelm@34828
   190
  }
wenzelm@34828
   191
wenzelm@34828
   192
wenzelm@38158
   193
  /* activation */
wenzelm@37557
   194
wenzelm@43512
   195
  private def activate()
wenzelm@34784
   196
  {
wenzelm@34784
   197
    buffer.addBufferListener(buffer_listener)
wenzelm@43512
   198
    pending_edits.init()
wenzelm@44358
   199
    Token_Markup.refresh_buffer(buffer)
immler@34680
   200
  }
immler@34680
   201
wenzelm@43512
   202
  private def deactivate()
immler@34680
   203
  {
wenzelm@46740
   204
    pending_edits.exit()
wenzelm@34784
   205
    buffer.removeBufferListener(buffer_listener)
wenzelm@44358
   206
    Token_Markup.refresh_buffer(buffer)
immler@34680
   207
  }
wenzelm@34447
   208
}