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