src/Tools/jEdit/src/jedit/isabelle_token_marker.scala
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34777 91d6089cef88
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Tue Dec 08 16:30:20 2009 +0100
     1.3 @@ -0,0 +1,153 @@
     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.proofdocument.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 Isabelle_Token_Marker
    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 Isabelle_Token_Marker(buffer: JEditBuffer, prover: Prover) extends TokenMarker
   1.107 +{
   1.108 +  override def markTokens(prev: TokenMarker.LineContext,
   1.109 +      handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
   1.110 +  {
   1.111 +    val previous = prev.asInstanceOf[Isabelle_Token_Marker.LineContext]
   1.112 +    val line = if (prev == null) 0 else previous.line + 1
   1.113 +    val context = new Isabelle_Token_Marker.LineContext(line, previous)
   1.114 +    val start = buffer.getLineStartOffset(line)
   1.115 +    val stop = start + line_segment.count
   1.116 +
   1.117 +    val theory_view = Isabelle.prover_setup(buffer).get.theory_view
   1.118 +    val document = theory_view.current_document()
   1.119 +    def to: Int => Int = theory_view.to_current(document, _)
   1.120 +    def from: Int => Int = theory_view.from_current(document, _)
   1.121 +
   1.122 +    var next_x = start
   1.123 +    var cmd = document.command_at(from(start))
   1.124 +    while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
   1.125 +      val command = cmd.get
   1.126 +      for {
   1.127 +        markup <- command.highlight(document).flatten
   1.128 +        command_start = command.start(document)
   1.129 +        abs_start = to(command_start + markup.start)
   1.130 +        abs_stop = to(command_start + markup.stop)
   1.131 +        if (abs_stop > start)
   1.132 +        if (abs_start < stop)
   1.133 +        byte = Isabelle_Token_Marker.choose_byte(markup.info.toString)
   1.134 +        token_start = (abs_start - start) max 0
   1.135 +        token_length =
   1.136 +          (abs_stop - abs_start) -
   1.137 +          ((start - abs_start) max 0) -
   1.138 +          ((abs_stop - stop) max 0)
   1.139 +      } {
   1.140 +        if (start + token_start > next_x)
   1.141 +          handler.handleToken(line_segment, 1,
   1.142 +            next_x - start, start + token_start - next_x, context)
   1.143 +        handler.handleToken(line_segment, byte,
   1.144 +          token_start, token_length, context)
   1.145 +        next_x = start + token_start + token_length
   1.146 +      }
   1.147 +      cmd = document.commands.next(command)
   1.148 +    }
   1.149 +    if (next_x < stop)
   1.150 +      handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
   1.151 +
   1.152 +    handler.handleToken(line_segment, JToken.END, line_segment.count, 0, context)
   1.153 +    handler.setLineContext(context)
   1.154 +    return context
   1.155 +  }
   1.156 +}