# HG changeset patch # User wenzelm # Date 1308432874 -7200 # Node ID 5cf548485529085794fb50437c1d57eec77d404b # Parent be760a642d385a10fec14a9dfa81509aa5ab17dc avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider; diff -r be760a642d38 -r 5cf548485529 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Sat Jun 18 22:01:22 2011 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Sat Jun 18 23:34:34 2011 +0200 @@ -129,30 +129,18 @@ } - /* token marker */ - - private val token_marker = Token_Markup.token_marker(session, buffer) - - /* activation */ def activate() { - buffer.setTokenMarker(token_marker) buffer.addBufferListener(buffer_listener) buffer.propertiesChanged() pending_edits.init() } - def refresh() - { - buffer.setTokenMarker(token_marker) - } - def deactivate() { pending_edits.flush() - buffer.setTokenMarker(buffer.getMode.getTokenMarker) buffer.removeBufferListener(buffer_listener) } } diff -r be760a642d38 -r 5cf548485529 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Sat Jun 18 22:01:22 2011 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Sat Jun 18 23:34:34 2011 +0200 @@ -19,7 +19,7 @@ Buffer, EditPane, ServiceManager, View} import org.gjt.sp.jedit.buffer.JEditBuffer import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} -import org.gjt.sp.jedit.syntax.{Token => JEditToken} +import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider} import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged} import org.gjt.sp.jedit.gui.DockableWindowManager @@ -290,7 +290,7 @@ Isabelle.swing_buffer_lock(buffer) { val opt_model = Document_Model(buffer) match { - case Some(model) => model.refresh; Some(model) + case Some(model) => Some(model) case None => Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match { case Some((dir, thy_name)) => @@ -408,8 +408,10 @@ } } + override def start() { + ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance) Isabelle.plugin = this Isabelle.setup_tooltips() Isabelle.system = new Isabelle_System diff -r be760a642d38 -r 5cf548485529 src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala Sat Jun 18 22:01:22 2011 +0200 +++ b/src/Tools/jEdit/src/token_markup.scala Sat Jun 18 23:34:34 2011 +0200 @@ -9,8 +9,10 @@ import isabelle._ -import org.gjt.sp.jedit.Buffer -import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet} +import org.gjt.sp.jedit.Mode +import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, + ParserRuleSet, ModeProvider, XModeHandler} + import javax.swing.text.Segment @@ -78,46 +80,65 @@ } } - def token_marker(session: Session, buffer: Buffer): TokenMarker = - new TokenMarker { - override def markTokens(context: TokenMarker.LineContext, - handler: TokenHandler, line: Segment): TokenMarker.LineContext = - { - val syntax = session.current_syntax() - val ctxt = - context match { - case c: Line_Context => c.context - case _ => Scan.Finished - } - val (tokens, ctxt1) = syntax.scan_context(line, ctxt) - val context1 = new Line_Context(ctxt1) + class Marker extends TokenMarker + { + override def markTokens(context: TokenMarker.LineContext, + handler: TokenHandler, line: Segment): TokenMarker.LineContext = + { + val symbols = Isabelle.system.symbols + val syntax = Isabelle.session.current_syntax() - val extended = extended_styles(session.system.symbols, line) + val ctxt = + context match { + case c: Line_Context => c.context + case _ => Scan.Finished + } + val (tokens, ctxt1) = syntax.scan_context(line, ctxt) + val context1 = new Line_Context(ctxt1) + + val extended = extended_styles(symbols, line) - var offset = 0 - for (token <- tokens) { - val style = Isabelle_Markup.token_markup(syntax, token) - val length = token.source.length - val end_offset = offset + length - if ((offset until end_offset) exists extended.isDefinedAt) { - for (i <- offset until end_offset) { - val style1 = - extended.get(i) match { - case None => style - case Some(ext) => ext(style) - } - handler.handleToken(line, style1, i, 1, context1) - } + var offset = 0 + for (token <- tokens) { + val style = Isabelle_Markup.token_markup(syntax, token) + val length = token.source.length + val end_offset = offset + length + if ((offset until end_offset) exists extended.isDefinedAt) { + for (i <- offset until end_offset) { + val style1 = + extended.get(i) match { + case None => style + case Some(ext) => ext(style) + } + handler.handleToken(line, style1, i, 1, context1) } - else handler.handleToken(line, style, offset, length, context1) - offset += length } - handler.handleToken(line, JEditToken.END, line.count, 0, context1) + else handler.handleToken(line, style, offset, length, context1) + offset += length + } + handler.handleToken(line, JEditToken.END, line.count, 0, context1) + + val context2 = context1.intern + handler.setLineContext(context2) + context2 + } + } + - val context2 = context1.intern - handler.setLineContext(context2) - context2 - } + /* mode provider */ + + class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider + { + for (mode <- orig_provider.getModes) addMode(mode) + + val isabelle_token_marker = new Token_Markup.Marker + + override def loadMode(mode: Mode, xmh: XModeHandler) + { + super.loadMode(mode, xmh) + if (mode.getName == "isabelle") + mode.setTokenMarker(isabelle_token_marker) } + } }