src/Tools/jEdit/src/jedit/document_model.scala
author wenzelm
Thu Aug 05 16:58:18 2010 +0200 (2010-08-05)
changeset 38151 2837c952ca31
parent 38150 67fc24df3721
child 38152 eab0d1c2e46e
permissions -rw-r--r--
explicit Change.Snapshot and Document.Node;
misc tuning and clarification;
Document_View: explicitly highlight outdated command status;
wenzelm@36760
     1
/*  Title:      Tools/jEdit/src/jedit/document_model.scala
wenzelm@36760
     2
    Author:     Fabian Immler, TU Munich
wenzelm@36760
     3
    Author:     Makarius
wenzelm@36760
     4
wenzelm@36760
     5
Document model connected to jEdit buffer.
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@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@38151
    57
wenzelm@34784
    58
class Document_Model(val session: Session, val buffer: Buffer)
wenzelm@34588
    59
{
wenzelm@37555
    60
  /* visible line end */
wenzelm@37555
    61
wenzelm@37555
    62
  // simplify slightly odd result of TextArea.getLineEndOffset
wenzelm@37555
    63
  // NB: jEdit already normalizes \r\n and \r to \n
wenzelm@37555
    64
  def visible_line_end(start: Int, end: Int): Int =
wenzelm@37555
    65
  {
wenzelm@37555
    66
    val end1 = end - 1
wenzelm@37555
    67
    if (start <= end1 && end1 < buffer.getLength &&
wenzelm@37555
    68
        buffer.getSegment(end1, 1).charAt(0) == '\n') end1
wenzelm@37555
    69
    else end
wenzelm@37555
    70
  }
wenzelm@37555
    71
wenzelm@37555
    72
wenzelm@34828
    73
  /* history */
wenzelm@34731
    74
wenzelm@38150
    75
  // FIXME proper error handling
wenzelm@38150
    76
  val thy_name = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))._2
wenzelm@34833
    77
wenzelm@38150
    78
  @volatile private var history = Change.init // owned by Swing thread
wenzelm@34731
    79
wenzelm@34830
    80
  def current_change(): Change = history
wenzelm@38151
    81
  def snapshot(): Change.Snapshot = current_change().snapshot(thy_name)
immler@34654
    82
wenzelm@34731
    83
immler@34680
    84
  /* transforming offsets */
immler@34680
    85
wenzelm@34838
    86
  private def changes_from(doc: Document): List[Text_Edit] =
wenzelm@34828
    87
  {
wenzelm@34828
    88
    Swing_Thread.assert()
wenzelm@34833
    89
    (edits_buffer.toList /:
wenzelm@38150
    90
      current_change.ancestors.takeWhile(_.id != doc.id))((edits, change) =>
wenzelm@38150
    91
        (for ((name, eds) <- change.edits if name == thy_name) yield eds).flatten ::: edits)
wenzelm@34828
    92
  }
immler@34680
    93
wenzelm@34823
    94
  def from_current(doc: Document, offset: Int): Int =
immler@34718
    95
    (offset /: changes_from(doc).reverse) ((i, change) => change before i)
immler@34680
    96
wenzelm@34823
    97
  def to_current(doc: Document, offset: Int): Int =
immler@34718
    98
    (offset /: changes_from(doc)) ((i, change) => change after i)
immler@34680
    99
immler@34680
   100
wenzelm@34828
   101
  /* text edits */
wenzelm@34828
   102
wenzelm@34838
   103
  private val edits_buffer = new mutable.ListBuffer[Text_Edit]   // owned by Swing thread
wenzelm@34828
   104
wenzelm@37849
   105
  private val edits_delay = Swing_Thread.delay_last(session.input_delay) {
wenzelm@34828
   106
    if (!edits_buffer.isEmpty) {
wenzelm@38150
   107
      val new_change = current_change().edit(session, List((thy_name, edits_buffer.toList)))
wenzelm@34828
   108
      edits_buffer.clear
wenzelm@34853
   109
      history = new_change
wenzelm@34853
   110
      new_change.result.map(_ => session.input(new_change))
wenzelm@34828
   111
    }
wenzelm@34828
   112
  }
wenzelm@34828
   113
wenzelm@34828
   114
wenzelm@34828
   115
  /* buffer listener */
wenzelm@34828
   116
wenzelm@34828
   117
  private val buffer_listener: BufferListener = new BufferAdapter
wenzelm@34828
   118
  {
wenzelm@34828
   119
    override def contentInserted(buffer: JEditBuffer,
wenzelm@34828
   120
      start_line: Int, offset: Int, num_lines: Int, length: Int)
wenzelm@34828
   121
    {
wenzelm@34864
   122
      edits_buffer += new Text_Edit(true, offset, buffer.getText(offset, length))
wenzelm@34828
   123
      edits_delay()
wenzelm@34828
   124
    }
wenzelm@34828
   125
wenzelm@34828
   126
    override def preContentRemoved(buffer: JEditBuffer,
wenzelm@34828
   127
      start_line: Int, start: Int, num_lines: Int, removed_length: Int)
wenzelm@34828
   128
    {
wenzelm@34864
   129
      edits_buffer += new Text_Edit(false, start, buffer.getText(start, removed_length))
wenzelm@34828
   130
      edits_delay()
wenzelm@34828
   131
    }
wenzelm@34828
   132
  }
wenzelm@34828
   133
wenzelm@34828
   134
wenzelm@34784
   135
  /* activation */
immler@34680
   136
wenzelm@37557
   137
  private val token_marker = new Isabelle_Token_Marker(this)
wenzelm@37557
   138
wenzelm@34784
   139
  def activate()
wenzelm@34784
   140
  {
wenzelm@37557
   141
    buffer.setTokenMarker(token_marker)
wenzelm@34784
   142
    buffer.addBufferListener(buffer_listener)
wenzelm@34784
   143
    buffer.propertiesChanged()
immler@34680
   144
wenzelm@34864
   145
    edits_buffer += new Text_Edit(true, 0, buffer.getText(0, buffer.getLength))
wenzelm@34784
   146
    edits_delay()
immler@34680
   147
  }
immler@34680
   148
wenzelm@37557
   149
  def refresh()
wenzelm@37557
   150
  {
wenzelm@37557
   151
    buffer.setTokenMarker(token_marker)
wenzelm@37557
   152
  }
wenzelm@37557
   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
}