1.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Fri Jan 01 21:53:00 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Fri Jan 01 22:11:32 2010 +0100
     1.3 @@ -56,56 +56,17 @@
     1.4  
     1.5  class Document_Model(val session: Session, val buffer: Buffer)
     1.6  {
     1.7 -  /* changes vs. edits */
     1.8 +  /* history */
     1.9  
    1.10    private val document_0 = session.begin_document(buffer.getName)
    1.11 +  private val change_0 = new Change(None, Nil, Future.value(document_0, Nil))
    1.12  
    1.13 -  private val change_0 = new Change(None, Nil, Future.value(document_0, Nil))
    1.14 -  private var _changes = List(change_0)   // owned by Swing thread
    1.15 -  def changes = _changes
    1.16 -  private var current_change = change_0
    1.17 +  @volatile private var history = List(change_0)   // owned by Swing thread
    1.18 +  def changes = history
    1.19 +  def current_change: Change = history.first
    1.20  
    1.21 -  private val edits = new mutable.ListBuffer[Edit]   // owned by Swing thread
    1.22  
    1.23 -  private val edits_delay = Swing_Thread.delay_last(300) {
    1.24 -    if (!edits.isEmpty) {
    1.25 -      val new_id = session.create_id()
    1.26 -      val eds = edits.toList
    1.27 -      val change1 = current_change
    1.28 -      val result: Future[Document.Result] = Future.fork {
    1.29 -        val old_doc = change1.document
    1.30 -        Document.text_edits(session, old_doc, new_id, eds)
    1.31 -      }
    1.32 -      val change2 = new Change(Some(change1), eds, result)
    1.33 -      _changes ::= change2
    1.34 -      session.input(change2)
    1.35 -      current_change = change2
    1.36 -      edits.clear
    1.37 -    }
    1.38 -  }
    1.39 -
    1.40 -
    1.41 -  /* buffer listener */
    1.42 -
    1.43 -  private val buffer_listener: BufferListener = new BufferAdapter
    1.44 -  {
    1.45 -    override def contentInserted(buffer: JEditBuffer,
    1.46 -      start_line: Int, offset: Int, num_lines: Int, length: Int)
    1.47 -    {
    1.48 -      edits += Insert(offset, buffer.getText(offset, length))
    1.49 -      edits_delay()
    1.50 -    }
    1.51 -
    1.52 -    override def preContentRemoved(buffer: JEditBuffer,
    1.53 -      start_line: Int, start: Int, num_lines: Int, removed_length: Int)
    1.54 -    {
    1.55 -      edits += Remove(start, buffer.getText(start, removed_length))
    1.56 -      edits_delay()
    1.57 -    }
    1.58 -  }
    1.59 -
    1.60 -
    1.61 -  /* history of changes */
    1.62 +    /* history of changes */
    1.63  
    1.64    def recent_document(): Document =
    1.65    {
    1.66 @@ -119,8 +80,11 @@
    1.67    /* transforming offsets */
    1.68  
    1.69    private def changes_from(doc: Document): List[Edit] =
    1.70 +  {
    1.71 +    Swing_Thread.assert()
    1.72      List.flatten(current_change.ancestors(_.document.id == doc.id).reverse.map(_.edits)) :::
    1.73 -      edits.toList
    1.74 +      edits_buffer.toList
    1.75 +  }
    1.76  
    1.77    def from_current(doc: Document, offset: Int): Int =
    1.78      (offset /: changes_from(doc).reverse) ((i, change) => change before i)
    1.79 @@ -136,15 +100,54 @@
    1.80    }
    1.81  
    1.82  
    1.83 +  /* text edits */
    1.84 +
    1.85 +  private val edits_buffer = new mutable.ListBuffer[Edit]   // owned by Swing thread
    1.86 +
    1.87 +  private val edits_delay = Swing_Thread.delay_last(300) {
    1.88 +    if (!edits_buffer.isEmpty) {
    1.89 +      val edits = edits_buffer.toList
    1.90 +      val change1 = current_change
    1.91 +      val result: Future[Document.Result] = Future.fork {
    1.92 +        Document.text_edits(session, change1.document, session.create_id(), edits)
    1.93 +      }
    1.94 +      val change2 = new Change(Some(change1), edits, result)  // FIXME edits!?
    1.95 +      history ::= change2
    1.96 +      result.map(_ => session.input(change2))
    1.97 +      edits_buffer.clear
    1.98 +    }
    1.99 +  }
   1.100 +
   1.101 +
   1.102 +  /* buffer listener */
   1.103 +
   1.104 +  private val buffer_listener: BufferListener = new BufferAdapter
   1.105 +  {
   1.106 +    override def contentInserted(buffer: JEditBuffer,
   1.107 +      start_line: Int, offset: Int, num_lines: Int, length: Int)
   1.108 +    {
   1.109 +      edits_buffer += Insert(offset, buffer.getText(offset, length))
   1.110 +      edits_delay()
   1.111 +    }
   1.112 +
   1.113 +    override def preContentRemoved(buffer: JEditBuffer,
   1.114 +      start_line: Int, start: Int, num_lines: Int, removed_length: Int)
   1.115 +    {
   1.116 +      edits_buffer += Remove(start, buffer.getText(start, removed_length))
   1.117 +      edits_delay()
   1.118 +    }
   1.119 +  }
   1.120 +
   1.121 +
   1.122    /* activation */
   1.123  
   1.124    def activate()
   1.125    {
   1.126 -    buffer.setTokenMarker(new Isabelle_Token_Marker(this))  // FIXME tune!?
   1.127 +    buffer.setTokenMarker(new Isabelle_Token_Marker(this))
   1.128      buffer.addBufferListener(buffer_listener)
   1.129      buffer.propertiesChanged()
   1.130  
   1.131 -    edits += Insert(0, buffer.getText(0, buffer.getLength))
   1.132 +    edits_buffer += Insert(0, buffer.getText(0, buffer.getLength))
   1.133      edits_delay()
   1.134    }
   1.135