src/Tools/jEdit/src/jedit/document_model.scala
author wenzelm
Sun Aug 15 21:42:13 2010 +0200 (2010-08-15)
changeset 38425 e467db701d78
parent 38417 b8922ae21111
child 38426 2858ec7b6dd8
permissions -rw-r--r--
moved Text_Edit to Text.Edit;
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@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}
wenzelm@38158
    18
import org.gjt.sp.jedit.syntax.{SyntaxStyle, Token, TokenMarker, TokenHandler, ParserRuleSet}
wenzelm@38158
    19
import org.gjt.sp.jedit.textarea.TextArea
wenzelm@38158
    20
wenzelm@38158
    21
import java.awt.font.TextAttribute
wenzelm@38158
    22
import javax.swing.text.Segment;
wenzelm@34318
    23
wenzelm@34760
    24
wenzelm@34784
    25
object Document_Model
wenzelm@34588
    26
{
wenzelm@38158
    27
  object Token_Markup
wenzelm@38158
    28
  {
wenzelm@38158
    29
    /* extended token styles */
wenzelm@38158
    30
wenzelm@38158
    31
    private val plain_range: Int = Token.ID_COUNT
wenzelm@38158
    32
    private val full_range: Int = 3 * plain_range
wenzelm@38158
    33
    private def check_range(i: Int) { require(0 <= i && i < plain_range) }
wenzelm@38158
    34
wenzelm@38158
    35
    def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
wenzelm@38158
    36
    def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
wenzelm@38158
    37
wenzelm@38158
    38
    private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
wenzelm@38158
    39
    {
wenzelm@38158
    40
      import scala.collection.JavaConversions._
wenzelm@38158
    41
      val script_font =
wenzelm@38158
    42
        style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
wenzelm@38158
    43
      new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font)
wenzelm@38158
    44
    }
wenzelm@38158
    45
wenzelm@38158
    46
    def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
wenzelm@38158
    47
    {
wenzelm@38158
    48
      val new_styles = new Array[SyntaxStyle](full_range)
wenzelm@38158
    49
      for (i <- 0 until plain_range) {
wenzelm@38158
    50
        val style = styles(i)
wenzelm@38158
    51
        new_styles(i) = style
wenzelm@38158
    52
        new_styles(subscript(i.toByte)) = script_style(style, -1)
wenzelm@38158
    53
        new_styles(superscript(i.toByte)) = script_style(style, 1)
wenzelm@38158
    54
      }
wenzelm@38158
    55
      new_styles
wenzelm@38158
    56
    }
wenzelm@38158
    57
wenzelm@38158
    58
wenzelm@38158
    59
    /* line context */
wenzelm@38158
    60
wenzelm@38158
    61
    private val rule_set = new ParserRuleSet("isabelle", "MAIN")
wenzelm@38158
    62
    class LineContext(val line: Int, prev: LineContext)
wenzelm@38158
    63
      extends TokenMarker.LineContext(rule_set, prev)
wenzelm@38158
    64
wenzelm@38158
    65
wenzelm@38158
    66
    /* mapping to jEdit token types */
wenzelm@38158
    67
    // TODO: as properties or CSS style sheet
wenzelm@38158
    68
wenzelm@38158
    69
    val command_style: Map[String, Byte] =
wenzelm@38158
    70
    {
wenzelm@38158
    71
      import Token._
wenzelm@38158
    72
      Map[String, Byte](
wenzelm@38158
    73
        Keyword.THY_END -> KEYWORD2,
wenzelm@38158
    74
        Keyword.THY_SCRIPT -> LABEL,
wenzelm@38158
    75
        Keyword.PRF_SCRIPT -> LABEL,
wenzelm@38158
    76
        Keyword.PRF_ASM -> KEYWORD3,
wenzelm@38158
    77
        Keyword.PRF_ASM_GOAL -> KEYWORD3
wenzelm@38158
    78
      ).withDefaultValue(KEYWORD1)
wenzelm@38158
    79
    }
wenzelm@38158
    80
wenzelm@38158
    81
    val token_style: Map[String, Byte] =
wenzelm@38158
    82
    {
wenzelm@38158
    83
      import Token._
wenzelm@38158
    84
      Map[String, Byte](
wenzelm@38158
    85
        // logical entities
wenzelm@38158
    86
        Markup.TCLASS -> NULL,
wenzelm@38158
    87
        Markup.TYCON -> NULL,
wenzelm@38158
    88
        Markup.FIXED_DECL -> FUNCTION,
wenzelm@38158
    89
        Markup.FIXED -> NULL,
wenzelm@38158
    90
        Markup.CONST_DECL -> FUNCTION,
wenzelm@38158
    91
        Markup.CONST -> NULL,
wenzelm@38158
    92
        Markup.FACT_DECL -> FUNCTION,
wenzelm@38158
    93
        Markup.FACT -> NULL,
wenzelm@38158
    94
        Markup.DYNAMIC_FACT -> LABEL,
wenzelm@38158
    95
        Markup.LOCAL_FACT_DECL -> FUNCTION,
wenzelm@38158
    96
        Markup.LOCAL_FACT -> NULL,
wenzelm@38158
    97
        // inner syntax
wenzelm@38158
    98
        Markup.TFREE -> NULL,
wenzelm@38158
    99
        Markup.FREE -> NULL,
wenzelm@38158
   100
        Markup.TVAR -> NULL,
wenzelm@38158
   101
        Markup.SKOLEM -> NULL,
wenzelm@38158
   102
        Markup.BOUND -> NULL,
wenzelm@38158
   103
        Markup.VAR -> NULL,
wenzelm@38158
   104
        Markup.NUM -> DIGIT,
wenzelm@38158
   105
        Markup.FLOAT -> DIGIT,
wenzelm@38158
   106
        Markup.XNUM -> DIGIT,
wenzelm@38158
   107
        Markup.XSTR -> LITERAL4,
wenzelm@38158
   108
        Markup.LITERAL -> OPERATOR,
wenzelm@38158
   109
        Markup.INNER_COMMENT -> COMMENT1,
wenzelm@38158
   110
        Markup.SORT -> NULL,
wenzelm@38158
   111
        Markup.TYP -> NULL,
wenzelm@38158
   112
        Markup.TERM -> NULL,
wenzelm@38158
   113
        Markup.PROP -> NULL,
wenzelm@38158
   114
        Markup.ATTRIBUTE -> NULL,
wenzelm@38158
   115
        Markup.METHOD -> NULL,
wenzelm@38158
   116
        // ML syntax
wenzelm@38158
   117
        Markup.ML_KEYWORD -> KEYWORD1,
wenzelm@38158
   118
        Markup.ML_DELIMITER -> OPERATOR,
wenzelm@38158
   119
        Markup.ML_IDENT -> NULL,
wenzelm@38158
   120
        Markup.ML_TVAR -> NULL,
wenzelm@38158
   121
        Markup.ML_NUMERAL -> DIGIT,
wenzelm@38158
   122
        Markup.ML_CHAR -> LITERAL1,
wenzelm@38158
   123
        Markup.ML_STRING -> LITERAL1,
wenzelm@38158
   124
        Markup.ML_COMMENT -> COMMENT1,
wenzelm@38158
   125
        Markup.ML_MALFORMED -> INVALID,
wenzelm@38158
   126
        // embedded source text
wenzelm@38158
   127
        Markup.ML_SOURCE -> COMMENT3,
wenzelm@38158
   128
        Markup.DOC_SOURCE -> COMMENT3,
wenzelm@38158
   129
        Markup.ANTIQ -> COMMENT4,
wenzelm@38158
   130
        Markup.ML_ANTIQ -> COMMENT4,
wenzelm@38158
   131
        Markup.DOC_ANTIQ -> COMMENT4,
wenzelm@38158
   132
        // outer syntax
wenzelm@38158
   133
        Markup.KEYWORD -> KEYWORD2,
wenzelm@38158
   134
        Markup.OPERATOR -> OPERATOR,
wenzelm@38158
   135
        Markup.COMMAND -> KEYWORD1,
wenzelm@38158
   136
        Markup.IDENT -> NULL,
wenzelm@38158
   137
        Markup.VERBATIM -> COMMENT3,
wenzelm@38158
   138
        Markup.COMMENT -> COMMENT1,
wenzelm@38158
   139
        Markup.CONTROL -> COMMENT3,
wenzelm@38158
   140
        Markup.MALFORMED -> INVALID,
wenzelm@38158
   141
        Markup.STRING -> LITERAL3,
wenzelm@38158
   142
        Markup.ALTSTRING -> LITERAL1
wenzelm@38158
   143
      ).withDefaultValue(NULL)
wenzelm@38158
   144
    }
wenzelm@38158
   145
  }
wenzelm@38158
   146
wenzelm@38158
   147
wenzelm@34784
   148
  /* document model of buffer */
wenzelm@34784
   149
wenzelm@34784
   150
  private val key = "isabelle.document_model"
wenzelm@34784
   151
wenzelm@38222
   152
  def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
wenzelm@34716
   153
  {
wenzelm@38223
   154
    Swing_Thread.require()
wenzelm@38222
   155
    val model = new Document_Model(session, buffer, thy_name)
wenzelm@34784
   156
    buffer.setProperty(key, model)
wenzelm@34784
   157
    model.activate()
wenzelm@34784
   158
    model
wenzelm@34784
   159
  }
wenzelm@34784
   160
wenzelm@34788
   161
  def apply(buffer: Buffer): Option[Document_Model] =
wenzelm@34784
   162
  {
wenzelm@38223
   163
    Swing_Thread.require()
wenzelm@34784
   164
    buffer.getProperty(key) match {
wenzelm@34784
   165
      case model: Document_Model => Some(model)
wenzelm@34784
   166
      case _ => None
wenzelm@34784
   167
    }
wenzelm@34784
   168
  }
wenzelm@34784
   169
wenzelm@34784
   170
  def exit(buffer: Buffer)
wenzelm@34784
   171
  {
wenzelm@38223
   172
    Swing_Thread.require()
wenzelm@34788
   173
    apply(buffer) match {
wenzelm@34784
   174
      case None => error("No document model for buffer: " + buffer)
wenzelm@34784
   175
      case Some(model) =>
wenzelm@34784
   176
        model.deactivate()
wenzelm@34784
   177
        buffer.unsetProperty(key)
immler@34653
   178
    }
wenzelm@34318
   179
  }
wenzelm@34318
   180
}
wenzelm@34318
   181
wenzelm@38151
   182
wenzelm@38222
   183
class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
wenzelm@34588
   184
{
wenzelm@37555
   185
  /* visible line end */
wenzelm@37555
   186
wenzelm@37555
   187
  // simplify slightly odd result of TextArea.getLineEndOffset
wenzelm@37555
   188
  // NB: jEdit already normalizes \r\n and \r to \n
wenzelm@37555
   189
  def visible_line_end(start: Int, end: Int): Int =
wenzelm@37555
   190
  {
wenzelm@37555
   191
    val end1 = end - 1
wenzelm@37555
   192
    if (start <= end1 && end1 < buffer.getLength &&
wenzelm@37555
   193
        buffer.getSegment(end1, 1).charAt(0) == '\n') end1
wenzelm@37555
   194
    else end
wenzelm@37555
   195
  }
wenzelm@37555
   196
wenzelm@37555
   197
wenzelm@38224
   198
  /* pending text edits */
wenzelm@38222
   199
wenzelm@38224
   200
  object pending_edits  // owned by Swing thread
wenzelm@38224
   201
  {
wenzelm@38425
   202
    private val pending = new mutable.ListBuffer[Text.Edit]
wenzelm@38425
   203
    def snapshot(): List[Text.Edit] = pending.toList
wenzelm@38224
   204
wenzelm@38224
   205
    private val delay_flush = Swing_Thread.delay_last(session.input_delay) {
wenzelm@38417
   206
      if (!pending.isEmpty) session.edit_version(List((thy_name, flush())))
wenzelm@38224
   207
    }
wenzelm@38152
   208
wenzelm@38425
   209
    def flush(): List[Text.Edit] =
wenzelm@38224
   210
    {
wenzelm@38224
   211
      Swing_Thread.require()
wenzelm@38224
   212
      val edits = snapshot()
wenzelm@38224
   213
      pending.clear
wenzelm@38224
   214
      edits
wenzelm@38224
   215
    }
wenzelm@38224
   216
wenzelm@38425
   217
    def +=(edit: Text.Edit)
wenzelm@38224
   218
    {
wenzelm@38224
   219
      Swing_Thread.require()
wenzelm@38224
   220
      pending += edit
wenzelm@38224
   221
      delay_flush()
wenzelm@38222
   222
    }
wenzelm@38222
   223
  }
wenzelm@38152
   224
wenzelm@38152
   225
wenzelm@38152
   226
  /* snapshot */
wenzelm@34731
   227
wenzelm@38417
   228
  def snapshot(): Document.Snapshot =
wenzelm@38417
   229
  {
wenzelm@38223
   230
    Swing_Thread.require()
wenzelm@38359
   231
    session.snapshot(thy_name, pending_edits.snapshot())
wenzelm@38223
   232
  }
wenzelm@34828
   233
wenzelm@34828
   234
wenzelm@34828
   235
  /* buffer listener */
wenzelm@34828
   236
wenzelm@34828
   237
  private val buffer_listener: BufferListener = new BufferAdapter
wenzelm@34828
   238
  {
wenzelm@34828
   239
    override def contentInserted(buffer: JEditBuffer,
wenzelm@34828
   240
      start_line: Int, offset: Int, num_lines: Int, length: Int)
wenzelm@34828
   241
    {
wenzelm@38425
   242
      pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
wenzelm@34828
   243
    }
wenzelm@34828
   244
wenzelm@34828
   245
    override def preContentRemoved(buffer: JEditBuffer,
wenzelm@34828
   246
      start_line: Int, start: Int, num_lines: Int, removed_length: Int)
wenzelm@34828
   247
    {
wenzelm@38425
   248
      pending_edits += Text.Edit.remove(start, buffer.getText(start, removed_length))
wenzelm@34828
   249
    }
wenzelm@34828
   250
  }
wenzelm@34828
   251
wenzelm@34828
   252
wenzelm@38158
   253
  /* semantic token marker */
wenzelm@38158
   254
wenzelm@38158
   255
  private val token_marker = new TokenMarker
wenzelm@38158
   256
  {
wenzelm@38158
   257
    override def markTokens(prev: TokenMarker.LineContext,
wenzelm@38158
   258
        handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
wenzelm@38158
   259
    {
wenzelm@38158
   260
      val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext]
wenzelm@38158
   261
      val line = if (prev == null) 0 else previous.line + 1
wenzelm@38158
   262
      val context = new Document_Model.Token_Markup.LineContext(line, previous)
wenzelm@38158
   263
      val start = buffer.getLineStartOffset(line)
wenzelm@38158
   264
      val stop = start + line_segment.count
wenzelm@38158
   265
wenzelm@38225
   266
      // FIXME proper synchronization / thread context (!??)
wenzelm@38223
   267
      val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
wenzelm@38158
   268
wenzelm@38158
   269
      /* FIXME
wenzelm@38158
   270
      for (text_area <- Isabelle.jedit_text_areas(buffer)
wenzelm@38158
   271
            if Document_View(text_area).isDefined)
wenzelm@38158
   272
        Document_View(text_area).get.set_styles()
wenzelm@38158
   273
      */
wenzelm@38158
   274
wenzelm@38158
   275
      def handle_token(style: Byte, offset: Int, length: Int) =
wenzelm@38158
   276
        handler.handleToken(line_segment, style, offset, length, context)
immler@34680
   277
wenzelm@38158
   278
      var next_x = start
wenzelm@38158
   279
      for {
wenzelm@38158
   280
        (command, command_start) <-
wenzelm@38158
   281
          snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
wenzelm@38356
   282
        markup <- snapshot.state(command).highlight.flatten
wenzelm@38158
   283
        val abs_start = snapshot.convert(command_start + markup.start)
wenzelm@38158
   284
        val abs_stop = snapshot.convert(command_start + markup.stop)
wenzelm@38158
   285
        if (abs_stop > start)
wenzelm@38158
   286
        if (abs_start < stop)
wenzelm@38158
   287
        val token_start = (abs_start - start) max 0
wenzelm@38158
   288
        val token_length =
wenzelm@38158
   289
          (abs_stop - abs_start) -
wenzelm@38158
   290
          ((start - abs_start) max 0) -
wenzelm@38158
   291
          ((abs_stop - stop) max 0)
wenzelm@38158
   292
      }
wenzelm@38158
   293
      {
wenzelm@38158
   294
        val token_type =
wenzelm@38158
   295
          markup.info match {
wenzelm@38158
   296
            case Command.HighlightInfo(Markup.COMMAND, Some(kind)) =>
wenzelm@38158
   297
              Document_Model.Token_Markup.command_style(kind)
wenzelm@38158
   298
            case Command.HighlightInfo(kind, _) =>
wenzelm@38158
   299
              Document_Model.Token_Markup.token_style(kind)
wenzelm@38158
   300
            case _ => Token.NULL
wenzelm@38158
   301
          }
wenzelm@38158
   302
        if (start + token_start > next_x)
wenzelm@38158
   303
          handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
wenzelm@38158
   304
        handle_token(token_type, token_start, token_length)
wenzelm@38158
   305
        next_x = start + token_start + token_length
wenzelm@38158
   306
      }
wenzelm@38158
   307
      if (next_x < stop)
wenzelm@38158
   308
        handle_token(Token.COMMENT1, next_x - start, stop - next_x)
wenzelm@38158
   309
wenzelm@38158
   310
      handle_token(Token.END, line_segment.count, 0)
wenzelm@38158
   311
      handler.setLineContext(context)
wenzelm@38158
   312
      context
wenzelm@38158
   313
    }
wenzelm@38158
   314
  }
wenzelm@38158
   315
wenzelm@38158
   316
wenzelm@38158
   317
  /* activation */
wenzelm@37557
   318
wenzelm@34784
   319
  def activate()
wenzelm@34784
   320
  {
wenzelm@37557
   321
    buffer.setTokenMarker(token_marker)
wenzelm@34784
   322
    buffer.addBufferListener(buffer_listener)
wenzelm@34784
   323
    buffer.propertiesChanged()
wenzelm@38425
   324
    pending_edits += Text.Edit.insert(0, buffer.getText(0, buffer.getLength))
immler@34680
   325
  }
immler@34680
   326
wenzelm@37557
   327
  def refresh()
wenzelm@37557
   328
  {
wenzelm@37557
   329
    buffer.setTokenMarker(token_marker)
wenzelm@37557
   330
  }
wenzelm@37557
   331
wenzelm@34784
   332
  def deactivate()
immler@34680
   333
  {
wenzelm@34784
   334
    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
wenzelm@34784
   335
    buffer.removeBufferListener(buffer_listener)
immler@34680
   336
  }
wenzelm@34447
   337
}