src/Tools/jEdit/src/jedit/document_model.scala
author wenzelm
Fri Jan 01 22:11:32 2010 +0100 (2010-01-01)
changeset 34828 c2308b317244
parent 34827 69852bd3c4c4
child 34829 e75ff2d8819e
permissions -rw-r--r--
misc tuning;
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@34823
    11
import isabelle.proofdocument.{Change, Command, Edit, Insert, Remove, 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@34789
    29
    Swing_Thread.assert()
wenzelm@34784
    30
    val model = new Document_Model(session, buffer)
wenzelm@34784
    31
    buffer.setProperty(key, model)
wenzelm@34784
    32
    model.activate()
wenzelm@34784
    33
    model
wenzelm@34784
    34
  }
wenzelm@34784
    35
wenzelm@34788
    36
  def apply(buffer: Buffer): Option[Document_Model] =
wenzelm@34784
    37
  {
wenzelm@34789
    38
    Swing_Thread.assert()
wenzelm@34784
    39
    buffer.getProperty(key) match {
wenzelm@34784
    40
      case model: Document_Model => Some(model)
wenzelm@34784
    41
      case _ => None
wenzelm@34784
    42
    }
wenzelm@34784
    43
  }
wenzelm@34784
    44
wenzelm@34784
    45
  def exit(buffer: Buffer)
wenzelm@34784
    46
  {
wenzelm@34789
    47
    Swing_Thread.assert()
wenzelm@34788
    48
    apply(buffer) match {
wenzelm@34784
    49
      case None => error("No document model for buffer: " + buffer)
wenzelm@34784
    50
      case Some(model) =>
wenzelm@34784
    51
        model.deactivate()
wenzelm@34784
    52
        buffer.unsetProperty(key)
immler@34653
    53
    }
wenzelm@34318
    54
  }
wenzelm@34318
    55
}
wenzelm@34318
    56
wenzelm@34784
    57
class Document_Model(val session: Session, val buffer: Buffer)
wenzelm@34588
    58
{
wenzelm@34828
    59
  /* history */
wenzelm@34731
    60
wenzelm@34808
    61
  private val document_0 = session.begin_document(buffer.getName)
wenzelm@34827
    62
  private val change_0 = new Change(None, Nil, Future.value(document_0, Nil))
wenzelm@34731
    63
wenzelm@34828
    64
  @volatile private var history = List(change_0)   // owned by Swing thread
wenzelm@34828
    65
  def changes = history
wenzelm@34828
    66
  def current_change: Change = history.first
wenzelm@34731
    67
wenzelm@34731
    68
wenzelm@34828
    69
    /* history of changes */
immler@34660
    70
wenzelm@34824
    71
  def recent_document(): Document =
wenzelm@34824
    72
  {
wenzelm@34824
    73
    def find(change: Change): Document =
wenzelm@34825
    74
      if (change.result.is_finished || !change.parent.isDefined) change.document
wenzelm@34824
    75
      else find(change.parent.get)
wenzelm@34824
    76
    find(current_change)
wenzelm@34824
    77
  }
immler@34654
    78
wenzelm@34731
    79
immler@34680
    80
  /* transforming offsets */
immler@34680
    81
wenzelm@34823
    82
  private def changes_from(doc: Document): List[Edit] =
wenzelm@34828
    83
  {
wenzelm@34828
    84
    Swing_Thread.assert()
wenzelm@34827
    85
    List.flatten(current_change.ancestors(_.document.id == doc.id).reverse.map(_.edits)) :::
wenzelm@34828
    86
      edits_buffer.toList
wenzelm@34828
    87
  }
immler@34680
    88
wenzelm@34823
    89
  def from_current(doc: Document, offset: Int): Int =
immler@34718
    90
    (offset /: changes_from(doc).reverse) ((i, change) => change before i)
immler@34680
    91
wenzelm@34823
    92
  def to_current(doc: Document, offset: Int): Int =
immler@34718
    93
    (offset /: changes_from(doc)) ((i, change) => change after i)
immler@34680
    94
wenzelm@34784
    95
  def lines_of_command(cmd: Command): (Int, Int) =
immler@34680
    96
  {
wenzelm@34824
    97
    val document = recent_document()
immler@34681
    98
    (buffer.getLineOfOffset(to_current(document, cmd.start(document))),
immler@34681
    99
     buffer.getLineOfOffset(to_current(document, cmd.stop(document))))
immler@34680
   100
  }
immler@34680
   101
immler@34680
   102
wenzelm@34828
   103
  /* text edits */
wenzelm@34828
   104
wenzelm@34828
   105
  private val edits_buffer = new mutable.ListBuffer[Edit]   // owned by Swing thread
wenzelm@34828
   106
wenzelm@34828
   107
  private val edits_delay = Swing_Thread.delay_last(300) {
wenzelm@34828
   108
    if (!edits_buffer.isEmpty) {
wenzelm@34828
   109
      val edits = edits_buffer.toList
wenzelm@34828
   110
      val change1 = current_change
wenzelm@34828
   111
      val result: Future[Document.Result] = Future.fork {
wenzelm@34828
   112
        Document.text_edits(session, change1.document, session.create_id(), edits)
wenzelm@34828
   113
      }
wenzelm@34828
   114
      val change2 = new Change(Some(change1), edits, result)  // FIXME edits!?
wenzelm@34828
   115
      history ::= change2
wenzelm@34828
   116
      result.map(_ => session.input(change2))
wenzelm@34828
   117
      edits_buffer.clear
wenzelm@34828
   118
    }
wenzelm@34828
   119
  }
wenzelm@34828
   120
wenzelm@34828
   121
wenzelm@34828
   122
  /* buffer listener */
wenzelm@34828
   123
wenzelm@34828
   124
  private val buffer_listener: BufferListener = new BufferAdapter
wenzelm@34828
   125
  {
wenzelm@34828
   126
    override def contentInserted(buffer: JEditBuffer,
wenzelm@34828
   127
      start_line: Int, offset: Int, num_lines: Int, length: Int)
wenzelm@34828
   128
    {
wenzelm@34828
   129
      edits_buffer += Insert(offset, buffer.getText(offset, length))
wenzelm@34828
   130
      edits_delay()
wenzelm@34828
   131
    }
wenzelm@34828
   132
wenzelm@34828
   133
    override def preContentRemoved(buffer: JEditBuffer,
wenzelm@34828
   134
      start_line: Int, start: Int, num_lines: Int, removed_length: Int)
wenzelm@34828
   135
    {
wenzelm@34828
   136
      edits_buffer += Remove(start, buffer.getText(start, removed_length))
wenzelm@34828
   137
      edits_delay()
wenzelm@34828
   138
    }
wenzelm@34828
   139
  }
wenzelm@34828
   140
wenzelm@34828
   141
wenzelm@34784
   142
  /* activation */
immler@34680
   143
wenzelm@34784
   144
  def activate()
wenzelm@34784
   145
  {
wenzelm@34828
   146
    buffer.setTokenMarker(new Isabelle_Token_Marker(this))
wenzelm@34784
   147
    buffer.addBufferListener(buffer_listener)
wenzelm@34784
   148
    buffer.propertiesChanged()
immler@34680
   149
wenzelm@34828
   150
    edits_buffer += Insert(0, buffer.getText(0, buffer.getLength))
wenzelm@34784
   151
    edits_delay()
immler@34680
   152
  }
immler@34680
   153
wenzelm@34784
   154
  def deactivate()
immler@34680
   155
  {
wenzelm@34784
   156
    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
wenzelm@34784
   157
    buffer.removeBufferListener(buffer_listener)
immler@34680
   158
  }
wenzelm@34447
   159
}