src/Tools/jEdit/src/jedit/token_marker.scala
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34761 0ad6d8372f9d
     1.1 --- a/src/Tools/jEdit/src/jedit/token_marker.scala	Tue Dec 08 14:49:01 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,154 +0,0 @@
     1.4 -/*
     1.5 - * include isabelle's command- and keyword-declarations
     1.6 - * live in jEdits syntax-highlighting
     1.7 - *
     1.8 - * @author Fabian Immler, TU Munich
     1.9 - */
    1.10 -
    1.11 -package isabelle.jedit
    1.12 -
    1.13 -
    1.14 -import isabelle.prover.Prover
    1.15 -import isabelle.Markup
    1.16 -
    1.17 -import org.gjt.sp.jedit.buffer.JEditBuffer
    1.18 -import org.gjt.sp.jedit.syntax.{Token => JToken,
    1.19 -  TokenMarker, TokenHandler, SyntaxStyle, ParserRuleSet}
    1.20 -
    1.21 -import java.awt.Color
    1.22 -import java.awt.Font
    1.23 -import javax.swing.text.Segment;
    1.24 -
    1.25 -
    1.26 -object DynamicTokenMarker
    1.27 -{
    1.28 -  /* line context */
    1.29 -
    1.30 -  private val rule_set = new ParserRuleSet("isabelle", "MAIN")
    1.31 -  private class LineContext(val line: Int, prev: LineContext)
    1.32 -    extends TokenMarker.LineContext(rule_set, prev)
    1.33 -
    1.34 -
    1.35 -  /* mapping to jEdit token types */
    1.36 -  // TODO: as properties or CSS style sheet
    1.37 -
    1.38 -  private val choose_byte: Map[String, Byte] =
    1.39 -  {
    1.40 -    import JToken._
    1.41 -    Map[String, Byte](
    1.42 -      // logical entities
    1.43 -      Markup.TCLASS -> LABEL,
    1.44 -      Markup.TYCON -> LABEL,
    1.45 -      Markup.FIXED_DECL -> LABEL,
    1.46 -      Markup.FIXED -> LABEL,
    1.47 -      Markup.CONST_DECL -> LABEL,
    1.48 -      Markup.CONST -> LABEL,
    1.49 -      Markup.FACT_DECL -> LABEL,
    1.50 -      Markup.FACT -> LABEL,
    1.51 -      Markup.DYNAMIC_FACT -> LABEL,
    1.52 -      Markup.LOCAL_FACT_DECL -> LABEL,
    1.53 -      Markup.LOCAL_FACT -> LABEL,
    1.54 -      // inner syntax
    1.55 -      Markup.TFREE -> LITERAL2,
    1.56 -      Markup.FREE -> LITERAL2,
    1.57 -      Markup.TVAR -> LITERAL3,
    1.58 -      Markup.SKOLEM -> LITERAL3,
    1.59 -      Markup.BOUND -> LITERAL3,
    1.60 -      Markup.VAR -> LITERAL3,
    1.61 -      Markup.NUM -> DIGIT,
    1.62 -      Markup.FLOAT -> DIGIT,
    1.63 -      Markup.XNUM -> DIGIT,
    1.64 -      Markup.XSTR -> LITERAL4,
    1.65 -      Markup.LITERAL -> LITERAL4,
    1.66 -      Markup.INNER_COMMENT -> COMMENT1,
    1.67 -      Markup.SORT -> FUNCTION,
    1.68 -      Markup.TYP -> FUNCTION,
    1.69 -      Markup.TERM -> FUNCTION,
    1.70 -      Markup.PROP -> FUNCTION,
    1.71 -      Markup.ATTRIBUTE -> FUNCTION,
    1.72 -      Markup.METHOD -> FUNCTION,
    1.73 -      // ML syntax
    1.74 -      Markup.ML_KEYWORD -> KEYWORD2,
    1.75 -      Markup.ML_IDENT -> NULL,
    1.76 -      Markup.ML_TVAR -> LITERAL3,
    1.77 -      Markup.ML_NUMERAL -> DIGIT,
    1.78 -      Markup.ML_CHAR -> LITERAL1,
    1.79 -      Markup.ML_STRING -> LITERAL1,
    1.80 -      Markup.ML_COMMENT -> COMMENT1,
    1.81 -      Markup.ML_MALFORMED -> INVALID,
    1.82 -      // embedded source text
    1.83 -      Markup.ML_SOURCE -> COMMENT4,
    1.84 -      Markup.DOC_SOURCE -> COMMENT4,
    1.85 -      Markup.ANTIQ -> COMMENT4,
    1.86 -      Markup.ML_ANTIQ -> COMMENT4,
    1.87 -      Markup.DOC_ANTIQ -> COMMENT4,
    1.88 -      // outer syntax
    1.89 -      Markup.IDENT -> NULL,
    1.90 -      Markup.COMMAND -> OPERATOR,
    1.91 -      Markup.KEYWORD -> KEYWORD4,
    1.92 -      Markup.VERBATIM -> COMMENT3,
    1.93 -      Markup.COMMENT -> COMMENT1,
    1.94 -      Markup.CONTROL -> COMMENT3,
    1.95 -      Markup.MALFORMED -> INVALID,
    1.96 -      Markup.STRING -> LITERAL3,
    1.97 -      Markup.ALTSTRING -> LITERAL1
    1.98 -    ).withDefaultValue(NULL)
    1.99 -  }
   1.100 -
   1.101 -  def choose_color(kind: String, styles: Array[SyntaxStyle]): Color =
   1.102 -    styles(choose_byte(kind)).getForegroundColor
   1.103 -}
   1.104 -
   1.105 -
   1.106 -class DynamicTokenMarker(buffer: JEditBuffer, prover: Prover)
   1.107 -  extends TokenMarker
   1.108 -{
   1.109 -  override def markTokens(prev: TokenMarker.LineContext,
   1.110 -      handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
   1.111 -  {
   1.112 -    val previous = prev.asInstanceOf[DynamicTokenMarker.LineContext]
   1.113 -    val line = if (prev == null) 0 else previous.line + 1
   1.114 -    val context = new DynamicTokenMarker.LineContext(line, previous)
   1.115 -    val start = buffer.getLineStartOffset(line)
   1.116 -    val stop = start + line_segment.count
   1.117 -
   1.118 -    val theory_view = Isabelle.prover_setup(buffer).get.theory_view
   1.119 -    val document = theory_view.current_document()
   1.120 -    def to: Int => Int = theory_view.to_current(document, _)
   1.121 -    def from: Int => Int = theory_view.from_current(document, _)
   1.122 -
   1.123 -    var next_x = start
   1.124 -    var cmd = document.command_at(from(start))
   1.125 -    while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
   1.126 -      val command = cmd.get
   1.127 -      for {
   1.128 -        markup <- command.highlight(document).flatten
   1.129 -        command_start = command.start(document)
   1.130 -        abs_start = to(command_start + markup.start)
   1.131 -        abs_stop = to(command_start + markup.stop)
   1.132 -        if (abs_stop > start)
   1.133 -        if (abs_start < stop)
   1.134 -        byte = DynamicTokenMarker.choose_byte(markup.info.toString)
   1.135 -        token_start = (abs_start - start) max 0
   1.136 -        token_length =
   1.137 -          (abs_stop - abs_start) -
   1.138 -          ((start - abs_start) max 0) -
   1.139 -          ((abs_stop - stop) max 0)
   1.140 -      } {
   1.141 -        if (start + token_start > next_x)
   1.142 -          handler.handleToken(line_segment, 1,
   1.143 -            next_x - start, start + token_start - next_x, context)
   1.144 -        handler.handleToken(line_segment, byte,
   1.145 -          token_start, token_length, context)
   1.146 -        next_x = start + token_start + token_length
   1.147 -      }
   1.148 -      cmd = document.commands.next(command)
   1.149 -    }
   1.150 -    if (next_x < stop)
   1.151 -      handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
   1.152 -
   1.153 -    handler.handleToken(line_segment, JToken.END, line_segment.count, 0, context)
   1.154 -    handler.setLineContext(context)
   1.155 -    return context
   1.156 -  }
   1.157 -}