always use extended styles (despite de26cf3191a3);
authorwenzelm
Thu, 29 Aug 2013 15:24:36 +0200
changeset 53278 c31532691e55
parent 53277 6aa348237973
child 53279 763d35697338
always use extended styles (despite de26cf3191a3);
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) {