src/Tools/jEdit/src/jedit/document_model.scala
author wenzelm
Thu Nov 11 16:48:46 2010 +0100 (2010-11-11)
changeset 40478 4bae781b8f7c
parent 40474 576b88b1dce9
child 40481 da2c56aaaa68
permissions -rw-r--r--
replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
Document_Model.pending_edits: more robust treatment of init, including buffer reload event (jEdit 4.3.2 produces malformed remove/insert that lacks the last character);
tuned;
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@38222
     5
Document model connected to jEdit buffer -- single node in theory graph.
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@34693
    13
import scala.collection.mutable
wenzelm@34446
    14
wenzelm@34784
    15
import org.gjt.sp.jedit.Buffer
wenzelm@34783
    16
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
wenzelm@38158
    17
import org.gjt.sp.jedit.syntax.{SyntaxStyle, Token, TokenMarker, TokenHandler, ParserRuleSet}
wenzelm@38158
    18
import org.gjt.sp.jedit.textarea.TextArea
wenzelm@38158
    19
wenzelm@38158
    20
import java.awt.font.TextAttribute
wenzelm@38158
    21
import javax.swing.text.Segment;
wenzelm@34318
    22
wenzelm@34760
    23
wenzelm@34784
    24
object Document_Model
wenzelm@34588
    25
{
wenzelm@38158
    26
  object Token_Markup
wenzelm@38158
    27
  {
wenzelm@38158
    28
    /* extended token styles */
wenzelm@38158
    29
wenzelm@38158
    30
    private val plain_range: Int = Token.ID_COUNT
wenzelm@38158
    31
    private val full_range: Int = 3 * plain_range
wenzelm@38158
    32
    private def check_range(i: Int) { require(0 <= i && i < plain_range) }
wenzelm@38158
    33
wenzelm@38158
    34
    def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
wenzelm@38158
    35
    def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
wenzelm@38158
    36
wenzelm@38158
    37
    private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
wenzelm@38158
    38
    {
wenzelm@38158
    39
      import scala.collection.JavaConversions._
wenzelm@38158
    40
      val script_font =
wenzelm@38158
    41
        style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
wenzelm@38158
    42
      new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font)
wenzelm@38158
    43
    }
wenzelm@38158
    44
wenzelm@38158
    45
    def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
wenzelm@38158
    46
    {
wenzelm@38158
    47
      val new_styles = new Array[SyntaxStyle](full_range)
wenzelm@38158
    48
      for (i <- 0 until plain_range) {
wenzelm@38158
    49
        val style = styles(i)
wenzelm@38158
    50
        new_styles(i) = style
wenzelm@38158
    51
        new_styles(subscript(i.toByte)) = script_style(style, -1)
wenzelm@38158
    52
        new_styles(superscript(i.toByte)) = script_style(style, 1)
wenzelm@38158
    53
      }
wenzelm@38158
    54
      new_styles
wenzelm@38158
    55
    }
wenzelm@38158
    56
wenzelm@38158
    57
wenzelm@38158
    58
    /* line context */
wenzelm@38158
    59
wenzelm@38852
    60
    private val dummy_rules = new ParserRuleSet("isabelle", "MAIN")
wenzelm@38852
    61
wenzelm@38852
    62
    class Line_Context(val line: Int, prev: Line_Context)
wenzelm@38852
    63
      extends TokenMarker.LineContext(dummy_rules, prev)
wenzelm@38852
    64
    {
wenzelm@38852
    65
      override def hashCode: Int = line
wenzelm@38852
    66
      override def equals(that: Any) =
wenzelm@38852
    67
        that match {
wenzelm@38852
    68
          case other: Line_Context => line == other.line
wenzelm@38852
    69
          case _ => false
wenzelm@38852
    70
        }
wenzelm@38852
    71
    }
wenzelm@38158
    72
  }
wenzelm@38158
    73
wenzelm@38158
    74
wenzelm@34784
    75
  /* document model of buffer */
wenzelm@34784
    76
wenzelm@34784
    77
  private val key = "isabelle.document_model"
wenzelm@34784
    78
wenzelm@38222
    79
  def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
wenzelm@34716
    80
  {
wenzelm@38223
    81
    Swing_Thread.require()
wenzelm@38222
    82
    val model = new Document_Model(session, buffer, thy_name)
wenzelm@34784
    83
    buffer.setProperty(key, model)
wenzelm@34784
    84
    model.activate()
wenzelm@34784
    85
    model
wenzelm@34784
    86
  }
wenzelm@34784
    87
wenzelm@34788
    88
  def apply(buffer: Buffer): Option[Document_Model] =
wenzelm@34784
    89
  {
wenzelm@38223
    90
    Swing_Thread.require()
wenzelm@34784
    91
    buffer.getProperty(key) match {
wenzelm@34784
    92
      case model: Document_Model => Some(model)
wenzelm@34784
    93
      case _ => None
wenzelm@34784
    94
    }
wenzelm@34784
    95
  }
wenzelm@34784
    96
wenzelm@34784
    97
  def exit(buffer: Buffer)
wenzelm@34784
    98
  {
wenzelm@38223
    99
    Swing_Thread.require()
wenzelm@34788
   100
    apply(buffer) match {
wenzelm@39636
   101
      case None =>
wenzelm@34784
   102
      case Some(model) =>
wenzelm@34784
   103
        model.deactivate()
wenzelm@34784
   104
        buffer.unsetProperty(key)
immler@34653
   105
    }
wenzelm@34318
   106
  }
wenzelm@34318
   107
}
wenzelm@34318
   108
wenzelm@38151
   109
wenzelm@38222
   110
class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
wenzelm@34588
   111
{
wenzelm@38224
   112
  /* pending text edits */
wenzelm@38222
   113
wenzelm@38224
   114
  object pending_edits  // owned by Swing thread
wenzelm@38224
   115
  {
wenzelm@38425
   116
    private val pending = new mutable.ListBuffer[Text.Edit]
wenzelm@38425
   117
    def snapshot(): List[Text.Edit] = pending.toList
wenzelm@38224
   118
wenzelm@40478
   119
    def flush(more_edits: Option[List[Text.Edit]]*)
wenzelm@38224
   120
    {
wenzelm@38224
   121
      Swing_Thread.require()
wenzelm@38224
   122
      val edits = snapshot()
wenzelm@38224
   123
      pending.clear
wenzelm@40478
   124
wenzelm@40478
   125
      if (!edits.isEmpty || !more_edits.isEmpty)
wenzelm@40478
   126
        session.edit_version((Some(edits) :: more_edits.toList).map((thy_name, _)))
wenzelm@38224
   127
    }
wenzelm@38224
   128
wenzelm@40478
   129
    def init()
wenzelm@40478
   130
    {
wenzelm@40478
   131
      Swing_Thread.require()
wenzelm@40478
   132
      flush(None, Some(List(Text.Edit.insert(0, Isabelle.buffer_text(buffer)))))
wenzelm@40478
   133
    }
wenzelm@40478
   134
wenzelm@40478
   135
    private val delay_flush =
wenzelm@40478
   136
      Swing_Thread.delay_last(session.input_delay) { flush() }
wenzelm@40478
   137
wenzelm@38425
   138
    def +=(edit: Text.Edit)
wenzelm@38224
   139
    {
wenzelm@38224
   140
      Swing_Thread.require()
wenzelm@38224
   141
      pending += edit
wenzelm@38224
   142
      delay_flush()
wenzelm@38222
   143
    }
wenzelm@38222
   144
  }
wenzelm@38152
   145
wenzelm@38152
   146
wenzelm@38152
   147
  /* snapshot */
wenzelm@34731
   148
wenzelm@38417
   149
  def snapshot(): Document.Snapshot =
wenzelm@38417
   150
  {
wenzelm@38223
   151
    Swing_Thread.require()
wenzelm@38359
   152
    session.snapshot(thy_name, pending_edits.snapshot())
wenzelm@38223
   153
  }
wenzelm@34828
   154
wenzelm@34828
   155
wenzelm@34828
   156
  /* buffer listener */
wenzelm@34828
   157
wenzelm@34828
   158
  private val buffer_listener: BufferListener = new BufferAdapter
wenzelm@34828
   159
  {
wenzelm@40478
   160
    override def bufferLoaded(buffer: JEditBuffer)
wenzelm@40478
   161
    {
wenzelm@40478
   162
      pending_edits.init()
wenzelm@40478
   163
    }
wenzelm@40478
   164
wenzelm@34828
   165
    override def contentInserted(buffer: JEditBuffer,
wenzelm@34828
   166
      start_line: Int, offset: Int, num_lines: Int, length: Int)
wenzelm@34828
   167
    {
wenzelm@40478
   168
      if (!buffer.isLoading)
wenzelm@40478
   169
        pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
wenzelm@34828
   170
    }
wenzelm@34828
   171
wenzelm@34828
   172
    override def preContentRemoved(buffer: JEditBuffer,
wenzelm@38426
   173
      start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
wenzelm@34828
   174
    {
wenzelm@40478
   175
      if (!buffer.isLoading)
wenzelm@40478
   176
        pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
wenzelm@34828
   177
    }
wenzelm@34828
   178
  }
wenzelm@34828
   179
wenzelm@34828
   180
wenzelm@38158
   181
  /* semantic token marker */
wenzelm@38158
   182
wenzelm@38158
   183
  private val token_marker = new TokenMarker
wenzelm@38158
   184
  {
wenzelm@38158
   185
    override def markTokens(prev: TokenMarker.LineContext,
wenzelm@38158
   186
        handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
wenzelm@38158
   187
    {
wenzelm@38843
   188
      Isabelle.swing_buffer_lock(buffer) {
wenzelm@38843
   189
        val snapshot = Document_Model.this.snapshot()
wenzelm@38572
   190
wenzelm@38852
   191
        val previous = prev.asInstanceOf[Document_Model.Token_Markup.Line_Context]
wenzelm@38641
   192
        val line = if (prev == null) 0 else previous.line + 1
wenzelm@38852
   193
        val context = new Document_Model.Token_Markup.Line_Context(line, previous)
wenzelm@38572
   194
wenzelm@38641
   195
        val start = buffer.getLineStartOffset(line)
wenzelm@38641
   196
        val stop = start + line_segment.count
wenzelm@38158
   197
wenzelm@38641
   198
        /* FIXME
wenzelm@38641
   199
        for (text_area <- Isabelle.jedit_text_areas(buffer)
wenzelm@38641
   200
              if Document_View(text_area).isDefined)
wenzelm@38641
   201
          Document_View(text_area).get.set_styles()
wenzelm@38641
   202
        */
wenzelm@38158
   203
wenzelm@38641
   204
        def handle_token(style: Byte, offset: Text.Offset, length: Int) =
wenzelm@38641
   205
          handler.handleToken(line_segment, style, offset, length, context)
immler@34680
   206
wenzelm@38641
   207
        val syntax = session.current_syntax()
wenzelm@39179
   208
        val tokens = snapshot.select_markup(Text.Range(start, stop))(Isabelle_Markup.tokens(syntax))
wenzelm@38572
   209
wenzelm@38846
   210
        var last = start
wenzelm@39179
   211
        for (token <- tokens.iterator) {
wenzelm@38846
   212
          val Text.Range(token_start, token_stop) = token.range
wenzelm@38846
   213
          if (last < token_start)
wenzelm@38846
   214
            handle_token(Token.COMMENT1, last - start, token_start - last)
wenzelm@39177
   215
          handle_token(token.info getOrElse Token.NULL,
wenzelm@39177
   216
            token_start - start, token_stop - token_start)
wenzelm@38846
   217
          last = token_stop
wenzelm@38641
   218
        }
wenzelm@39179
   219
        if (last < stop) handle_token(Token.COMMENT1, last - start, stop - last)
wenzelm@38641
   220
wenzelm@38641
   221
        handle_token(Token.END, line_segment.count, 0)
wenzelm@38641
   222
        handler.setLineContext(context)
wenzelm@38641
   223
        context
wenzelm@38572
   224
      }
wenzelm@38158
   225
    }
wenzelm@38158
   226
  }
wenzelm@38158
   227
wenzelm@38158
   228
wenzelm@38158
   229
  /* activation */
wenzelm@37557
   230
wenzelm@34784
   231
  def activate()
wenzelm@34784
   232
  {
wenzelm@37557
   233
    buffer.setTokenMarker(token_marker)
wenzelm@34784
   234
    buffer.addBufferListener(buffer_listener)
wenzelm@34784
   235
    buffer.propertiesChanged()
wenzelm@40478
   236
    pending_edits.init()
immler@34680
   237
  }
immler@34680
   238
wenzelm@37557
   239
  def refresh()
wenzelm@37557
   240
  {
wenzelm@37557
   241
    buffer.setTokenMarker(token_marker)
wenzelm@37557
   242
  }
wenzelm@37557
   243
wenzelm@34784
   244
  def deactivate()
immler@34680
   245
  {
wenzelm@40478
   246
    pending_edits.flush()
wenzelm@34784
   247
    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
wenzelm@34784
   248
    buffer.removeBufferListener(buffer_listener)
immler@34680
   249
  }
wenzelm@34447
   250
}