src/Tools/jEdit/src/jedit/isabelle_token_marker.scala

disable set_styles for now -- there are still some race conditions of PropertiesChanged vs. TextArea painting (NB: without it Isabelle_Token_Marker will crash if sub/superscript is actually used);

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

Include isabelle's command- and keyword-declarations live in jEdits
syntax-highlighting.
*/

package isabelle.jedit


import isabelle._

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

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


object Isabelle_Token_Marker
{
  /* 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")
  private 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

  private 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)
  }

  private 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)
  }
}


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

    val document = model.recent_document()
    def to: Int => Int = model.to_current(document, _)
    def from: Int => Int = model.from_current(document, _)

    /* FIXME
    for (text_area <- Isabelle.jedit_text_areas(model.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) <- document.command_range(from(start), from(stop))
      markup <- document.current_state(command).highlight.flatten
      val abs_start = to(command_start + markup.start)
      val abs_stop = to(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)) =>
            Isabelle_Token_Marker.command_style(kind)
          case Command.HighlightInfo(kind, _) =>
            Isabelle_Token_Marker.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
  }
}