src/Tools/jEdit/src/jedit/document_model.scala
author wenzelm
Sun Aug 15 14:18:52 2010 +0200 (2010-08-15)
changeset 38417 b8922ae21111
parent 38359 96b22dfeb56a
child 38425 e467db701d78
permissions -rw-r--r--
renamed class Document to Document.Version etc.;
renamed Change.prev to Change.previous, and Change.document to Change.current;
tuned;
     1 /*  Title:      Tools/jEdit/src/jedit/document_model.scala
     2     Author:     Fabian Immler, TU Munich
     3     Author:     Makarius
     4 
     5 Document model connected to jEdit buffer -- single node in theory graph.
     6 */
     7 
     8 package isabelle.jedit
     9 
    10 
    11 import isabelle._
    12 
    13 import scala.actors.Actor, Actor._
    14 import scala.collection.mutable
    15 
    16 import org.gjt.sp.jedit.Buffer
    17 import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
    18 import org.gjt.sp.jedit.syntax.{SyntaxStyle, Token, TokenMarker, TokenHandler, ParserRuleSet}
    19 import org.gjt.sp.jedit.textarea.TextArea
    20 
    21 import java.awt.font.TextAttribute
    22 import javax.swing.text.Segment;
    23 
    24 
    25 object Document_Model
    26 {
    27   object Token_Markup
    28   {
    29     /* extended token styles */
    30 
    31     private val plain_range: Int = Token.ID_COUNT
    32     private val full_range: Int = 3 * plain_range
    33     private def check_range(i: Int) { require(0 <= i && i < plain_range) }
    34 
    35     def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
    36     def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
    37 
    38     private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
    39     {
    40       import scala.collection.JavaConversions._
    41       val script_font =
    42         style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
    43       new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font)
    44     }
    45 
    46     def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
    47     {
    48       val new_styles = new Array[SyntaxStyle](full_range)
    49       for (i <- 0 until plain_range) {
    50         val style = styles(i)
    51         new_styles(i) = style
    52         new_styles(subscript(i.toByte)) = script_style(style, -1)
    53         new_styles(superscript(i.toByte)) = script_style(style, 1)
    54       }
    55       new_styles
    56     }
    57 
    58 
    59     /* line context */
    60 
    61     private val rule_set = new ParserRuleSet("isabelle", "MAIN")
    62     class LineContext(val line: Int, prev: LineContext)
    63       extends TokenMarker.LineContext(rule_set, prev)
    64 
    65 
    66     /* mapping to jEdit token types */
    67     // TODO: as properties or CSS style sheet
    68 
    69     val command_style: Map[String, Byte] =
    70     {
    71       import Token._
    72       Map[String, Byte](
    73         Keyword.THY_END -> KEYWORD2,
    74         Keyword.THY_SCRIPT -> LABEL,
    75         Keyword.PRF_SCRIPT -> LABEL,
    76         Keyword.PRF_ASM -> KEYWORD3,
    77         Keyword.PRF_ASM_GOAL -> KEYWORD3
    78       ).withDefaultValue(KEYWORD1)
    79     }
    80 
    81     val token_style: Map[String, Byte] =
    82     {
    83       import Token._
    84       Map[String, Byte](
    85         // logical entities
    86         Markup.TCLASS -> NULL,
    87         Markup.TYCON -> NULL,
    88         Markup.FIXED_DECL -> FUNCTION,
    89         Markup.FIXED -> NULL,
    90         Markup.CONST_DECL -> FUNCTION,
    91         Markup.CONST -> NULL,
    92         Markup.FACT_DECL -> FUNCTION,
    93         Markup.FACT -> NULL,
    94         Markup.DYNAMIC_FACT -> LABEL,
    95         Markup.LOCAL_FACT_DECL -> FUNCTION,
    96         Markup.LOCAL_FACT -> NULL,
    97         // inner syntax
    98         Markup.TFREE -> NULL,
    99         Markup.FREE -> NULL,
   100         Markup.TVAR -> NULL,
   101         Markup.SKOLEM -> NULL,
   102         Markup.BOUND -> NULL,
   103         Markup.VAR -> NULL,
   104         Markup.NUM -> DIGIT,
   105         Markup.FLOAT -> DIGIT,
   106         Markup.XNUM -> DIGIT,
   107         Markup.XSTR -> LITERAL4,
   108         Markup.LITERAL -> OPERATOR,
   109         Markup.INNER_COMMENT -> COMMENT1,
   110         Markup.SORT -> NULL,
   111         Markup.TYP -> NULL,
   112         Markup.TERM -> NULL,
   113         Markup.PROP -> NULL,
   114         Markup.ATTRIBUTE -> NULL,
   115         Markup.METHOD -> NULL,
   116         // ML syntax
   117         Markup.ML_KEYWORD -> KEYWORD1,
   118         Markup.ML_DELIMITER -> OPERATOR,
   119         Markup.ML_IDENT -> NULL,
   120         Markup.ML_TVAR -> NULL,
   121         Markup.ML_NUMERAL -> DIGIT,
   122         Markup.ML_CHAR -> LITERAL1,
   123         Markup.ML_STRING -> LITERAL1,
   124         Markup.ML_COMMENT -> COMMENT1,
   125         Markup.ML_MALFORMED -> INVALID,
   126         // embedded source text
   127         Markup.ML_SOURCE -> COMMENT3,
   128         Markup.DOC_SOURCE -> COMMENT3,
   129         Markup.ANTIQ -> COMMENT4,
   130         Markup.ML_ANTIQ -> COMMENT4,
   131         Markup.DOC_ANTIQ -> COMMENT4,
   132         // outer syntax
   133         Markup.KEYWORD -> KEYWORD2,
   134         Markup.OPERATOR -> OPERATOR,
   135         Markup.COMMAND -> KEYWORD1,
   136         Markup.IDENT -> NULL,
   137         Markup.VERBATIM -> COMMENT3,
   138         Markup.COMMENT -> COMMENT1,
   139         Markup.CONTROL -> COMMENT3,
   140         Markup.MALFORMED -> INVALID,
   141         Markup.STRING -> LITERAL3,
   142         Markup.ALTSTRING -> LITERAL1
   143       ).withDefaultValue(NULL)
   144     }
   145   }
   146 
   147 
   148   /* document model of buffer */
   149 
   150   private val key = "isabelle.document_model"
   151 
   152   def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
   153   {
   154     Swing_Thread.require()
   155     val model = new Document_Model(session, buffer, thy_name)
   156     buffer.setProperty(key, model)
   157     model.activate()
   158     model
   159   }
   160 
   161   def apply(buffer: Buffer): Option[Document_Model] =
   162   {
   163     Swing_Thread.require()
   164     buffer.getProperty(key) match {
   165       case model: Document_Model => Some(model)
   166       case _ => None
   167     }
   168   }
   169 
   170   def exit(buffer: Buffer)
   171   {
   172     Swing_Thread.require()
   173     apply(buffer) match {
   174       case None => error("No document model for buffer: " + buffer)
   175       case Some(model) =>
   176         model.deactivate()
   177         buffer.unsetProperty(key)
   178     }
   179   }
   180 }
   181 
   182 
   183 class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
   184 {
   185   /* visible line end */
   186 
   187   // simplify slightly odd result of TextArea.getLineEndOffset
   188   // NB: jEdit already normalizes \r\n and \r to \n
   189   def visible_line_end(start: Int, end: Int): Int =
   190   {
   191     val end1 = end - 1
   192     if (start <= end1 && end1 < buffer.getLength &&
   193         buffer.getSegment(end1, 1).charAt(0) == '\n') end1
   194     else end
   195   }
   196 
   197 
   198   /* pending text edits */
   199 
   200   object pending_edits  // owned by Swing thread
   201   {
   202     private val pending = new mutable.ListBuffer[Text_Edit]
   203     def snapshot(): List[Text_Edit] = pending.toList
   204 
   205     private val delay_flush = Swing_Thread.delay_last(session.input_delay) {
   206       if (!pending.isEmpty) session.edit_version(List((thy_name, flush())))
   207     }
   208 
   209     def flush(): List[Text_Edit] =
   210     {
   211       Swing_Thread.require()
   212       val edits = snapshot()
   213       pending.clear
   214       edits
   215     }
   216 
   217     def +=(edit: Text_Edit)
   218     {
   219       Swing_Thread.require()
   220       pending += edit
   221       delay_flush()
   222     }
   223   }
   224 
   225 
   226   /* snapshot */
   227 
   228   def snapshot(): Document.Snapshot =
   229   {
   230     Swing_Thread.require()
   231     session.snapshot(thy_name, pending_edits.snapshot())
   232   }
   233 
   234 
   235   /* buffer listener */
   236 
   237   private val buffer_listener: BufferListener = new BufferAdapter
   238   {
   239     override def contentInserted(buffer: JEditBuffer,
   240       start_line: Int, offset: Int, num_lines: Int, length: Int)
   241     {
   242       pending_edits += new Text_Edit(true, offset, buffer.getText(offset, length))
   243     }
   244 
   245     override def preContentRemoved(buffer: JEditBuffer,
   246       start_line: Int, start: Int, num_lines: Int, removed_length: Int)
   247     {
   248       pending_edits += new Text_Edit(false, start, buffer.getText(start, removed_length))
   249     }
   250   }
   251 
   252 
   253   /* semantic token marker */
   254 
   255   private val token_marker = new TokenMarker
   256   {
   257     override def markTokens(prev: TokenMarker.LineContext,
   258         handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
   259     {
   260       val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext]
   261       val line = if (prev == null) 0 else previous.line + 1
   262       val context = new Document_Model.Token_Markup.LineContext(line, previous)
   263       val start = buffer.getLineStartOffset(line)
   264       val stop = start + line_segment.count
   265 
   266       // FIXME proper synchronization / thread context (!??)
   267       val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
   268 
   269       /* FIXME
   270       for (text_area <- Isabelle.jedit_text_areas(buffer)
   271             if Document_View(text_area).isDefined)
   272         Document_View(text_area).get.set_styles()
   273       */
   274 
   275       def handle_token(style: Byte, offset: Int, length: Int) =
   276         handler.handleToken(line_segment, style, offset, length, context)
   277 
   278       var next_x = start
   279       for {
   280         (command, command_start) <-
   281           snapshot.node.command_range(snapshot.revert(start), snapshot.revert(stop))
   282         markup <- snapshot.state(command).highlight.flatten
   283         val abs_start = snapshot.convert(command_start + markup.start)
   284         val abs_stop = snapshot.convert(command_start + markup.stop)
   285         if (abs_stop > start)
   286         if (abs_start < stop)
   287         val token_start = (abs_start - start) max 0
   288         val token_length =
   289           (abs_stop - abs_start) -
   290           ((start - abs_start) max 0) -
   291           ((abs_stop - stop) max 0)
   292       }
   293       {
   294         val token_type =
   295           markup.info match {
   296             case Command.HighlightInfo(Markup.COMMAND, Some(kind)) =>
   297               Document_Model.Token_Markup.command_style(kind)
   298             case Command.HighlightInfo(kind, _) =>
   299               Document_Model.Token_Markup.token_style(kind)
   300             case _ => Token.NULL
   301           }
   302         if (start + token_start > next_x)
   303           handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
   304         handle_token(token_type, token_start, token_length)
   305         next_x = start + token_start + token_length
   306       }
   307       if (next_x < stop)
   308         handle_token(Token.COMMENT1, next_x - start, stop - next_x)
   309 
   310       handle_token(Token.END, line_segment.count, 0)
   311       handler.setLineContext(context)
   312       context
   313     }
   314   }
   315 
   316 
   317   /* activation */
   318 
   319   def activate()
   320   {
   321     buffer.setTokenMarker(token_marker)
   322     buffer.addBufferListener(buffer_listener)
   323     buffer.propertiesChanged()
   324     pending_edits += new Text_Edit(true, 0, buffer.getText(0, buffer.getLength))
   325   }
   326 
   327   def refresh()
   328   {
   329     buffer.setTokenMarker(token_marker)
   330   }
   331 
   332   def deactivate()
   333   {
   334     buffer.setTokenMarker(buffer.getMode.getTokenMarker)
   335     buffer.removeBufferListener(buffer_listener)
   336   }
   337 }