--- a/src/Tools/jEdit/src/token_markup.scala Mon Dec 01 17:51:07 2014 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Mon Dec 01 19:25:20 2014 +0100
@@ -14,7 +14,7 @@
import java.awt.geom.AffineTransform
import org.gjt.sp.util.SyntaxUtilities
-import org.gjt.sp.jedit.{jEdit, Mode}
+import org.gjt.sp.jedit.{jEdit, Mode, Buffer}
import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler,
ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
import org.gjt.sp.jedit.textarea.{TextArea, Selection}
@@ -308,8 +308,14 @@
/* token marker */
- class Marker(mode: String) extends TokenMarker
+ class Marker(mode: String, opt_buffer: Option[Buffer]) extends TokenMarker
{
+ override def toString: String =
+ opt_buffer match {
+ case None => "Marker(" + mode + ")"
+ case Some(buffer) => "Marker(" + mode + "," + JEdit_Lib.buffer_name(buffer) + ")"
+ }
+
override def markTokens(context: TokenMarker.LineContext,
handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
{
@@ -319,8 +325,13 @@
val context1 =
{
+ val opt_syntax =
+ opt_buffer match {
+ case Some(buffer) => Isabelle.buffer_syntax(buffer)
+ case None => Isabelle.mode_syntax(mode)
+ }
val (styled_tokens, context1) =
- (line_context.context, Isabelle.mode_syntax(mode)) match {
+ (line_context.context, opt_syntax) match {
case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" =>
val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt)
val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
@@ -378,17 +389,7 @@
override def loadMode(mode: Mode, xmh: XModeHandler)
{
super.loadMode(mode, xmh)
- Isabelle.token_marker(mode.getName).foreach(mode.setTokenMarker _)
- }
- }
-
- def refresh_buffer(buffer: JEditBuffer)
- {
- Isabelle.token_marker(JEdit_Lib.buffer_mode(buffer)) match {
- case None =>
- case Some(marker) =>
- buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
- buffer.setTokenMarker(marker)
+ Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker _)
}
}
}