src/Tools/jEdit/src/jedit/document_model.scala

more explicit model of pending text edits;

/*  Title:      Tools/jEdit/src/jedit/document_model.scala
    Author:     Fabian Immler, TU Munich
    Author:     Makarius

Document model connected to jEdit buffer -- single node in theory graph.
*/

package isabelle.jedit


import isabelle._

import scala.actors.Actor, Actor._
import scala.collection.mutable

import org.gjt.sp.jedit.Buffer
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
import org.gjt.sp.jedit.syntax.{SyntaxStyle, Token, TokenMarker, TokenHandler, ParserRuleSet}
import org.gjt.sp.jedit.textarea.TextArea

import java.awt.font.TextAttribute
import javax.swing.text.Segment;


object Document_Model
{
  object Token_Markup
  {
    /* extended token styles */

    private val plain_range: Int = Token.ID_COUNT
    private val full_range: Int = 3 * plain_range
    private def check_range(i: Int) { require(0 <= i && i < plain_range) }

    def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
    def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }

    private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
    {
      import scala.collection.JavaConversions._
      val script_font =
        style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
      new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font)
    }

    def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
    {
      val new_styles = new Array[SyntaxStyle](full_range)
      for (i <- 0 until plain_range) {
        val style = styles(i)
        new_styles(i) = style
        new_styles(subscript(i.toByte)) = script_style(style, -1)
        new_styles(superscript(i.toByte)) = script_style(style, 1)
      }
      new_styles
    }


    /* line context */

    private val rule_set = new ParserRuleSet("isabelle", "MAIN")
    class LineContext(val line: Int, prev: LineContext)
      extends TokenMarker.LineContext(rule_set, prev)


    /* mapping to jEdit token types */
    // TODO: as properties or CSS style sheet

    val command_style: Map[String, Byte] =
    {
      import Token._
      Map[String, Byte](
        Keyword.THY_END -> KEYWORD2,
        Keyword.THY_SCRIPT -> LABEL,
        Keyword.PRF_SCRIPT -> LABEL,
        Keyword.PRF_ASM -> KEYWORD3,
        Keyword.PRF_ASM_GOAL -> KEYWORD3
      ).withDefaultValue(KEYWORD1)
    }

    val token_style: Map[String, Byte] =
    {
      import Token._
      Map[String, Byte](
        // logical entities
        Markup.TCLASS -> NULL,
        Markup.TYCON -> NULL,
        Markup.FIXED_DECL -> FUNCTION,
        Markup.FIXED -> NULL,
        Markup.CONST_DECL -> FUNCTION,
        Markup.CONST -> NULL,
        Markup.FACT_DECL -> FUNCTION,
        Markup.FACT -> NULL,
        Markup.DYNAMIC_FACT -> LABEL,
        Markup.LOCAL_FACT_DECL -> FUNCTION,
        Markup.LOCAL_FACT -> NULL,
        // inner syntax
        Markup.TFREE -> NULL,
        Markup.FREE -> NULL,
        Markup.TVAR -> NULL,
        Markup.SKOLEM -> NULL,
        Markup.BOUND -> NULL,
        Markup.VAR -> NULL,
        Markup.NUM -> DIGIT,
        Markup.FLOAT -> DIGIT,
        Markup.XNUM -> DIGIT,
        Markup.XSTR -> LITERAL4,
        Markup.LITERAL -> OPERATOR,
        Markup.INNER_COMMENT -> COMMENT1,
        Markup.SORT -> NULL,
        Markup.TYP -> NULL,
        Markup.TERM -> NULL,
        Markup.PROP -> NULL,
        Markup.ATTRIBUTE -> NULL,
        Markup.METHOD -> NULL,
        // ML syntax
        Markup.ML_KEYWORD -> KEYWORD1,
        Markup.ML_DELIMITER -> OPERATOR,
        Markup.ML_IDENT -> NULL,
        Markup.ML_TVAR -> NULL,
        Markup.ML_NUMERAL -> DIGIT,
        Markup.ML_CHAR -> LITERAL1,
        Markup.ML_STRING -> LITERAL1,
        Markup.ML_COMMENT -> COMMENT1,
        Markup.ML_MALFORMED -> INVALID,
        // embedded source text
        Markup.ML_SOURCE -> COMMENT3,
        Markup.DOC_SOURCE -> COMMENT3,
        Markup.ANTIQ -> COMMENT4,
        Markup.ML_ANTIQ -> COMMENT4,
        Markup.DOC_ANTIQ -> COMMENT4,
        // outer syntax
        Markup.KEYWORD -> KEYWORD2,
        Markup.OPERATOR -> OPERATOR,
        Markup.COMMAND -> KEYWORD1,
        Markup.IDENT -> NULL,
        Markup.VERBATIM -> COMMENT3,
        Markup.COMMENT -> COMMENT1,
        Markup.CONTROL -> COMMENT3,
        Markup.MALFORMED -> INVALID,
        Markup.STRING -> LITERAL3,
        Markup.ALTSTRING -> LITERAL1
      ).withDefaultValue(NULL)
    }
  }


  /* document model of buffer */

  private val key = "isabelle.document_model"

  def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
  {
    Swing_Thread.require()
    val model = new Document_Model(session, buffer, thy_name)
    buffer.setProperty(key, model)
    model.activate()
    model
  }

  def apply(buffer: Buffer): Option[Document_Model] =
  {
    Swing_Thread.require()
    buffer.getProperty(key) match {
      case model: Document_Model => Some(model)
      case _ => None
    }
  }

  def exit(buffer: Buffer)
  {
    Swing_Thread.require()
    apply(buffer) match {
      case None => error("No document model for buffer: " + buffer)
      case Some(model) =>
        model.deactivate()
        buffer.unsetProperty(key)
    }
  }
}


class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
{
  /* visible line end */

  // simplify slightly odd result of TextArea.getLineEndOffset
  // NB: jEdit already normalizes \r\n and \r to \n
  def visible_line_end(start: Int, end: Int): Int =
  {
    val end1 = end - 1
    if (start <= end1 && end1 < buffer.getLength &&
        buffer.getSegment(end1, 1).charAt(0) == '\n') end1
    else end
  }


  /* pending text edits */

  object pending_edits  // owned by Swing thread
  {
    private val pending = new mutable.ListBuffer[Text_Edit]
    def snapshot(): List[Text_Edit] = pending.toList

    private val delay_flush = Swing_Thread.delay_last(session.input_delay) {
      if (!pending.isEmpty) session.edit_document(List((thy_name, flush())))
    }

    def flush(): List[Text_Edit] =
    {
      Swing_Thread.require()
      val edits = snapshot()
      pending.clear
      edits
    }

    def +=(edit: Text_Edit)
    {
      Swing_Thread.require()
      pending += edit
      delay_flush()
    }
  }


  /* snapshot */

  def snapshot(): Change.Snapshot = {
    Swing_Thread.require()
    session.current_change().snapshot(thy_name, pending_edits.snapshot())
  }


  /* buffer listener */

  private val buffer_listener: BufferListener = new BufferAdapter
  {
    override def contentInserted(buffer: JEditBuffer,
      start_line: Int, offset: Int, num_lines: Int, length: Int)
    {
      pending_edits += new Text_Edit(true, offset, buffer.getText(offset, length))
    }

    override def preContentRemoved(buffer: JEditBuffer,
      start_line: Int, start: Int, num_lines: Int, removed_length: Int)
    {
      pending_edits += new Text_Edit(false, start, buffer.getText(start, removed_length))
    }
  }


  /* semantic token marker */

  private val token_marker = new TokenMarker
  {
    override def markTokens(prev: TokenMarker.LineContext,
        handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
    {
      val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext]
      val line = if (prev == null) 0 else previous.line + 1
      val context = new Document_Model.Token_Markup.LineContext(line, previous)
      val start = buffer.getLineStartOffset(line)
      val stop = start + line_segment.count

      val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }

      /* FIXME
      for (text_area <- Isabelle.jedit_text_areas(buffer)
            if Document_View(text_area).isDefined)
        Document_View(text_area).get.set_styles()
      */

      def handle_token(style: Byte, offset: Int, length: Int) =
        handler.handleToken(line_segment, style, offset, length, context)

      var next_x = start
      for {
        (command, command_start) <-
          snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
        markup <- snapshot.document.current_state(command).highlight.flatten
        val abs_start = snapshot.convert(command_start + markup.start)
        val abs_stop = snapshot.convert(command_start + markup.stop)
        if (abs_stop > start)
        if (abs_start < stop)
        val token_start = (abs_start - start) max 0
        val token_length =
          (abs_stop - abs_start) -
          ((start - abs_start) max 0) -
          ((abs_stop - stop) max 0)
      }
      {
        val token_type =
          markup.info match {
            case Command.HighlightInfo(Markup.COMMAND, Some(kind)) =>
              Document_Model.Token_Markup.command_style(kind)
            case Command.HighlightInfo(kind, _) =>
              Document_Model.Token_Markup.token_style(kind)
            case _ => Token.NULL
          }
        if (start + token_start > next_x)
          handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
        handle_token(token_type, token_start, token_length)
        next_x = start + token_start + token_length
      }
      if (next_x < stop)
        handle_token(Token.COMMENT1, next_x - start, stop - next_x)

      handle_token(Token.END, line_segment.count, 0)
      handler.setLineContext(context)
      context
    }
  }


  /* activation */

  def activate()
  {
    buffer.setTokenMarker(token_marker)
    buffer.addBufferListener(buffer_listener)
    buffer.propertiesChanged()
    pending_edits += new Text_Edit(true, 0, buffer.getText(0, buffer.getLength))
  }

  def refresh()
  {
    buffer.setTokenMarker(token_marker)
  }

  def deactivate()
  {
    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
    buffer.removeBufferListener(buffer_listener)
  }
}