src/Tools/jEdit/src/document_model.scala
author wenzelm
Tue Aug 23 12:20:12 2011 +0200 (2011-08-23)
changeset 44385 e7fdb008aa7d
parent 44379 1079ab6b342b
child 44436 546adfa8a6fc
permissions -rw-r--r--
propagate editor perspective through document model;
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@44160
    48
  def init(session: Session, buffer: Buffer,
wenzelm@44160
    49
    master_dir: String, node_name: String, thy_name: String): Document_Model =
wenzelm@43397
    50
  {
wenzelm@43397
    51
    exit(buffer)
wenzelm@44160
    52
    val model = new Document_Model(session, buffer, master_dir, node_name, thy_name)
wenzelm@43397
    53
    buffer.setProperty(key, model)
wenzelm@43397
    54
    model.activate()
wenzelm@43397
    55
    model
wenzelm@43397
    56
  }
wenzelm@34318
    57
}
wenzelm@34318
    58
wenzelm@38151
    59
wenzelm@44160
    60
class Document_Model(val session: Session, val buffer: Buffer,
wenzelm@44160
    61
  val master_dir: String, val node_name: String, val thy_name: String)
wenzelm@34588
    62
{
wenzelm@44385
    63
  /* header */
wenzelm@38222
    64
wenzelm@44182
    65
  def node_header(): Exn.Result[Thy_Header] =
wenzelm@44385
    66
  {
wenzelm@44385
    67
    Swing_Thread.require()
wenzelm@44182
    68
    Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) }
wenzelm@44385
    69
  }
wenzelm@44385
    70
wenzelm@44385
    71
wenzelm@44385
    72
  /* perspective */
wenzelm@44385
    73
wenzelm@44385
    74
  def perspective(): Text.Perspective =
wenzelm@44385
    75
  {
wenzelm@44385
    76
    Swing_Thread.require()
wenzelm@44385
    77
    Text.perspective(
wenzelm@44385
    78
      for {
wenzelm@44385
    79
        doc_view <- Isabelle.document_views(buffer)
wenzelm@44385
    80
        range <- doc_view.perspective()
wenzelm@44385
    81
      } yield range)
wenzelm@44385
    82
  }
wenzelm@44385
    83
wenzelm@44385
    84
wenzelm@44385
    85
  /* pending text edits */
wenzelm@43648
    86
wenzelm@43644
    87
  private object pending_edits  // owned by Swing thread
wenzelm@38224
    88
  {
wenzelm@38425
    89
    private val pending = new mutable.ListBuffer[Text.Edit]
wenzelm@38425
    90
    def snapshot(): List[Text.Edit] = pending.toList
wenzelm@38224
    91
wenzelm@43648
    92
    def flush()
wenzelm@38224
    93
    {
wenzelm@38224
    94
      Swing_Thread.require()
wenzelm@43648
    95
      snapshot() match {
wenzelm@43648
    96
        case Nil =>
wenzelm@43648
    97
        case edits =>
wenzelm@43648
    98
          pending.clear
wenzelm@44385
    99
          session.edit_node(node_name, master_dir, node_header(), perspective(), edits)
wenzelm@43648
   100
      }
wenzelm@38224
   101
    }
wenzelm@38224
   102
wenzelm@40478
   103
    def init()
wenzelm@40478
   104
    {
wenzelm@43648
   105
      flush()
wenzelm@44385
   106
      session.init_node(node_name, master_dir,
wenzelm@44385
   107
        node_header(), perspective(), Isabelle.buffer_text(buffer))
wenzelm@40478
   108
    }
wenzelm@40478
   109
wenzelm@40478
   110
    private val delay_flush =
wenzelm@40478
   111
      Swing_Thread.delay_last(session.input_delay) { flush() }
wenzelm@40478
   112
wenzelm@38425
   113
    def +=(edit: Text.Edit)
wenzelm@38224
   114
    {
wenzelm@38224
   115
      Swing_Thread.require()
wenzelm@38224
   116
      pending += edit
wenzelm@38224
   117
      delay_flush()
wenzelm@38222
   118
    }
wenzelm@38222
   119
  }
wenzelm@38152
   120
wenzelm@38152
   121
wenzelm@38152
   122
  /* snapshot */
wenzelm@34731
   123
wenzelm@38417
   124
  def snapshot(): Document.Snapshot =
wenzelm@38417
   125
  {
wenzelm@38223
   126
    Swing_Thread.require()
wenzelm@43697
   127
    session.snapshot(node_name, pending_edits.snapshot())
wenzelm@38223
   128
  }
wenzelm@34828
   129
wenzelm@34828
   130
wenzelm@34828
   131
  /* buffer listener */
wenzelm@34828
   132
wenzelm@34828
   133
  private val buffer_listener: BufferListener = new BufferAdapter
wenzelm@34828
   134
  {
wenzelm@40478
   135
    override def bufferLoaded(buffer: JEditBuffer)
wenzelm@40478
   136
    {
wenzelm@40478
   137
      pending_edits.init()
wenzelm@40478
   138
    }
wenzelm@40478
   139
wenzelm@34828
   140
    override def contentInserted(buffer: JEditBuffer,
wenzelm@34828
   141
      start_line: Int, offset: Int, num_lines: Int, length: Int)
wenzelm@34828
   142
    {
wenzelm@40478
   143
      if (!buffer.isLoading)
wenzelm@40478
   144
        pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
wenzelm@34828
   145
    }
wenzelm@34828
   146
wenzelm@34828
   147
    override def preContentRemoved(buffer: JEditBuffer,
wenzelm@38426
   148
      start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
wenzelm@34828
   149
    {
wenzelm@40478
   150
      if (!buffer.isLoading)
wenzelm@40478
   151
        pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
wenzelm@34828
   152
    }
wenzelm@34828
   153
  }
wenzelm@34828
   154
wenzelm@34828
   155
wenzelm@38158
   156
  /* activation */
wenzelm@37557
   157
wenzelm@43512
   158
  private def activate()
wenzelm@34784
   159
  {
wenzelm@34784
   160
    buffer.addBufferListener(buffer_listener)
wenzelm@43512
   161
    pending_edits.init()
wenzelm@44358
   162
    Token_Markup.refresh_buffer(buffer)
immler@34680
   163
  }
immler@34680
   164
wenzelm@43512
   165
  private def deactivate()
immler@34680
   166
  {
wenzelm@40478
   167
    pending_edits.flush()
wenzelm@34784
   168
    buffer.removeBufferListener(buffer_listener)
wenzelm@44358
   169
    Token_Markup.refresh_buffer(buffer)
immler@34680
   170
  }
wenzelm@34447
   171
}