src/Tools/jEdit/src/isabelle_rendering.scala
author wenzelm
Mon Jan 16 13:19:44 2012 +0100 (2012-01-16)
changeset 46234 de441d4ff1be
parent 46228 302d3ecff25d
child 46235 e4e0b5190f3d
permissions -rw-r--r--
tuned;
wenzelm@45665
     1
/*  Title:      Tools/jEdit/src/isabelle_rendering.scala
wenzelm@39178
     2
    Author:     Makarius
wenzelm@39178
     3
wenzelm@39178
     4
Isabelle specific physical rendering and markup selection.
wenzelm@39178
     5
*/
wenzelm@39178
     6
wenzelm@39178
     7
package isabelle.jedit
wenzelm@39178
     8
wenzelm@39178
     9
wenzelm@39178
    10
import isabelle._
wenzelm@39178
    11
wenzelm@39178
    12
import java.awt.Color
wenzelm@46227
    13
import javax.swing.Icon
wenzelm@39178
    14
wenzelm@43386
    15
import org.lobobrowser.util.gui.ColorFactory
wenzelm@43414
    16
import org.gjt.sp.jedit.syntax.{Token => JEditToken}
wenzelm@39178
    17
wenzelm@45460
    18
import scala.collection.immutable.SortedMap
wenzelm@45460
    19
wenzelm@39178
    20
wenzelm@45665
    21
object Isabelle_Rendering
wenzelm@39178
    22
{
wenzelm@39178
    23
  /* physical rendering */
wenzelm@39178
    24
wenzelm@43377
    25
  // see http://www.w3schools.com/css/css_colornames.asp
wenzelm@43377
    26
wenzelm@43386
    27
  def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
wenzelm@43386
    28
wenzelm@44579
    29
  val outdated_color = new Color(238, 227, 227)
wenzelm@46166
    30
  val unprocessed_color = new Color(255, 160, 160)
wenzelm@46166
    31
  val unprocessed1_color = new Color(255, 160, 160, 50)
wenzelm@44611
    32
  val running_color = new Color(97, 0, 97)
wenzelm@44611
    33
  val running1_color = new Color(97, 0, 97, 100)
wenzelm@39178
    34
wenzelm@39690
    35
  val light_color = new Color(240, 240, 240)
wenzelm@46227
    36
  val writeln_color = new Color(192, 192, 192)
wenzelm@39692
    37
  val warning_color = new Color(255, 140, 0)
wenzelm@39691
    38
  val error_color = new Color(178, 34, 34)
wenzelm@44866
    39
  val error1_color = new Color(178, 34, 34, 50)
wenzelm@39690
    40
  val bad_color = new Color(255, 106, 106, 100)
wenzelm@42171
    41
  val hilite_color = new Color(255, 204, 102, 100)
wenzelm@39178
    42
wenzelm@44546
    43
  val quoted_color = new Color(139, 139, 139, 25)
wenzelm@44545
    44
  val subexp_color = new Color(80, 80, 80, 50)
wenzelm@43435
    45
wenzelm@43388
    46
  val keyword1_color = get_color("#006699")
wenzelm@43388
    47
  val keyword2_color = get_color("#009966")
wenzelm@43388
    48
wenzelm@46227
    49
  private val writeln_pri = 1
wenzelm@46227
    50
  private val warning_pri = 2
wenzelm@46227
    51
  private val legacy_pri = 3
wenzelm@46227
    52
  private val error_pri = 4
wenzelm@39178
    53
wenzelm@39178
    54
wenzelm@46166
    55
  /* command overview */
wenzelm@39178
    56
wenzelm@46227
    57
  def overview_color(snapshot: Document.Snapshot, range: Text.Range): Option[Color] =
wenzelm@39178
    58
  {
wenzelm@39178
    59
    if (snapshot.is_outdated) None
wenzelm@46166
    60
    else {
wenzelm@46227
    61
      val results =
wenzelm@46227
    62
        snapshot.cumulate_markup[(Protocol.Status, Int)](
wenzelm@46227
    63
          range, (Protocol.Status.init, 0),
wenzelm@46227
    64
          Some(Protocol.command_status_markup + Isabelle_Markup.WARNING + Isabelle_Markup.ERROR),
wenzelm@46227
    65
          {
wenzelm@46227
    66
            case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
wenzelm@46227
    67
              if (markup.name == Isabelle_Markup.WARNING) (status, pri max warning_pri)
wenzelm@46227
    68
              else if (markup.name == Isabelle_Markup.ERROR) (status, pri max error_pri)
wenzelm@46227
    69
              else (Protocol.command_status(status, markup), pri)
wenzelm@46227
    70
          })
wenzelm@46227
    71
      if (results.isEmpty) None
wenzelm@46227
    72
      else {
wenzelm@46227
    73
        val (status, pri) =
wenzelm@46227
    74
          ((Protocol.Status.init, 0) /: results) {
wenzelm@46227
    75
            case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) }
wenzelm@46166
    76
wenzelm@46227
    77
        if (pri == warning_pri) Some(warning_color)
wenzelm@46227
    78
        else if (pri == error_pri) Some(error_color)
wenzelm@46227
    79
        else if (status.is_unprocessed) Some(unprocessed_color)
wenzelm@46227
    80
        else if (status.is_running) Some(running_color)
wenzelm@46227
    81
        else if (status.is_failed) Some(error_color)
wenzelm@46166
    82
        else None
wenzelm@39178
    83
      }
wenzelm@46166
    84
    }
wenzelm@39178
    85
  }
wenzelm@39178
    86
wenzelm@39178
    87
wenzelm@39178
    88
  /* markup selectors */
wenzelm@39178
    89
wenzelm@46234
    90
  private val subexp_include =
wenzelm@46234
    91
    Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
wenzelm@46234
    92
      Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
wenzelm@46234
    93
      Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND,
wenzelm@46234
    94
      Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE,
wenzelm@46234
    95
      Isabelle_Markup.DOC_SOURCE)
wenzelm@46234
    96
wenzelm@46234
    97
  def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Color]] =
wenzelm@46234
    98
  {
wenzelm@46234
    99
    snapshot.select_markup(range, Some(subexp_include),
wenzelm@46234
   100
        {
wenzelm@46234
   101
          case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
wenzelm@46234
   102
            Text.Info(snapshot.convert(range), subexp_color)
wenzelm@46234
   103
        }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
wenzelm@46234
   104
  }
wenzelm@46234
   105
wenzelm@46234
   106
wenzelm@46178
   107
  def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
wenzelm@46199
   108
  {
wenzelm@46199
   109
    val msgs =
wenzelm@46199
   110
      snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
wenzelm@46199
   111
        Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
wenzelm@46199
   112
        {
wenzelm@46199
   113
          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
wenzelm@46199
   114
          if markup == Isabelle_Markup.WRITELN ||
wenzelm@46199
   115
              markup == Isabelle_Markup.WARNING ||
wenzelm@46199
   116
              markup == Isabelle_Markup.ERROR =>
wenzelm@46199
   117
            msgs + (serial ->
wenzelm@46199
   118
              Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
wenzelm@46199
   119
        }).toList.flatMap(_.info)
wenzelm@46199
   120
    if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2)))
wenzelm@46199
   121
  }
wenzelm@39740
   122
wenzelm@43376
   123
wenzelm@43431
   124
  private val tooltips: Map[String, String] =
wenzelm@43431
   125
    Map(
wenzelm@45666
   126
      Isabelle_Markup.SORT -> "sort",
wenzelm@45666
   127
      Isabelle_Markup.TYP -> "type",
wenzelm@45666
   128
      Isabelle_Markup.TERM -> "term",
wenzelm@45666
   129
      Isabelle_Markup.PROP -> "proposition",
wenzelm@45666
   130
      Isabelle_Markup.TOKEN_RANGE -> "inner syntax token",
wenzelm@45666
   131
      Isabelle_Markup.FREE -> "free variable",
wenzelm@45666
   132
      Isabelle_Markup.SKOLEM -> "skolem variable",
wenzelm@45666
   133
      Isabelle_Markup.BOUND -> "bound variable",
wenzelm@45666
   134
      Isabelle_Markup.VAR -> "schematic variable",
wenzelm@45666
   135
      Isabelle_Markup.TFREE -> "free type variable",
wenzelm@45666
   136
      Isabelle_Markup.TVAR -> "schematic type variable",
wenzelm@45666
   137
      Isabelle_Markup.ML_SOURCE -> "ML source",
wenzelm@45666
   138
      Isabelle_Markup.DOC_SOURCE -> "document source")
wenzelm@43431
   139
wenzelm@45445
   140
  private def string_of_typing(kind: String, body: XML.Body): String =
wenzelm@45445
   141
    Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
wenzelm@45445
   142
      margin = Isabelle.Int_Property("tooltip-margin"))
wenzelm@45445
   143
wenzelm@46178
   144
  def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
wenzelm@46178
   145
  {
wenzelm@46178
   146
    val tip1 =
wenzelm@46178
   147
      snapshot.select_markup(range,
wenzelm@46178
   148
        Some(Set(Isabelle_Markup.ENTITY, Isabelle_Markup.ML_TYPING) ++ tooltips.keys),
wenzelm@46178
   149
        {
wenzelm@46178
   150
          case Text.Info(_, XML.Elem(Isabelle_Markup.Entity(kind, name), _)) =>
wenzelm@46178
   151
            kind + " " + quote(name)
wenzelm@46178
   152
          case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body)) =>
wenzelm@46178
   153
            string_of_typing("ML:", body)
wenzelm@46178
   154
          case Text.Info(_, XML.Elem(Markup(name, _), _))
wenzelm@46178
   155
          if tooltips.isDefinedAt(name) => tooltips(name)
wenzelm@46178
   156
        })
wenzelm@46178
   157
    val tip2 =
wenzelm@46178
   158
      snapshot.select_markup(range, Some(Set(Isabelle_Markup.TYPING)),
wenzelm@46178
   159
        {
wenzelm@46178
   160
          case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body)) =>
wenzelm@46178
   161
            string_of_typing("::", body)
wenzelm@46178
   162
        })
wenzelm@42302
   163
wenzelm@46178
   164
    val tips =
wenzelm@46198
   165
      (tip1 match { case Text.Info(_, text) #:: _ => List(text) case _ => Nil }) :::
wenzelm@46198
   166
      (tip2 match { case Text.Info(_, text) #:: _ => List(text) case _ => Nil })
wenzelm@46178
   167
wenzelm@46196
   168
    if (tips.isEmpty) None else Some(cat_lines(tips))
wenzelm@46178
   169
  }
wenzelm@45460
   170
wenzelm@46234
   171
wenzelm@46234
   172
  private val gutter_icons = Map(
wenzelm@46234
   173
    warning_pri -> Isabelle.load_icon("16x16/status/dialog-information.png"),
wenzelm@46234
   174
    legacy_pri -> Isabelle.load_icon("16x16/status/dialog-warning.png"),
wenzelm@46234
   175
    error_pri -> Isabelle.load_icon("16x16/status/dialog-error.png"))
wenzelm@46234
   176
wenzelm@46234
   177
  def gutter_message(snapshot: Document.Snapshot, range: Text.Range): Option[Icon] =
wenzelm@46234
   178
  {
wenzelm@46234
   179
    val results =
wenzelm@46234
   180
      snapshot.cumulate_markup[Int](range, 0,
wenzelm@46234
   181
        Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
wenzelm@46234
   182
        {
wenzelm@46234
   183
          case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body))) =>
wenzelm@46234
   184
            body match {
wenzelm@46234
   185
              case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => pri max legacy_pri
wenzelm@46234
   186
              case _ => pri max warning_pri
wenzelm@46234
   187
            }
wenzelm@46234
   188
          case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _))) =>
wenzelm@46234
   189
            pri max error_pri
wenzelm@46234
   190
        })
wenzelm@46234
   191
    val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
wenzelm@46234
   192
    gutter_icons.get(pri)
wenzelm@46234
   193
  }
wenzelm@46234
   194
wenzelm@46234
   195
wenzelm@46234
   196
  private val squiggly_colors = Map(
wenzelm@46234
   197
    writeln_pri -> writeln_color,
wenzelm@46234
   198
    warning_pri -> warning_color,
wenzelm@46234
   199
    error_pri -> error_color)
wenzelm@46234
   200
wenzelm@46234
   201
  def squiggly_underline(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
wenzelm@46234
   202
  {
wenzelm@46234
   203
    val results =
wenzelm@46234
   204
      snapshot.cumulate_markup[Int](range, 0,
wenzelm@46234
   205
        Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
wenzelm@46234
   206
        {
wenzelm@46234
   207
          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) =>
wenzelm@46234
   208
            name match {
wenzelm@46234
   209
              case Isabelle_Markup.WRITELN => pri max writeln_pri
wenzelm@46234
   210
              case Isabelle_Markup.WARNING => pri max warning_pri
wenzelm@46234
   211
              case Isabelle_Markup.ERROR => pri max error_pri
wenzelm@46234
   212
              case _ => pri
wenzelm@46234
   213
            }
wenzelm@46234
   214
        })
wenzelm@46234
   215
    for {
wenzelm@46234
   216
      Text.Info(r, pri) <- results
wenzelm@46234
   217
      color <- squiggly_colors.get(pri)
wenzelm@46234
   218
    } yield Text.Info(r, color)
wenzelm@46234
   219
  }
wenzelm@46234
   220
wenzelm@42302
   221
wenzelm@46234
   222
  def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
wenzelm@46178
   223
  {
wenzelm@46234
   224
    if (snapshot.is_outdated) Stream(Text.Info(range, outdated_color))
wenzelm@46234
   225
    else
wenzelm@46234
   226
      for {
wenzelm@46234
   227
        Text.Info(r, result) <-
wenzelm@46234
   228
          snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
wenzelm@46234
   229
            range, (Some(Protocol.Status.init), None),
wenzelm@46234
   230
            Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE),
wenzelm@46234
   231
            {
wenzelm@46234
   232
              case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
wenzelm@46234
   233
              if (Protocol.command_status_markup(markup.name)) =>
wenzelm@46234
   234
                (Some(Protocol.command_status(status, markup)), color)
wenzelm@46234
   235
              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
wenzelm@46234
   236
                (None, Some(bad_color))
wenzelm@46234
   237
              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
wenzelm@46234
   238
                (None, Some(hilite_color))
wenzelm@46234
   239
            })
wenzelm@46234
   240
        color <-
wenzelm@46234
   241
          (result match {
wenzelm@46234
   242
            case (Some(status), _) =>
wenzelm@46234
   243
              if (status.is_running) Some(running1_color)
wenzelm@46234
   244
              else if (status.is_unprocessed) Some(unprocessed1_color)
wenzelm@46234
   245
              else None
wenzelm@46234
   246
            case (_, opt_color) => opt_color
wenzelm@46234
   247
          })
wenzelm@46234
   248
      } yield Text.Info(r, color)
wenzelm@46178
   249
  }
wenzelm@39179
   250
wenzelm@39179
   251
wenzelm@46234
   252
  def background2(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
wenzelm@46234
   253
    snapshot.select_markup(range,
wenzelm@46234
   254
      Some(Set(Isabelle_Markup.TOKEN_RANGE)),
wenzelm@46234
   255
      {
wenzelm@46234
   256
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
wenzelm@46234
   257
      })
wenzelm@46234
   258
wenzelm@46234
   259
wenzelm@46234
   260
  def foreground(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
wenzelm@46234
   261
    snapshot.select_markup(range,
wenzelm@46234
   262
      Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)),
wenzelm@46234
   263
      {
wenzelm@46234
   264
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
wenzelm@46234
   265
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
wenzelm@46234
   266
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
wenzelm@46234
   267
      })
wenzelm@46234
   268
wenzelm@46234
   269
wenzelm@46234
   270
  private val text_colors: Map[String, Color] =
wenzelm@46234
   271
    Map(
wenzelm@46234
   272
      Isabelle_Markup.STRING -> get_color("black"),
wenzelm@46234
   273
      Isabelle_Markup.ALTSTRING -> get_color("black"),
wenzelm@46234
   274
      Isabelle_Markup.VERBATIM -> get_color("black"),
wenzelm@46234
   275
      Isabelle_Markup.LITERAL -> keyword1_color,
wenzelm@46234
   276
      Isabelle_Markup.DELIMITER -> get_color("black"),
wenzelm@46234
   277
      Isabelle_Markup.TFREE -> get_color("#A020F0"),
wenzelm@46234
   278
      Isabelle_Markup.TVAR -> get_color("#A020F0"),
wenzelm@46234
   279
      Isabelle_Markup.FREE -> get_color("blue"),
wenzelm@46234
   280
      Isabelle_Markup.SKOLEM -> get_color("#D2691E"),
wenzelm@46234
   281
      Isabelle_Markup.BOUND -> get_color("green"),
wenzelm@46234
   282
      Isabelle_Markup.VAR -> get_color("#00009B"),
wenzelm@46234
   283
      Isabelle_Markup.INNER_STRING -> get_color("#D2691E"),
wenzelm@46234
   284
      Isabelle_Markup.INNER_COMMENT -> get_color("#8B0000"),
wenzelm@46234
   285
      Isabelle_Markup.DYNAMIC_FACT -> get_color("#7BA428"),
wenzelm@46234
   286
      Isabelle_Markup.ML_KEYWORD -> keyword1_color,
wenzelm@46234
   287
      Isabelle_Markup.ML_DELIMITER -> get_color("black"),
wenzelm@46234
   288
      Isabelle_Markup.ML_NUMERAL -> get_color("red"),
wenzelm@46234
   289
      Isabelle_Markup.ML_CHAR -> get_color("#D2691E"),
wenzelm@46234
   290
      Isabelle_Markup.ML_STRING -> get_color("#D2691E"),
wenzelm@46234
   291
      Isabelle_Markup.ML_COMMENT -> get_color("#8B0000"),
wenzelm@46234
   292
      Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"),
wenzelm@46234
   293
      Isabelle_Markup.ANTIQ -> get_color("blue"))
wenzelm@46234
   294
wenzelm@46234
   295
  private val text_color_elements = Set.empty[String] ++ text_colors.keys
wenzelm@46234
   296
wenzelm@46234
   297
  def text_color(snapshot: Document.Snapshot, range: Text.Range, color: Color)
wenzelm@46234
   298
      : Stream[Text.Info[Color]] =
wenzelm@46234
   299
    snapshot.cumulate_markup(range, color, Some(text_color_elements),
wenzelm@46234
   300
      {
wenzelm@46234
   301
        case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
wenzelm@46234
   302
        if text_colors.isDefinedAt(m) => text_colors(m)
wenzelm@46234
   303
      })
wenzelm@46234
   304
wenzelm@46234
   305
wenzelm@39179
   306
  /* token markup -- text styles */
wenzelm@39179
   307
wenzelm@39179
   308
  private val command_style: Map[String, Byte] =
wenzelm@39179
   309
  {
wenzelm@43414
   310
    import JEditToken._
wenzelm@39179
   311
    Map[String, Byte](
wenzelm@39179
   312
      Keyword.THY_END -> KEYWORD2,
wenzelm@39179
   313
      Keyword.THY_SCRIPT -> LABEL,
wenzelm@39179
   314
      Keyword.PRF_SCRIPT -> LABEL,
wenzelm@39179
   315
      Keyword.PRF_ASM -> KEYWORD3,
wenzelm@39179
   316
      Keyword.PRF_ASM_GOAL -> KEYWORD3
wenzelm@39179
   317
    ).withDefaultValue(KEYWORD1)
wenzelm@39179
   318
  }
wenzelm@39179
   319
wenzelm@43414
   320
  private val token_style: Map[Token.Kind.Value, Byte] =
wenzelm@39179
   321
  {
wenzelm@43414
   322
    import JEditToken._
wenzelm@43414
   323
    Map[Token.Kind.Value, Byte](
wenzelm@43414
   324
      Token.Kind.KEYWORD -> KEYWORD2,
wenzelm@43414
   325
      Token.Kind.IDENT -> NULL,
wenzelm@43414
   326
      Token.Kind.LONG_IDENT -> NULL,
wenzelm@43414
   327
      Token.Kind.SYM_IDENT -> NULL,
wenzelm@43414
   328
      Token.Kind.VAR -> NULL,
wenzelm@43414
   329
      Token.Kind.TYPE_IDENT -> NULL,
wenzelm@43414
   330
      Token.Kind.TYPE_VAR -> NULL,
wenzelm@43414
   331
      Token.Kind.NAT -> NULL,
wenzelm@43414
   332
      Token.Kind.FLOAT -> NULL,
wenzelm@43431
   333
      Token.Kind.STRING -> LITERAL1,
wenzelm@43431
   334
      Token.Kind.ALT_STRING -> LITERAL2,
wenzelm@43414
   335
      Token.Kind.VERBATIM -> COMMENT3,
wenzelm@43414
   336
      Token.Kind.SPACE -> NULL,
wenzelm@43414
   337
      Token.Kind.COMMENT -> COMMENT1,
wenzelm@43414
   338
      Token.Kind.UNPARSED -> INVALID
wenzelm@39179
   339
    ).withDefaultValue(NULL)
wenzelm@39179
   340
  }
wenzelm@39179
   341
wenzelm@43414
   342
  def token_markup(syntax: Outer_Syntax, token: Token): Byte =
wenzelm@43430
   343
    if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
wenzelm@43430
   344
    else if (token.is_operator) JEditToken.OPERATOR
wenzelm@43414
   345
    else token_style(token.kind)
wenzelm@39178
   346
}