src/Tools/jEdit/src/jedit/document_model.scala
author wenzelm
Tue Dec 15 20:20:07 2009 +0100 (2009-12-15)
changeset 34788 3779c54a2d21
parent 34784 02959dcea756
child 34789 30528e68f774
permissions -rw-r--r--
direct apply for Document_Model and Document_View;
wenzelm@34407
     1
/*
wenzelm@34784
     2
 * Document model connected to jEdit buffer
wenzelm@34407
     3
 *
wenzelm@34407
     4
 * @author Fabian Immler, TU Munich
wenzelm@34447
     5
 * @author Makarius
wenzelm@34407
     6
 */
wenzelm@34407
     7
wenzelm@34784
     8
package isabelle.jedit
wenzelm@34760
     9
wenzelm@34318
    10
wenzelm@34784
    11
import isabelle.proofdocument.{Change, Command, Edit, Insert, Remove, Proof_Document, Session}
wenzelm@34783
    12
wenzelm@34703
    13
import scala.actors.Actor, Actor._
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}
immler@34649
    18
import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
wenzelm@34318
    19
wenzelm@34760
    20
wenzelm@34784
    21
object Document_Model
wenzelm@34588
    22
{
wenzelm@34784
    23
  /* document model of buffer */
wenzelm@34784
    24
wenzelm@34784
    25
  private val key = "isabelle.document_model"
wenzelm@34784
    26
wenzelm@34784
    27
  def init(session: Session, buffer: Buffer): Document_Model =
wenzelm@34716
    28
  {
wenzelm@34784
    29
    val model = new Document_Model(session, buffer)
wenzelm@34784
    30
    buffer.setProperty(key, model)
wenzelm@34784
    31
    model.activate()
wenzelm@34784
    32
    model
wenzelm@34784
    33
  }
wenzelm@34784
    34
wenzelm@34788
    35
  def apply(buffer: Buffer): Option[Document_Model] =
wenzelm@34784
    36
  {
wenzelm@34784
    37
    buffer.getProperty(key) match {
wenzelm@34784
    38
      case model: Document_Model => Some(model)
wenzelm@34784
    39
      case _ => None
wenzelm@34784
    40
    }
wenzelm@34784
    41
  }
wenzelm@34784
    42
wenzelm@34784
    43
  def exit(buffer: Buffer)
wenzelm@34784
    44
  {
wenzelm@34788
    45
    apply(buffer) match {
wenzelm@34784
    46
      case None => error("No document model for buffer: " + buffer)
wenzelm@34784
    47
      case Some(model) =>
wenzelm@34784
    48
        model.deactivate()
wenzelm@34784
    49
        buffer.unsetProperty(key)
immler@34653
    50
    }
wenzelm@34318
    51
  }
wenzelm@34318
    52
}
wenzelm@34318
    53
wenzelm@34784
    54
class Document_Model(val session: Session, val buffer: Buffer)
wenzelm@34588
    55
{
wenzelm@34731
    56
  /* changes vs. edits */
wenzelm@34731
    57
wenzelm@34777
    58
  private val change_0 = new Change(Isabelle.session.document_0.id, None, Nil)  // FIXME !?
wenzelm@34731
    59
  private var _changes = List(change_0)   // owned by Swing/AWT thread
wenzelm@34731
    60
  def changes = _changes
wenzelm@34731
    61
  private var current_change = change_0
wenzelm@34731
    62
wenzelm@34731
    63
  private val edits = new mutable.ListBuffer[Edit]   // owned by Swing thread
wenzelm@34731
    64
wenzelm@34731
    65
  private val edits_delay = Swing_Thread.delay_last(300) {
wenzelm@34731
    66
    if (!edits.isEmpty) {
wenzelm@34778
    67
      val change = new Change(session.create_id(), Some(current_change), edits.toList)
wenzelm@34731
    68
      _changes ::= change
wenzelm@34777
    69
      session.input(change)
wenzelm@34731
    70
      current_change = change
wenzelm@34731
    71
      edits.clear
wenzelm@34731
    72
    }
wenzelm@34731
    73
  }
wenzelm@34731
    74
wenzelm@34731
    75
wenzelm@34784
    76
  /* buffer listener */
wenzelm@34731
    77
wenzelm@34784
    78
  private val buffer_listener: BufferListener = new BufferAdapter
wenzelm@34784
    79
  {
wenzelm@34783
    80
    override def contentInserted(buffer: JEditBuffer,
wenzelm@34731
    81
      start_line: Int, offset: Int, num_lines: Int, length: Int)
wenzelm@34731
    82
    {
wenzelm@34731
    83
      edits += Insert(offset, buffer.getText(offset, length))
wenzelm@34731
    84
      edits_delay()
wenzelm@34731
    85
    }
wenzelm@34731
    86
wenzelm@34731
    87
    override def preContentRemoved(buffer: JEditBuffer,
wenzelm@34731
    88
      start_line: Int, start: Int, num_lines: Int, removed_length: Int)
wenzelm@34731
    89
    {
wenzelm@34731
    90
      edits += Remove(start, buffer.getText(start, removed_length))
wenzelm@34731
    91
      edits_delay()
wenzelm@34731
    92
    }
wenzelm@34731
    93
  }
wenzelm@34731
    94
wenzelm@34731
    95
wenzelm@34731
    96
  /* history of changes */
immler@34660
    97
wenzelm@34760
    98
  private def doc_or_pred(c: Change): Proof_Document =
wenzelm@34777
    99
    session.document(c.id).getOrElse(doc_or_pred(c.parent.get))
wenzelm@34731
   100
immler@34654
   101
  def current_document() = doc_or_pred(current_change)
immler@34654
   102
wenzelm@34731
   103
immler@34654
   104
  /* update to desired version */
immler@34654
   105
wenzelm@34784
   106
  def set_version(goal: Change)
wenzelm@34784
   107
  {
immler@34654
   108
    // changes in buffer must be ignored
wenzelm@34731
   109
    buffer.removeBufferListener(buffer_listener)
immler@34654
   110
wenzelm@34784
   111
    def apply(change: Change): Unit =
wenzelm@34784
   112
      change.edits.foreach {
wenzelm@34784
   113
        case Insert(start, text) => buffer.insert(start, text)
wenzelm@34784
   114
        case Remove(start, text) => buffer.remove(start, text.length)
wenzelm@34784
   115
      }
immler@34660
   116
wenzelm@34784
   117
    def unapply(change: Change): Unit =
wenzelm@34784
   118
      change.edits.reverse.foreach {
wenzelm@34784
   119
        case Insert(start, text) => buffer.remove(start, text.length)
wenzelm@34784
   120
        case Remove(start, text) => buffer.insert(start, text)
wenzelm@34784
   121
      }
wenzelm@34318
   122
immler@34654
   123
    // undo/redo changes
immler@34654
   124
    val ancs_current = current_change.ancestors
immler@34654
   125
    val ancs_goal = goal.ancestors
immler@34654
   126
    val paired = ancs_current.reverse zip ancs_goal.reverse
immler@34654
   127
    def last_common[A](xs: List[(A, A)]): Option[A] = {
immler@34654
   128
      xs match {
immler@34654
   129
        case (x, y) :: xs =>
immler@34654
   130
          if (x == y)
immler@34654
   131
            xs match {
immler@34654
   132
              case (a, b) :: ys =>
immler@34654
   133
                if (a == b) last_common(xs)
immler@34654
   134
                else Some(x)
immler@34654
   135
              case _ => Some(x)
immler@34654
   136
            }
immler@34654
   137
          else None
immler@34654
   138
        case _ => None
immler@34654
   139
      }
immler@34654
   140
    }
immler@34654
   141
    val common_anc = last_common(paired).get
immler@34654
   142
immler@34654
   143
    ancs_current.takeWhile(_ != common_anc) map unapply
immler@34654
   144
    ancs_goal.takeWhile(_ != common_anc).reverse map apply
immler@34654
   145
immler@34654
   146
    current_change = goal
immler@34654
   147
    // invoke repaint
immler@34679
   148
    buffer.propertiesChanged()
wenzelm@34784
   149
    // invalidate_all()  FIXME
wenzelm@34784
   150
    // overview.repaint()  FIXME
immler@34654
   151
wenzelm@34703
   152
    // track changes in buffer
wenzelm@34731
   153
    buffer.addBufferListener(buffer_listener)
wenzelm@34318
   154
  }
wenzelm@34446
   155
wenzelm@34693
   156
immler@34680
   157
  /* transforming offsets */
immler@34680
   158
wenzelm@34760
   159
  private def changes_from(doc: Proof_Document): List[Edit] =
immler@34718
   160
    List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
immler@34718
   161
      edits.toList
immler@34680
   162
wenzelm@34760
   163
  def from_current(doc: Proof_Document, offset: Int): Int =
immler@34718
   164
    (offset /: changes_from(doc).reverse) ((i, change) => change before i)
immler@34680
   165
wenzelm@34760
   166
  def to_current(doc: Proof_Document, offset: Int): Int =
immler@34718
   167
    (offset /: changes_from(doc)) ((i, change) => change after i)
immler@34680
   168
wenzelm@34784
   169
  def lines_of_command(cmd: Command): (Int, Int) =
immler@34680
   170
  {
immler@34680
   171
    val document = current_document()
immler@34681
   172
    (buffer.getLineOfOffset(to_current(document, cmd.start(document))),
immler@34681
   173
     buffer.getLineOfOffset(to_current(document, cmd.stop(document))))
immler@34680
   174
  }
immler@34680
   175
immler@34680
   176
wenzelm@34784
   177
  /* activation */
immler@34680
   178
wenzelm@34784
   179
  def activate()
wenzelm@34784
   180
  {
wenzelm@34784
   181
    buffer.setTokenMarker(new Isabelle_Token_Marker(this))  // FIXME tune!?
wenzelm@34784
   182
    buffer.addBufferListener(buffer_listener)
wenzelm@34784
   183
    buffer.propertiesChanged()
immler@34680
   184
wenzelm@34784
   185
    edits += Insert(0, buffer.getText(0, buffer.getLength))
wenzelm@34784
   186
    edits_delay()
immler@34680
   187
  }
immler@34680
   188
wenzelm@34784
   189
  def deactivate()
immler@34680
   190
  {
wenzelm@34784
   191
    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
wenzelm@34784
   192
    buffer.removeBufferListener(buffer_listener)
immler@34680
   193
  }
wenzelm@34447
   194
}