src/Tools/jEdit/src/isabelle_rendering.scala
author wenzelm
Thu, 12 Jan 2012 22:05:54 +0100
changeset 46199 9d2273d50f4f
parent 46198 cd040c5772de
child 46205 07e334ad2e2a
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45665
129db1416717 renamed Isabelle_Markup to Isabelle_Rendering to emphasize its meaning and make room for Pure Isabelle_Markup module;
wenzelm
parents: 45489
diff changeset
     1
/*  Title:      Tools/jEdit/src/isabelle_rendering.scala
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
     3
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
     4
Isabelle specific physical rendering and markup selection.
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
     5
*/
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
     6
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
     8
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
     9
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    10
import isabelle._
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    11
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    12
import java.awt.Color
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    13
43386
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
    14
import org.lobobrowser.util.gui.ColorFactory
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    15
import org.gjt.sp.jedit.syntax.{Token => JEditToken}
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    16
45460
dcd02d1a25d7 more tooltip content;
wenzelm
parents: 45454
diff changeset
    17
import scala.collection.immutable.SortedMap
dcd02d1a25d7 more tooltip content;
wenzelm
parents: 45454
diff changeset
    18
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    19
45665
129db1416717 renamed Isabelle_Markup to Isabelle_Rendering to emphasize its meaning and make room for Pure Isabelle_Markup module;
wenzelm
parents: 45489
diff changeset
    20
object Isabelle_Rendering
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    21
{
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    22
  /* physical rendering */
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    23
43377
ba199d75bc7e more accurate CSS colors;
wenzelm
parents: 43376
diff changeset
    24
  // see http://www.w3schools.com/css/css_colornames.asp
ba199d75bc7e more accurate CSS colors;
wenzelm
parents: 43376
diff changeset
    25
43386
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
    26
  def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
    27
44579
a9cf2380377d tuned colors -- more distance between outdated_color and quoted_color;
wenzelm
parents: 44549
diff changeset
    28
  val outdated_color = new Color(238, 227, 227)
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    29
  val unprocessed_color = new Color(255, 160, 160)
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    30
  val unprocessed1_color = new Color(255, 160, 160, 50)
44611
857c52a1c3f7 explicit running_color;
wenzelm
parents: 44602
diff changeset
    31
  val running_color = new Color(97, 0, 97)
857c52a1c3f7 explicit running_color;
wenzelm
parents: 44602
diff changeset
    32
  val running1_color = new Color(97, 0, 97, 100)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    33
39690
6c6164b37fef some attempts to improve visual appearance of bad text;
wenzelm
parents: 39512
diff changeset
    34
  val light_color = new Color(240, 240, 240)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    35
  val regular_color = new Color(192, 192, 192)
39692
b88a6bc371de tuned warning_color;
wenzelm
parents: 39691
diff changeset
    36
  val warning_color = new Color(255, 140, 0)
39691
4ce5f79df87a tuned error_color;
wenzelm
parents: 39690
diff changeset
    37
  val error_color = new Color(178, 34, 34)
44866
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44723
diff changeset
    38
  val error1_color = new Color(178, 34, 34, 50)
39690
6c6164b37fef some attempts to improve visual appearance of bad text;
wenzelm
parents: 39512
diff changeset
    39
  val bad_color = new Color(255, 106, 106, 100)
42171
620343510c88 visualize skolem and hilite (undeclared frees);
wenzelm
parents: 42136
diff changeset
    40
  val hilite_color = new Color(255, 204, 102, 100)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    41
44546
794a32d58c77 tuned colors;
wenzelm
parents: 44545
diff changeset
    42
  val quoted_color = new Color(139, 139, 139, 25)
44545
3c40007aa031 transparent foreground color for quoted entities;
wenzelm
parents: 44181
diff changeset
    43
  val subexp_color = new Color(80, 80, 80, 50)
43435
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
    44
43388
34492601c0e0 tuned colors;
wenzelm
parents: 43386
diff changeset
    45
  val keyword1_color = get_color("#006699")
34492601c0e0 tuned colors;
wenzelm
parents: 43386
diff changeset
    46
  val keyword2_color = get_color("#009966")
34492601c0e0 tuned colors;
wenzelm
parents: 43386
diff changeset
    47
39181
2257eded8323 Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents: 39179
diff changeset
    48
  class Icon(val priority: Int, val icon: javax.swing.Icon)
2257eded8323 Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents: 39179
diff changeset
    49
  {
2257eded8323 Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents: 39179
diff changeset
    50
    def >= (that: Icon): Boolean = this.priority >= that.priority
2257eded8323 Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents: 39179
diff changeset
    51
  }
44547
5a35790413f5 less aggressive warning icon;
wenzelm
parents: 44546
diff changeset
    52
  val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-information.png"))
44549
5e5e6ad3922c explicit markup for legacy warnings;
wenzelm
parents: 44547
diff changeset
    53
  val legacy_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-warning.png"))
5e5e6ad3922c explicit markup for legacy warnings;
wenzelm
parents: 44547
diff changeset
    54
  val error_icon = new Icon(3, Isabelle.load_icon("16x16/status/dialog-error.png"))
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    55
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    56
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    57
  /* command overview */
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    58
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    59
  def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    60
  {
44582
479c07072992 tuned signature;
wenzelm
parents: 44579
diff changeset
    61
    val state = snapshot.command_state(command)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    62
    if (snapshot.is_outdated) None
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    63
    else {
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    64
      val status = Protocol.command_status(state.status)
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    65
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    66
      if (status.is_unprocessed) Some(unprocessed_color)
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    67
      else if (status.is_running) Some(running_color)
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    68
      else if (status.is_finished) {
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    69
        if (state.results.exists(r => Protocol.is_error(r._2))) Some(error_color)
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    70
        else if (state.results.exists(r => Protocol.is_warning(r._2))) Some(warning_color)
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    71
        else None
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    72
      }
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    73
      else if (status.is_failed) Some(error_color)
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    74
      else None
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    75
    }
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    76
  }
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    77
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    78
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    79
  /* markup selectors */
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    80
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
    81
  def message_color(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
46198
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
    82
    snapshot.select_markup(range,
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
    83
      Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
    84
      {
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
    85
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN, _), _)) => regular_color
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
    86
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), _)) => warning_color
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
    87
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_color
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
    88
      })
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    89
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
    90
  def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
46199
wenzelm
parents: 46198
diff changeset
    91
  {
wenzelm
parents: 46198
diff changeset
    92
    val msgs =
wenzelm
parents: 46198
diff changeset
    93
      snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
wenzelm
parents: 46198
diff changeset
    94
        Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
wenzelm
parents: 46198
diff changeset
    95
        {
wenzelm
parents: 46198
diff changeset
    96
          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
wenzelm
parents: 46198
diff changeset
    97
          if markup == Isabelle_Markup.WRITELN ||
wenzelm
parents: 46198
diff changeset
    98
              markup == Isabelle_Markup.WARNING ||
wenzelm
parents: 46198
diff changeset
    99
              markup == Isabelle_Markup.ERROR =>
wenzelm
parents: 46198
diff changeset
   100
            msgs + (serial ->
wenzelm
parents: 46198
diff changeset
   101
              Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
wenzelm
parents: 46198
diff changeset
   102
        }).toList.flatMap(_.info)
wenzelm
parents: 46198
diff changeset
   103
    if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2)))
wenzelm
parents: 46198
diff changeset
   104
  }
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39704
diff changeset
   105
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   106
  def gutter_message(snapshot: Document.Snapshot, range: Text.Range): Option[Icon] =
46199
wenzelm
parents: 46198
diff changeset
   107
    snapshot.select_markup(range,
wenzelm
parents: 46198
diff changeset
   108
      Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
wenzelm
parents: 46198
diff changeset
   109
      {
wenzelm
parents: 46198
diff changeset
   110
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body)) =>
wenzelm
parents: 46198
diff changeset
   111
          body match {
wenzelm
parents: 46198
diff changeset
   112
            case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => legacy_icon
wenzelm
parents: 46198
diff changeset
   113
            case _ => warning_icon
wenzelm
parents: 46198
diff changeset
   114
          }
wenzelm
parents: 46198
diff changeset
   115
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon
wenzelm
parents: 46198
diff changeset
   116
      }).map(_.info).toList.sortWith(_ >= _).headOption
39181
2257eded8323 Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents: 39179
diff changeset
   117
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   118
  def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   119
    for {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   120
      Text.Info(r, result) <-
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   121
        snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   122
          range, (Some(Protocol.Status()), None),
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   123
          Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE),
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   124
          {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   125
            case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   126
            if (Protocol.command_status_markup(markup.name)) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   127
              (Some(Protocol.command_status(status, markup)), color)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   128
            case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   129
              (None, Some(bad_color))
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   130
            case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   131
              (None, Some(hilite_color))
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   132
          })
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   133
      color <-
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   134
        (result match {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   135
          case (Some(status), _) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   136
            if (status.is_running) Some(running1_color)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   137
            else if (status.is_unprocessed) Some(unprocessed1_color)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   138
            else None
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   139
          case (_, opt_color) => opt_color
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   140
        })
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   141
    } yield Text.Info(r, color)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   142
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   143
  def background2(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
46198
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   144
    snapshot.select_markup(range,
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   145
      Some(Set(Isabelle_Markup.TOKEN_RANGE)),
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   146
      {
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   147
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   148
      })
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   149
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   150
  def foreground(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
46198
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   151
    snapshot.select_markup(range,
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   152
      Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)),
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   153
      {
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   154
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   155
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   156
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   157
      })
44545
3c40007aa031 transparent foreground color for quoted entities;
wenzelm
parents: 44181
diff changeset
   158
43434
2fd41645813d tuned signature;
wenzelm
parents: 43432
diff changeset
   159
  private val text_colors: Map[String, Color] =
43386
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   160
    Map(
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   161
      Isabelle_Markup.STRING -> get_color("black"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   162
      Isabelle_Markup.ALTSTRING -> get_color("black"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   163
      Isabelle_Markup.VERBATIM -> get_color("black"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   164
      Isabelle_Markup.LITERAL -> keyword1_color,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   165
      Isabelle_Markup.DELIMITER -> get_color("black"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   166
      Isabelle_Markup.TFREE -> get_color("#A020F0"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   167
      Isabelle_Markup.TVAR -> get_color("#A020F0"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   168
      Isabelle_Markup.FREE -> get_color("blue"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   169
      Isabelle_Markup.SKOLEM -> get_color("#D2691E"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   170
      Isabelle_Markup.BOUND -> get_color("green"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   171
      Isabelle_Markup.VAR -> get_color("#00009B"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   172
      Isabelle_Markup.INNER_STRING -> get_color("#D2691E"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   173
      Isabelle_Markup.INNER_COMMENT -> get_color("#8B0000"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   174
      Isabelle_Markup.DYNAMIC_FACT -> get_color("#7BA428"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   175
      Isabelle_Markup.ML_KEYWORD -> keyword1_color,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   176
      Isabelle_Markup.ML_DELIMITER -> get_color("black"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   177
      Isabelle_Markup.ML_NUMERAL -> get_color("red"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   178
      Isabelle_Markup.ML_CHAR -> get_color("#D2691E"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   179
      Isabelle_Markup.ML_STRING -> get_color("#D2691E"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   180
      Isabelle_Markup.ML_COMMENT -> get_color("#8B0000"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   181
      Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   182
      Isabelle_Markup.ANTIQ -> get_color("blue"))
43386
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   183
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   184
  private val text_color_elements = Set.empty[String] ++ text_colors.keys
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   185
46197
e4da482283ef tuned text_color: cumulate with explicit default color;
wenzelm
parents: 46196
diff changeset
   186
  def text_color(snapshot: Document.Snapshot, range: Text.Range, color: Color)
e4da482283ef tuned text_color: cumulate with explicit default color;
wenzelm
parents: 46196
diff changeset
   187
      : Stream[Text.Info[Color]] =
e4da482283ef tuned text_color: cumulate with explicit default color;
wenzelm
parents: 46196
diff changeset
   188
    snapshot.cumulate_markup(range, color, Some(text_color_elements),
45468
33e946d3f449 tuned signature;
wenzelm
parents: 45467
diff changeset
   189
      {
46197
e4da482283ef tuned text_color: cumulate with explicit default color;
wenzelm
parents: 46196
diff changeset
   190
        case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
45474
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45468
diff changeset
   191
        if text_colors.isDefinedAt(m) => text_colors(m)
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   192
      })
43376
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43282
diff changeset
   193
43431
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   194
  private val tooltips: Map[String, String] =
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   195
    Map(
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   196
      Isabelle_Markup.SORT -> "sort",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   197
      Isabelle_Markup.TYP -> "type",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   198
      Isabelle_Markup.TERM -> "term",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   199
      Isabelle_Markup.PROP -> "proposition",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   200
      Isabelle_Markup.TOKEN_RANGE -> "inner syntax token",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   201
      Isabelle_Markup.FREE -> "free variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   202
      Isabelle_Markup.SKOLEM -> "skolem variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   203
      Isabelle_Markup.BOUND -> "bound variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   204
      Isabelle_Markup.VAR -> "schematic variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   205
      Isabelle_Markup.TFREE -> "free type variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   206
      Isabelle_Markup.TVAR -> "schematic type variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   207
      Isabelle_Markup.ML_SOURCE -> "ML source",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   208
      Isabelle_Markup.DOC_SOURCE -> "document source")
43431
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   209
45445
41e641a870de pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents: 44866
diff changeset
   210
  private def string_of_typing(kind: String, body: XML.Body): String =
41e641a870de pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents: 44866
diff changeset
   211
    Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
41e641a870de pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents: 44866
diff changeset
   212
      margin = Isabelle.Int_Property("tooltip-margin"))
41e641a870de pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents: 44866
diff changeset
   213
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   214
  def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   215
  {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   216
    val tip1 =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   217
      snapshot.select_markup(range,
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   218
        Some(Set(Isabelle_Markup.ENTITY, Isabelle_Markup.ML_TYPING) ++ tooltips.keys),
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   219
        {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   220
          case Text.Info(_, XML.Elem(Isabelle_Markup.Entity(kind, name), _)) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   221
            kind + " " + quote(name)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   222
          case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body)) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   223
            string_of_typing("ML:", body)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   224
          case Text.Info(_, XML.Elem(Markup(name, _), _))
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   225
          if tooltips.isDefinedAt(name) => tooltips(name)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   226
        })
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   227
    val tip2 =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   228
      snapshot.select_markup(range, Some(Set(Isabelle_Markup.TYPING)),
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   229
        {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   230
          case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body)) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   231
            string_of_typing("::", body)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   232
        })
42302
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   233
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   234
    val tips =
46198
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   235
      (tip1 match { case Text.Info(_, text) #:: _ => List(text) case _ => Nil }) :::
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   236
      (tip2 match { case Text.Info(_, text) #:: _ => List(text) case _ => Nil })
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   237
46196
805de058722b added cat_lines convenience;
wenzelm
parents: 46178
diff changeset
   238
    if (tips.isEmpty) None else Some(cat_lines(tips))
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   239
  }
45460
dcd02d1a25d7 more tooltip content;
wenzelm
parents: 45454
diff changeset
   240
42302
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   241
  private val subexp_include =
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   242
    Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   243
      Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   244
      Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   245
      Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   246
      Isabelle_Markup.DOC_SOURCE)
42302
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   247
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   248
  def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[(Text.Range, Color)] =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   249
  {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   250
    snapshot.select_markup(range, Some(subexp_include),
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   251
        {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   252
          case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   253
            (range, subexp_color)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   254
        }) match {
46198
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   255
      case Text.Info(_, (range, color)) #:: _ => Some((snapshot.convert(range), color))
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   256
      case _ => None
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   257
    }
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   258
  }
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   259
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   260
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   261
  /* token markup -- text styles */
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   262
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   263
  private val command_style: Map[String, Byte] =
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   264
  {
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   265
    import JEditToken._
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   266
    Map[String, Byte](
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   267
      Keyword.THY_END -> KEYWORD2,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   268
      Keyword.THY_SCRIPT -> LABEL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   269
      Keyword.PRF_SCRIPT -> LABEL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   270
      Keyword.PRF_ASM -> KEYWORD3,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   271
      Keyword.PRF_ASM_GOAL -> KEYWORD3
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   272
    ).withDefaultValue(KEYWORD1)
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   273
  }
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   274
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   275
  private val token_style: Map[Token.Kind.Value, Byte] =
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   276
  {
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   277
    import JEditToken._
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   278
    Map[Token.Kind.Value, Byte](
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   279
      Token.Kind.KEYWORD -> KEYWORD2,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   280
      Token.Kind.IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   281
      Token.Kind.LONG_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   282
      Token.Kind.SYM_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   283
      Token.Kind.VAR -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   284
      Token.Kind.TYPE_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   285
      Token.Kind.TYPE_VAR -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   286
      Token.Kind.NAT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   287
      Token.Kind.FLOAT -> NULL,
43431
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   288
      Token.Kind.STRING -> LITERAL1,
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   289
      Token.Kind.ALT_STRING -> LITERAL2,
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   290
      Token.Kind.VERBATIM -> COMMENT3,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   291
      Token.Kind.SPACE -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   292
      Token.Kind.COMMENT -> COMMENT1,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   293
      Token.Kind.UNPARSED -> INVALID
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   294
    ).withDefaultValue(NULL)
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   295
  }
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   296
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   297
  def token_markup(syntax: Outer_Syntax, token: Token): Byte =
43430
1ed88ddf1268 more uniform treatment of "keyword" vs. "operator";
wenzelm
parents: 43418
diff changeset
   298
    if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
1ed88ddf1268 more uniform treatment of "keyword" vs. "operator";
wenzelm
parents: 43418
diff changeset
   299
    else if (token.is_operator) JEditToken.OPERATOR
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   300
    else token_style(token.kind)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   301
}