more robust initialization of token marker and line context wrt. session startup;
authorwenzelm
Sun Aug 21 21:24:42 2011 +0200 (2011-08-21)
changeset 443582a2df4de1bbe
parent 44357 5f5649ac8235
child 44362 36598b3eb209
more robust initialization of token marker and line context wrt. session startup;
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Sun Aug 21 20:42:26 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sun Aug 21 21:24:42 2011 +0200
     1.3 @@ -139,13 +139,13 @@
     1.4    {
     1.5      buffer.addBufferListener(buffer_listener)
     1.6      pending_edits.init()
     1.7 -    buffer.propertiesChanged()
     1.8 +    Token_Markup.refresh_buffer(buffer)
     1.9    }
    1.10  
    1.11    private def deactivate()
    1.12    {
    1.13      pending_edits.flush()
    1.14      buffer.removeBufferListener(buffer_listener)
    1.15 -    buffer.propertiesChanged()
    1.16 +    Token_Markup.refresh_buffer(buffer)
    1.17    }
    1.18  }
     2.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sun Aug 21 20:42:26 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sun Aug 21 21:24:42 2011 +0200
     2.3 @@ -14,9 +14,10 @@
     2.4  import java.awt.geom.AffineTransform
     2.5  
     2.6  import org.gjt.sp.util.SyntaxUtilities
     2.7 -import org.gjt.sp.jedit.Mode
     2.8 +import org.gjt.sp.jedit.{jEdit, Mode}
     2.9  import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler,
    2.10    ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
    2.11 +import org.gjt.sp.jedit.buffer.JEditBuffer
    2.12  
    2.13  import javax.swing.text.Segment
    2.14  
    2.15 @@ -150,7 +151,7 @@
    2.16  
    2.17    private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN")
    2.18  
    2.19 -  private class Line_Context(val context: Scan.Context)
    2.20 +  private class Line_Context(val context: Option[Scan.Context])
    2.21      extends TokenMarker.LineContext(isabelle_rules, null)
    2.22    {
    2.23      override def hashCode: Int = context.hashCode
    2.24 @@ -166,17 +167,17 @@
    2.25      override def markTokens(context: TokenMarker.LineContext,
    2.26          handler: TokenHandler, line: Segment): TokenMarker.LineContext =
    2.27      {
    2.28 +      val line_ctxt =
    2.29 +        context match {
    2.30 +          case c: Line_Context => c.context
    2.31 +          case _ => Some(Scan.Finished)
    2.32 +        }
    2.33        val context1 =
    2.34 -        if (Isabelle.session.is_ready) {
    2.35 +        if (line_ctxt.isDefined && Isabelle.session.is_ready) {
    2.36            val syntax = Isabelle.session.current_syntax()
    2.37      
    2.38 -          val ctxt =
    2.39 -            context match {
    2.40 -              case c: Line_Context => c.context
    2.41 -              case _ => Scan.Finished
    2.42 -            }
    2.43 -          val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
    2.44 -          val context1 = new Line_Context(ctxt1)
    2.45 +          val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
    2.46 +          val context1 = new Line_Context(Some(ctxt1))
    2.47      
    2.48            val extended = extended_styles(line)
    2.49      
    2.50 @@ -202,7 +203,7 @@
    2.51            context1
    2.52          }
    2.53          else {
    2.54 -          val context1 = new Line_Context(Scan.Finished)
    2.55 +          val context1 = new Line_Context(None)
    2.56            handler.handleToken(line, JEditToken.NULL, 0, line.count, context1)
    2.57            handler.handleToken(line, JEditToken.END, line.count, 0, context1)
    2.58            context1
    2.59 @@ -216,12 +217,12 @@
    2.60  
    2.61    /* mode provider */
    2.62  
    2.63 +  private val isabelle_token_marker = new Token_Markup.Marker
    2.64 +
    2.65    class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
    2.66    {
    2.67      for (mode <- orig_provider.getModes) addMode(mode)
    2.68  
    2.69 -    val isabelle_token_marker = new Token_Markup.Marker
    2.70 -
    2.71      override def loadMode(mode: Mode, xmh: XModeHandler)
    2.72      {
    2.73        super.loadMode(mode, xmh)
    2.74 @@ -229,5 +230,12 @@
    2.75          mode.setTokenMarker(isabelle_token_marker)
    2.76      }
    2.77    }
    2.78 +
    2.79 +  def refresh_buffer(buffer: JEditBuffer)
    2.80 +  {
    2.81 +    buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
    2.82 +    buffer.setTokenMarker(isabelle_token_marker)
    2.83 +    buffer.propertiesChanged
    2.84 +  }
    2.85  }
    2.86