--- a/src/Tools/jEdit/src/token_markup.scala Thu Aug 29 13:53:45 2013 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Thu Aug 29 15:24:36 2013 +0200
@@ -208,8 +208,6 @@
class Marker(mode: String) extends TokenMarker
{
- private val ext_styles = mode == "isabelle"
-
override def markTokens(context: TokenMarker.LineContext,
handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
{
@@ -234,9 +232,7 @@
(List((JEditToken.NULL, token)), new Line_Context(None))
}
- val extended =
- if (ext_styles) extended_styles(line)
- else Map.empty[Text.Offset, Byte => Byte]
+ val extended = extended_styles(line)
var offset = 0
for ((style, token) <- styled_tokens) {