# HG changeset patch
# User wenzelm
# Date 1377782676 -7200
# Node ID c31532691e5530704caeff1020786a1ed7a49c8f
# Parent  6aa348237973a35ea0243a41751e8c47776b2905
always use extended styles (despite de26cf3191a3);

diff -r 6aa348237973 -r c31532691e55 src/Tools/jEdit/src/token_markup.scala
--- 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) {