avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
authorwenzelm
Sat Jun 18 23:34:34 2011 +0200 (2011-06-18)
changeset 434525cf548485529
parent 43451 be760a642d38
child 43453 3c9696efe6b4
avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Jun 18 22:01:22 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sat Jun 18 23:34:34 2011 +0200
     1.3 @@ -129,30 +129,18 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* token marker */
     1.8 -
     1.9 -  private val token_marker = Token_Markup.token_marker(session, buffer)
    1.10 -
    1.11 -
    1.12    /* activation */
    1.13  
    1.14    def activate()
    1.15    {
    1.16 -    buffer.setTokenMarker(token_marker)
    1.17      buffer.addBufferListener(buffer_listener)
    1.18      buffer.propertiesChanged()
    1.19      pending_edits.init()
    1.20    }
    1.21  
    1.22 -  def refresh()
    1.23 -  {
    1.24 -    buffer.setTokenMarker(token_marker)
    1.25 -  }
    1.26 -
    1.27    def deactivate()
    1.28    {
    1.29      pending_edits.flush()
    1.30 -    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
    1.31      buffer.removeBufferListener(buffer_listener)
    1.32    }
    1.33  }
     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Jun 18 22:01:22 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Jun 18 23:34:34 2011 +0200
     2.3 @@ -19,7 +19,7 @@
     2.4    Buffer, EditPane, ServiceManager, View}
     2.5  import org.gjt.sp.jedit.buffer.JEditBuffer
     2.6  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
     2.7 -import org.gjt.sp.jedit.syntax.{Token => JEditToken}
     2.8 +import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
     2.9  import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
    2.10  import org.gjt.sp.jedit.gui.DockableWindowManager
    2.11  
    2.12 @@ -290,7 +290,7 @@
    2.13      Isabelle.swing_buffer_lock(buffer) {
    2.14        val opt_model =
    2.15          Document_Model(buffer) match {
    2.16 -          case Some(model) => model.refresh; Some(model)
    2.17 +          case Some(model) => Some(model)
    2.18            case None =>
    2.19              Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
    2.20                case Some((dir, thy_name)) =>
    2.21 @@ -408,8 +408,10 @@
    2.22      }
    2.23    }
    2.24  
    2.25 +
    2.26    override def start()
    2.27    {
    2.28 +    ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
    2.29      Isabelle.plugin = this
    2.30      Isabelle.setup_tooltips()
    2.31      Isabelle.system = new Isabelle_System
     3.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sat Jun 18 22:01:22 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sat Jun 18 23:34:34 2011 +0200
     3.3 @@ -9,8 +9,10 @@
     3.4  
     3.5  import isabelle._
     3.6  
     3.7 -import org.gjt.sp.jedit.Buffer
     3.8 -import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet}
     3.9 +import org.gjt.sp.jedit.Mode
    3.10 +import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler,
    3.11 +  ParserRuleSet, ModeProvider, XModeHandler}
    3.12 +
    3.13  import javax.swing.text.Segment
    3.14  
    3.15  
    3.16 @@ -78,46 +80,65 @@
    3.17        }
    3.18    }
    3.19  
    3.20 -  def token_marker(session: Session, buffer: Buffer): TokenMarker =
    3.21 -    new TokenMarker {
    3.22 -      override def markTokens(context: TokenMarker.LineContext,
    3.23 -          handler: TokenHandler, line: Segment): TokenMarker.LineContext =
    3.24 -      {
    3.25 -        val syntax = session.current_syntax()
    3.26 -        val ctxt =
    3.27 -          context match {
    3.28 -            case c: Line_Context => c.context
    3.29 -            case _ => Scan.Finished
    3.30 -          }
    3.31 -        val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
    3.32 -        val context1 = new Line_Context(ctxt1)
    3.33 +  class Marker extends TokenMarker
    3.34 +  {
    3.35 +    override def markTokens(context: TokenMarker.LineContext,
    3.36 +        handler: TokenHandler, line: Segment): TokenMarker.LineContext =
    3.37 +    {
    3.38 +      val symbols = Isabelle.system.symbols
    3.39 +      val syntax = Isabelle.session.current_syntax()
    3.40  
    3.41 -        val extended = extended_styles(session.system.symbols, line)
    3.42 +      val ctxt =
    3.43 +        context match {
    3.44 +          case c: Line_Context => c.context
    3.45 +          case _ => Scan.Finished
    3.46 +        }
    3.47 +      val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
    3.48 +      val context1 = new Line_Context(ctxt1)
    3.49 +
    3.50 +      val extended = extended_styles(symbols, line)
    3.51  
    3.52 -        var offset = 0
    3.53 -        for (token <- tokens) {
    3.54 -          val style = Isabelle_Markup.token_markup(syntax, token)
    3.55 -          val length = token.source.length
    3.56 -          val end_offset = offset + length
    3.57 -          if ((offset until end_offset) exists extended.isDefinedAt) {
    3.58 -            for (i <- offset until end_offset) {
    3.59 -              val style1 =
    3.60 -                extended.get(i) match {
    3.61 -                  case None => style
    3.62 -                  case Some(ext) => ext(style)
    3.63 -                }
    3.64 -              handler.handleToken(line, style1, i, 1, context1)
    3.65 -            }
    3.66 +      var offset = 0
    3.67 +      for (token <- tokens) {
    3.68 +        val style = Isabelle_Markup.token_markup(syntax, token)
    3.69 +        val length = token.source.length
    3.70 +        val end_offset = offset + length
    3.71 +        if ((offset until end_offset) exists extended.isDefinedAt) {
    3.72 +          for (i <- offset until end_offset) {
    3.73 +            val style1 =
    3.74 +              extended.get(i) match {
    3.75 +                case None => style
    3.76 +                case Some(ext) => ext(style)
    3.77 +              }
    3.78 +            handler.handleToken(line, style1, i, 1, context1)
    3.79            }
    3.80 -          else handler.handleToken(line, style, offset, length, context1)
    3.81 -          offset += length
    3.82          }
    3.83 -        handler.handleToken(line, JEditToken.END, line.count, 0, context1)
    3.84 +        else handler.handleToken(line, style, offset, length, context1)
    3.85 +        offset += length
    3.86 +      }
    3.87 +      handler.handleToken(line, JEditToken.END, line.count, 0, context1)
    3.88 +
    3.89 +      val context2 = context1.intern
    3.90 +      handler.setLineContext(context2)
    3.91 +      context2
    3.92 +    }
    3.93 +  }
    3.94 +
    3.95  
    3.96 -        val context2 = context1.intern
    3.97 -        handler.setLineContext(context2)
    3.98 -        context2
    3.99 -      }
   3.100 +  /* mode provider */
   3.101 +
   3.102 +  class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
   3.103 +  {
   3.104 +    for (mode <- orig_provider.getModes) addMode(mode)
   3.105 +
   3.106 +    val isabelle_token_marker = new Token_Markup.Marker
   3.107 +
   3.108 +    override def loadMode(mode: Mode, xmh: XModeHandler)
   3.109 +    {
   3.110 +      super.loadMode(mode, xmh)
   3.111 +      if (mode.getName == "isabelle")
   3.112 +        mode.setTokenMarker(isabelle_token_marker)
   3.113      }
   3.114 +  }
   3.115  }
   3.116