src/Tools/jEdit/src/jedit/token_marker.scala
author wenzelm
Tue Dec 08 14:49:01 2009 +0100 (2009-12-08)
changeset 34759 bfea7839d9e1
parent 34728 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala@e3df9c8699ea
permissions -rw-r--r--
misc rearrangement of files;
immler@34467
     1
/*
immler@34467
     2
 * include isabelle's command- and keyword-declarations
immler@34467
     3
 * live in jEdits syntax-highlighting
immler@34517
     4
 *
immler@34467
     5
 * @author Fabian Immler, TU Munich
immler@34467
     6
 */
immler@34467
     7
immler@34467
     8
package isabelle.jedit
immler@34467
     9
wenzelm@34700
    10
wenzelm@34700
    11
import isabelle.prover.Prover
immler@34517
    12
import isabelle.Markup
immler@34467
    13
immler@34517
    14
import org.gjt.sp.jedit.buffer.JEditBuffer
wenzelm@34638
    15
import org.gjt.sp.jedit.syntax.{Token => JToken,
wenzelm@34638
    16
  TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet}
immler@34467
    17
immler@34517
    18
import java.awt.Color
immler@34517
    19
import java.awt.Font
immler@34517
    20
import javax.swing.text.Segment;
immler@34517
    21
wenzelm@34588
    22
wenzelm@34588
    23
object DynamicTokenMarker
wenzelm@34588
    24
{
wenzelm@34709
    25
  /* line context */
wenzelm@34709
    26
wenzelm@34727
    27
  private val rule_set = new ParserRuleSet("isabelle", "MAIN")
wenzelm@34709
    28
  private class LineContext(val line: Int, prev: LineContext)
wenzelm@34727
    29
    extends TokenMarker.LineContext(rule_set, prev)
wenzelm@34709
    30
wenzelm@34709
    31
wenzelm@34709
    32
  /* mapping to jEdit token types */
wenzelm@34638
    33
  // TODO: as properties or CSS style sheet
wenzelm@34709
    34
wenzelm@34638
    35
  private val choose_byte: Map[String, Byte] =
wenzelm@34638
    36
  {
wenzelm@34638
    37
    import JToken._
wenzelm@34639
    38
    Map[String, Byte](
immler@34549
    39
      // logical entities
wenzelm@34639
    40
      Markup.TCLASS -> LABEL,
wenzelm@34639
    41
      Markup.TYCON -> LABEL,
wenzelm@34639
    42
      Markup.FIXED_DECL -> LABEL,
wenzelm@34639
    43
      Markup.FIXED -> LABEL,
wenzelm@34639
    44
      Markup.CONST_DECL -> LABEL,
wenzelm@34639
    45
      Markup.CONST -> LABEL,
wenzelm@34639
    46
      Markup.FACT_DECL -> LABEL,
wenzelm@34639
    47
      Markup.FACT -> LABEL,
wenzelm@34639
    48
      Markup.DYNAMIC_FACT -> LABEL,
wenzelm@34639
    49
      Markup.LOCAL_FACT_DECL -> LABEL,
wenzelm@34639
    50
      Markup.LOCAL_FACT -> LABEL,
immler@34549
    51
      // inner syntax
wenzelm@34638
    52
      Markup.TFREE -> LITERAL2,
wenzelm@34638
    53
      Markup.FREE -> LITERAL2,
wenzelm@34638
    54
      Markup.TVAR -> LITERAL3,
wenzelm@34638
    55
      Markup.SKOLEM -> LITERAL3,
wenzelm@34638
    56
      Markup.BOUND -> LITERAL3,
wenzelm@34638
    57
      Markup.VAR -> LITERAL3,
wenzelm@34639
    58
      Markup.NUM -> DIGIT,
wenzelm@34639
    59
      Markup.FLOAT -> DIGIT,
wenzelm@34639
    60
      Markup.XNUM -> DIGIT,
wenzelm@34638
    61
      Markup.XSTR -> LITERAL4,
wenzelm@34638
    62
      Markup.LITERAL -> LITERAL4,
wenzelm@34639
    63
      Markup.INNER_COMMENT -> COMMENT1,
wenzelm@34638
    64
      Markup.SORT -> FUNCTION,
wenzelm@34638
    65
      Markup.TYP -> FUNCTION,
wenzelm@34638
    66
      Markup.TERM -> FUNCTION,
wenzelm@34638
    67
      Markup.PROP -> FUNCTION,
wenzelm@34638
    68
      Markup.ATTRIBUTE -> FUNCTION,
wenzelm@34638
    69
      Markup.METHOD -> FUNCTION,
immler@34549
    70
      // ML syntax
wenzelm@34638
    71
      Markup.ML_KEYWORD -> KEYWORD2,
wenzelm@34640
    72
      Markup.ML_IDENT -> NULL,
wenzelm@34638
    73
      Markup.ML_TVAR -> LITERAL3,
wenzelm@34639
    74
      Markup.ML_NUMERAL -> DIGIT,
wenzelm@34638
    75
      Markup.ML_CHAR -> LITERAL1,
wenzelm@34638
    76
      Markup.ML_STRING -> LITERAL1,
wenzelm@34638
    77
      Markup.ML_COMMENT -> COMMENT1,
wenzelm@34638
    78
      Markup.ML_MALFORMED -> INVALID,
immler@34549
    79
      // embedded source text
wenzelm@34638
    80
      Markup.ML_SOURCE -> COMMENT4,
wenzelm@34638
    81
      Markup.DOC_SOURCE -> COMMENT4,
wenzelm@34638
    82
      Markup.ANTIQ -> COMMENT4,
wenzelm@34638
    83
      Markup.ML_ANTIQ -> COMMENT4,
wenzelm@34638
    84
      Markup.DOC_ANTIQ -> COMMENT4,
immler@34549
    85
      // outer syntax
wenzelm@34640
    86
      Markup.IDENT -> NULL,
wenzelm@34639
    87
      Markup.COMMAND -> OPERATOR,
wenzelm@34639
    88
      Markup.KEYWORD -> KEYWORD4,
wenzelm@34639
    89
      Markup.VERBATIM -> COMMENT3,
wenzelm@34639
    90
      Markup.COMMENT -> COMMENT1,
wenzelm@34638
    91
      Markup.CONTROL -> COMMENT3,
wenzelm@34638
    92
      Markup.MALFORMED -> INVALID,
wenzelm@34639
    93
      Markup.STRING -> LITERAL3,
wenzelm@34638
    94
      Markup.ALTSTRING -> LITERAL1
wenzelm@34640
    95
    ).withDefaultValue(NULL)
immler@34517
    96
  }
immler@34467
    97
wenzelm@34638
    98
  def choose_color(kind: String, styles: Array[SyntaxStyle]): Color =
wenzelm@34638
    99
    styles(choose_byte(kind)).getForegroundColor
immler@34467
   100
}
immler@34517
   101
wenzelm@34700
   102
wenzelm@34700
   103
class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover)
wenzelm@34700
   104
  extends TokenMarker
wenzelm@34588
   105
{
immler@34517
   106
  override def markTokens(prev: TokenMarker.LineContext,
wenzelm@34638
   107
      handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
wenzelm@34638
   108
  {
wenzelm@34709
   109
    val previous = prev.asInstanceOf[DynamicTokenMarker.LineContext]
wenzelm@34582
   110
    val line = if (prev == null) 0 else previous.line + 1
wenzelm@34709
   111
    val context = new DynamicTokenMarker.LineContext(line, previous)
immler@34517
   112
    val start = buffer.getLineStartOffset(line)
immler@34517
   113
    val stop = start + line_segment.count
immler@34541
   114
wenzelm@34638
   115
    val theory_view = Isabelle.prover_setup(buffer).get.theory_view
immler@34650
   116
    val document = theory_view.current_document()
immler@34654
   117
    def to: Int => Int = theory_view.to_current(document, _)
immler@34654
   118
    def from: Int => Int = theory_view.from_current(document, _)
immler@34517
   119
immler@34522
   120
    var next_x = start
wenzelm@34712
   121
    var cmd = document.command_at(from(start))
wenzelm@34712
   122
    while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
wenzelm@34712
   123
      val command = cmd.get
immler@34596
   124
      for {
wenzelm@34717
   125
        markup <- command.highlight(document).flatten
wenzelm@34704
   126
        command_start = command.start(document)
wenzelm@34704
   127
        abs_start = to(command_start + markup.start)
wenzelm@34704
   128
        abs_stop = to(command_start + markup.stop)
immler@34687
   129
        if (abs_stop > start)
immler@34687
   130
        if (abs_start < stop)
immler@34596
   131
        byte = DynamicTokenMarker.choose_byte(markup.info.toString)
wenzelm@34709
   132
        token_start = (abs_start - start) max 0
wenzelm@34709
   133
        token_length =
wenzelm@34709
   134
          (abs_stop - abs_start) -
wenzelm@34709
   135
          ((start - abs_start) max 0) -
wenzelm@34709
   136
          ((abs_stop - stop) max 0)
immler@34596
   137
      } {
immler@34596
   138
        if (start + token_start > next_x)
wenzelm@34638
   139
          handler.handleToken(line_segment, 1,
wenzelm@34638
   140
            next_x - start, start + token_start - next_x, context)
wenzelm@34638
   141
        handler.handleToken(line_segment, byte,
wenzelm@34638
   142
          token_start, token_length, context)
immler@34596
   143
        next_x = start + token_start + token_length
immler@34596
   144
      }
wenzelm@34712
   145
      cmd = document.commands.next(command)
immler@34517
   146
    }
immler@34522
   147
    if (next_x < stop)
immler@34522
   148
      handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
immler@34517
   149
wenzelm@34638
   150
    handler.handleToken(line_segment, JToken.END, line_segment.count, 0, context)
immler@34517
   151
    handler.setLineContext(context)
immler@34517
   152
    return context
immler@34517
   153
  }
wenzelm@34700
   154
}