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