src/Tools/jEdit/src/jedit/document_model.scala
author wenzelm
Fri, 01 Jan 2010 21:53:00 +0100
changeset 34827 69852bd3c4c4
parent 34825 7f72547f9b12
child 34828 c2308b317244
permissions -rw-r--r--
tuned Change: eliminated redundant copy of document id;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34406
diff changeset
     1
/*
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
     2
 * Document model connected to jEdit buffer
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34406
diff changeset
     3
 *
aad6834ba380 added some headers and comments;
wenzelm
parents: 34406
diff changeset
     4
 * @author Fabian Immler, TU Munich
34447
wenzelm
parents: 34446
diff changeset
     5
 * @author Makarius
34407
aad6834ba380 added some headers and comments;
wenzelm
parents: 34406
diff changeset
     6
 */
aad6834ba380 added some headers and comments;
wenzelm
parents: 34406
diff changeset
     7
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
     8
package isabelle.jedit
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
     9
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    10
34823
2f3ea37c5958 renamed Proof_Document to Document;
wenzelm
parents: 34814
diff changeset
    11
import isabelle.proofdocument.{Change, Command, Edit, Insert, Remove, Document, Session}
34783
cb95d6bbf5f1 clarified BufferListener: use adapter, listen to contentInserted instead of preContentInserted;
wenzelm
parents: 34778
diff changeset
    12
34703
ff037c17332a minor tuning;
wenzelm
parents: 34696
diff changeset
    13
import scala.actors.Actor, Actor._
34693
3e995f100ad2 sealed Edit;
wenzelm
parents: 34685
diff changeset
    14
import scala.collection.mutable
34446
5c79f97ec1d1 superficial tuning;
wenzelm
parents: 34445
diff changeset
    15
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    16
import org.gjt.sp.jedit.Buffer
34783
cb95d6bbf5f1 clarified BufferListener: use adapter, listen to contentInserted instead of preContentInserted;
wenzelm
parents: 34778
diff changeset
    17
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
34649
70759ca6bb87 activation
immler@in.tum.de
parents: 34648
diff changeset
    18
import org.gjt.sp.jedit.syntax.{ModeProvider, SyntaxStyle}
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    19
34760
dc7f5e0d9d27 misc modernization of names;
wenzelm
parents: 34759
diff changeset
    20
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    21
object Document_Model
34588
e8ac8794971f superficial tuning;
wenzelm
parents: 34583
diff changeset
    22
{
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    23
  /* document model of buffer */
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    24
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    25
  private val key = "isabelle.document_model"
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    26
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    27
  def init(session: Session, buffer: Buffer): Document_Model =
34716
b8f2b44529fd tuned color (PG 4.0);
wenzelm
parents: 34712
diff changeset
    28
  {
34789
30528e68f774 some explicit Swing_Thread guards;
wenzelm
parents: 34788
diff changeset
    29
    Swing_Thread.assert()
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    30
    val model = new Document_Model(session, buffer)
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    31
    buffer.setProperty(key, model)
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    32
    model.activate()
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    33
    model
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    34
  }
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    35
34788
3779c54a2d21 direct apply for Document_Model and Document_View;
wenzelm
parents: 34784
diff changeset
    36
  def apply(buffer: Buffer): Option[Document_Model] =
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    37
  {
34789
30528e68f774 some explicit Swing_Thread guards;
wenzelm
parents: 34788
diff changeset
    38
    Swing_Thread.assert()
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    39
    buffer.getProperty(key) match {
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    40
      case model: Document_Model => Some(model)
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    41
      case _ => None
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    42
    }
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    43
  }
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    44
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    45
  def exit(buffer: Buffer)
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    46
  {
34789
30528e68f774 some explicit Swing_Thread guards;
wenzelm
parents: 34788
diff changeset
    47
    Swing_Thread.assert()
34788
3779c54a2d21 direct apply for Document_Model and Document_View;
wenzelm
parents: 34784
diff changeset
    48
    apply(buffer) match {
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    49
      case None => error("No document model for buffer: " + buffer)
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    50
      case Some(model) =>
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    51
        model.deactivate()
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    52
        buffer.unsetProperty(key)
34653
2e033aaf128e commands carrying state-information
immler@in.tum.de
parents: 34652
diff changeset
    53
    }
34318
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    54
  }
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    55
}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff changeset
    56
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    57
class Document_Model(val session: Session, val buffer: Buffer)
34588
e8ac8794971f superficial tuning;
wenzelm
parents: 34583
diff changeset
    58
{
34731
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    59
  /* changes vs. edits */
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    60
34808
e462572536e9 eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents: 34789
diff changeset
    61
  private val document_0 = session.begin_document(buffer.getName)
e462572536e9 eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents: 34789
diff changeset
    62
34827
69852bd3c4c4 tuned Change: eliminated redundant copy of document id;
wenzelm
parents: 34825
diff changeset
    63
  private val change_0 = new Change(None, Nil, Future.value(document_0, Nil))
34808
e462572536e9 eliminated global Session.document_0 -- did not work due to hardwired id;
wenzelm
parents: 34789
diff changeset
    64
  private var _changes = List(change_0)   // owned by Swing thread
34731
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    65
  def changes = _changes
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    66
  private var current_change = change_0
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    67
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    68
  private val edits = new mutable.ListBuffer[Edit]   // owned by Swing thread
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    69
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    70
  private val edits_delay = Swing_Thread.delay_last(300) {
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    71
    if (!edits.isEmpty) {
34824
ac35eee85f5c renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents: 34823
diff changeset
    72
      val new_id = session.create_id()
ac35eee85f5c renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents: 34823
diff changeset
    73
      val eds = edits.toList
ac35eee85f5c renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents: 34823
diff changeset
    74
      val change1 = current_change
34825
7f72547f9b12 use isabelle.Future;
wenzelm
parents: 34824
diff changeset
    75
      val result: Future[Document.Result] = Future.fork {
34824
ac35eee85f5c renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents: 34823
diff changeset
    76
        val old_doc = change1.document
ac35eee85f5c renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents: 34823
diff changeset
    77
        Document.text_edits(session, old_doc, new_id, eds)
ac35eee85f5c renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents: 34823
diff changeset
    78
      }
34827
69852bd3c4c4 tuned Change: eliminated redundant copy of document id;
wenzelm
parents: 34825
diff changeset
    79
      val change2 = new Change(Some(change1), eds, result)
34824
ac35eee85f5c renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents: 34823
diff changeset
    80
      _changes ::= change2
ac35eee85f5c renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents: 34823
diff changeset
    81
      session.input(change2)
ac35eee85f5c renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents: 34823
diff changeset
    82
      current_change = change2
34731
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    83
      edits.clear
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    84
    }
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    85
  }
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    86
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    87
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    88
  /* buffer listener */
34731
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    89
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    90
  private val buffer_listener: BufferListener = new BufferAdapter
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
    91
  {
34783
cb95d6bbf5f1 clarified BufferListener: use adapter, listen to contentInserted instead of preContentInserted;
wenzelm
parents: 34778
diff changeset
    92
    override def contentInserted(buffer: JEditBuffer,
34731
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    93
      start_line: Int, offset: Int, num_lines: Int, length: Int)
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    94
    {
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    95
      edits += Insert(offset, buffer.getText(offset, length))
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    96
      edits_delay()
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    97
    }
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    98
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
    99
    override def preContentRemoved(buffer: JEditBuffer,
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
   100
      start_line: Int, start: Int, num_lines: Int, removed_length: Int)
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
   101
    {
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
   102
      edits += Remove(start, buffer.getText(start, removed_length))
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
   103
      edits_delay()
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
   104
    }
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
   105
  }
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
   106
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
   107
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
   108
  /* history of changes */
34660
e0561943bfc9 Change consisting of a list of Edits
immler@in.tum.de
parents: 34654
diff changeset
   109
34824
ac35eee85f5c renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents: 34823
diff changeset
   110
  def recent_document(): Document =
ac35eee85f5c renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents: 34823
diff changeset
   111
  {
ac35eee85f5c renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents: 34823
diff changeset
   112
    def find(change: Change): Document =
34825
7f72547f9b12 use isabelle.Future;
wenzelm
parents: 34824
diff changeset
   113
      if (change.result.is_finished || !change.parent.isDefined) change.document
34824
ac35eee85f5c renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents: 34823
diff changeset
   114
      else find(change.parent.get)
ac35eee85f5c renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents: 34823
diff changeset
   115
    find(current_change)
ac35eee85f5c renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents: 34823
diff changeset
   116
  }
34654
30f588245884 arbitrary history
immler@in.tum.de
parents: 34653
diff changeset
   117
34731
c0cb6bd10eec keep BufferListener and TextAreaExtension private;
wenzelm
parents: 34724
diff changeset
   118
34680
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   119
  /* transforming offsets */
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   120
34823
2f3ea37c5958 renamed Proof_Document to Document;
wenzelm
parents: 34814
diff changeset
   121
  private def changes_from(doc: Document): List[Edit] =
34827
69852bd3c4c4 tuned Change: eliminated redundant copy of document id;
wenzelm
parents: 34825
diff changeset
   122
    List.flatten(current_change.ancestors(_.document.id == doc.id).reverse.map(_.edits)) :::
34718
39e3039645ae corrected order
immler@in.tum.de
parents: 34717
diff changeset
   123
      edits.toList
34680
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   124
34823
2f3ea37c5958 renamed Proof_Document to Document;
wenzelm
parents: 34814
diff changeset
   125
  def from_current(doc: Document, offset: Int): Int =
34718
39e3039645ae corrected order
immler@in.tum.de
parents: 34717
diff changeset
   126
    (offset /: changes_from(doc).reverse) ((i, change) => change before i)
34680
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   127
34823
2f3ea37c5958 renamed Proof_Document to Document;
wenzelm
parents: 34814
diff changeset
   128
  def to_current(doc: Document, offset: Int): Int =
34718
39e3039645ae corrected order
immler@in.tum.de
parents: 34717
diff changeset
   129
    (offset /: changes_from(doc)) ((i, change) => change after i)
34680
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   130
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   131
  def lines_of_command(cmd: Command): (Int, Int) =
34680
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   132
  {
34824
ac35eee85f5c renamed current_document to recent_document (might be a bit older than current_change);
wenzelm
parents: 34823
diff changeset
   133
    val document = recent_document()
34681
74cc10b5ba51 fixed some issues with multiple active buffers
immler@in.tum.de
parents: 34680
diff changeset
   134
    (buffer.getLineOfOffset(to_current(document, cmd.start(document))),
74cc10b5ba51 fixed some issues with multiple active buffers
immler@in.tum.de
parents: 34680
diff changeset
   135
     buffer.getLineOfOffset(to_current(document, cmd.stop(document))))
34680
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   136
  }
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   137
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   138
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   139
  /* activation */
34680
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   140
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   141
  def activate()
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   142
  {
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   143
    buffer.setTokenMarker(new Isabelle_Token_Marker(this))  // FIXME tune!?
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   144
    buffer.addBufferListener(buffer_listener)
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   145
    buffer.propertiesChanged()
34680
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   146
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   147
    edits += Insert(0, buffer.getText(0, buffer.getLength))
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   148
    edits_delay()
34680
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   149
  }
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   150
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   151
  def deactivate()
34680
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   152
  {
34784
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   153
    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
02959dcea756 split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents: 34783
diff changeset
   154
    buffer.removeBufferListener(buffer_listener)
34680
1f1f6c95de64 clarified structure of TheoryView
immler@in.tum.de
parents: 34679
diff changeset
   155
  }
34447
wenzelm
parents: 34446
diff changeset
   156
}