--- a/src/Tools/jEdit/src/isabelle.scala Thu May 07 22:12:05 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Fri May 08 10:19:44 2015 +0200
@@ -78,10 +78,8 @@
def buffer_token_marker(buffer: Buffer): Option[TokenMarker] =
{
val mode = JEdit_Lib.buffer_mode(buffer)
- val new_token_marker =
- if (mode == "isabelle") Some(new Token_Markup.Marker(mode, Some(buffer)))
- else mode_token_marker(mode)
- if (new_token_marker == Some(buffer.getTokenMarker)) None else new_token_marker
+ if (mode == "isabelle") Some(new Token_Markup.Marker(mode, Some(buffer)))
+ else mode_token_marker(mode)
}