src/Tools/jEdit/src/isabelle_rendering.scala
author wenzelm
Thu, 12 Jan 2012 21:50:00 +0100
changeset 46198 cd040c5772de
parent 46197 e4da482283ef
child 46199 9d2273d50f4f
permissions -rw-r--r--
improved select_markup: include filtering of defined results;
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] =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
    91
    snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
    92
      Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45460
diff changeset
    93
      {
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
    94
        case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
    95
        if markup == Isabelle_Markup.WRITELN ||
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
    96
            markup == Isabelle_Markup.WARNING ||
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
    97
            markup == Isabelle_Markup.ERROR =>
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45460
diff changeset
    98
          msgs + (serial ->
3f290b6288cf tuned signature;
wenzelm
parents: 45460
diff changeset
    99
            Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   100
      }) match {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   101
        case Text.Info(_, msgs) #:: _ if !msgs.isEmpty =>
46196
805de058722b added cat_lines convenience;
wenzelm
parents: 46178
diff changeset
   102
          Some(cat_lines(msgs.iterator.map(_._2)))
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   103
        case _ => None
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
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] =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   107
  {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   108
    val icons =
46198
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   109
     (snapshot.select_markup(range,
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   110
        Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   111
        {
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   112
          case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body)) =>
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   113
            body match {
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   114
              case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => legacy_icon
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   115
              case _ => warning_icon
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   116
            }
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   117
          case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   118
        }).map { case Text.Info(_, icon) => icon }).toList.sortWith(_ >= _)
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   119
    icons match {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   120
      case icon :: _ => Some(icon)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   121
      case Nil => None
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   122
    }
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   123
  }
39181
2257eded8323 Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents: 39179
diff changeset
   124
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   125
  def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   126
  {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   127
    for {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   128
      Text.Info(r, result) <-
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   129
        snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   130
          range, (Some(Protocol.Status()), None),
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   131
          Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE),
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
            case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   134
            if (Protocol.command_status_markup(markup.name)) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   135
              (Some(Protocol.command_status(status, markup)), color)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   136
            case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   137
              (None, Some(bad_color))
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   138
            case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   139
              (None, Some(hilite_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
      color <-
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   142
        (result match {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   143
          case (Some(status), _) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   144
            if (status.is_running) Some(running1_color)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   145
            else if (status.is_unprocessed) Some(unprocessed1_color)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   146
            else None
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   147
          case (_, opt_color) => opt_color
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   148
        })
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   149
    } yield Text.Info(r, color)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   150
  }
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   151
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   152
  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
   153
    snapshot.select_markup(range,
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   154
      Some(Set(Isabelle_Markup.TOKEN_RANGE)),
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   155
      {
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   156
        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
   157
      })
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   158
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   159
  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
   160
    snapshot.select_markup(range,
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   161
      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
   162
      {
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   163
        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
   164
        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
   165
        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
   166
      })
44545
3c40007aa031 transparent foreground color for quoted entities;
wenzelm
parents: 44181
diff changeset
   167
43434
2fd41645813d tuned signature;
wenzelm
parents: 43432
diff changeset
   168
  private val text_colors: Map[String, Color] =
43386
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   169
    Map(
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   170
      Isabelle_Markup.STRING -> get_color("black"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   171
      Isabelle_Markup.ALTSTRING -> get_color("black"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   172
      Isabelle_Markup.VERBATIM -> get_color("black"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   173
      Isabelle_Markup.LITERAL -> keyword1_color,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   174
      Isabelle_Markup.DELIMITER -> get_color("black"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   175
      Isabelle_Markup.TFREE -> get_color("#A020F0"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   176
      Isabelle_Markup.TVAR -> get_color("#A020F0"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   177
      Isabelle_Markup.FREE -> get_color("blue"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   178
      Isabelle_Markup.SKOLEM -> get_color("#D2691E"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   179
      Isabelle_Markup.BOUND -> get_color("green"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   180
      Isabelle_Markup.VAR -> get_color("#00009B"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   181
      Isabelle_Markup.INNER_STRING -> get_color("#D2691E"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   182
      Isabelle_Markup.INNER_COMMENT -> get_color("#8B0000"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   183
      Isabelle_Markup.DYNAMIC_FACT -> get_color("#7BA428"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   184
      Isabelle_Markup.ML_KEYWORD -> keyword1_color,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   185
      Isabelle_Markup.ML_DELIMITER -> get_color("black"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   186
      Isabelle_Markup.ML_NUMERAL -> get_color("red"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   187
      Isabelle_Markup.ML_CHAR -> get_color("#D2691E"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   188
      Isabelle_Markup.ML_STRING -> get_color("#D2691E"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   189
      Isabelle_Markup.ML_COMMENT -> get_color("#8B0000"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   190
      Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   191
      Isabelle_Markup.ANTIQ -> get_color("blue"))
43386
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   192
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   193
  private val text_color_elements = Set.empty[String] ++ text_colors.keys
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   194
46197
e4da482283ef tuned text_color: cumulate with explicit default color;
wenzelm
parents: 46196
diff changeset
   195
  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
   196
      : Stream[Text.Info[Color]] =
e4da482283ef tuned text_color: cumulate with explicit default color;
wenzelm
parents: 46196
diff changeset
   197
    snapshot.cumulate_markup(range, color, Some(text_color_elements),
45468
33e946d3f449 tuned signature;
wenzelm
parents: 45467
diff changeset
   198
      {
46197
e4da482283ef tuned text_color: cumulate with explicit default color;
wenzelm
parents: 46196
diff changeset
   199
        case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
45474
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45468
diff changeset
   200
        if text_colors.isDefinedAt(m) => text_colors(m)
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   201
      })
43376
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43282
diff changeset
   202
43431
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   203
  private val tooltips: Map[String, String] =
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   204
    Map(
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   205
      Isabelle_Markup.SORT -> "sort",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   206
      Isabelle_Markup.TYP -> "type",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   207
      Isabelle_Markup.TERM -> "term",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   208
      Isabelle_Markup.PROP -> "proposition",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   209
      Isabelle_Markup.TOKEN_RANGE -> "inner syntax token",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   210
      Isabelle_Markup.FREE -> "free variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   211
      Isabelle_Markup.SKOLEM -> "skolem variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   212
      Isabelle_Markup.BOUND -> "bound variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   213
      Isabelle_Markup.VAR -> "schematic variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   214
      Isabelle_Markup.TFREE -> "free type variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   215
      Isabelle_Markup.TVAR -> "schematic type variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   216
      Isabelle_Markup.ML_SOURCE -> "ML source",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   217
      Isabelle_Markup.DOC_SOURCE -> "document source")
43431
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   218
45445
41e641a870de pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents: 44866
diff changeset
   219
  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
   220
    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
   221
      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
   222
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   223
  def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   224
  {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   225
    val tip1 =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   226
      snapshot.select_markup(range,
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   227
        Some(Set(Isabelle_Markup.ENTITY, Isabelle_Markup.ML_TYPING) ++ tooltips.keys),
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   228
        {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   229
          case Text.Info(_, XML.Elem(Isabelle_Markup.Entity(kind, name), _)) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   230
            kind + " " + quote(name)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   231
          case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body)) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   232
            string_of_typing("ML:", body)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   233
          case Text.Info(_, XML.Elem(Markup(name, _), _))
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   234
          if tooltips.isDefinedAt(name) => tooltips(name)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   235
        })
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   236
    val tip2 =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   237
      snapshot.select_markup(range, Some(Set(Isabelle_Markup.TYPING)),
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   238
        {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   239
          case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body)) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   240
            string_of_typing("::", body)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   241
        })
42302
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   242
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   243
    val tips =
46198
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   244
      (tip1 match { case Text.Info(_, text) #:: _ => List(text) case _ => Nil }) :::
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   245
      (tip2 match { case Text.Info(_, text) #:: _ => List(text) case _ => Nil })
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   246
46196
805de058722b added cat_lines convenience;
wenzelm
parents: 46178
diff changeset
   247
    if (tips.isEmpty) None else Some(cat_lines(tips))
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   248
  }
45460
dcd02d1a25d7 more tooltip content;
wenzelm
parents: 45454
diff changeset
   249
42302
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   250
  private val subexp_include =
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   251
    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
   252
      Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   253
      Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   254
      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
   255
      Isabelle_Markup.DOC_SOURCE)
42302
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   256
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   257
  def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[(Text.Range, Color)] =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   258
  {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   259
    snapshot.select_markup(range, Some(subexp_include),
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   260
        {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   261
          case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   262
            (range, subexp_color)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   263
        }) match {
46198
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   264
      case Text.Info(_, (range, color)) #:: _ => Some((snapshot.convert(range), color))
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   265
      case _ => None
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   266
    }
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   267
  }
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   268
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   269
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   270
  /* token markup -- text styles */
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   271
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   272
  private val command_style: Map[String, Byte] =
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   273
  {
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   274
    import JEditToken._
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   275
    Map[String, Byte](
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   276
      Keyword.THY_END -> KEYWORD2,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   277
      Keyword.THY_SCRIPT -> LABEL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   278
      Keyword.PRF_SCRIPT -> LABEL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   279
      Keyword.PRF_ASM -> KEYWORD3,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   280
      Keyword.PRF_ASM_GOAL -> KEYWORD3
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   281
    ).withDefaultValue(KEYWORD1)
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   282
  }
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   283
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   284
  private val token_style: Map[Token.Kind.Value, Byte] =
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   285
  {
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   286
    import JEditToken._
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   287
    Map[Token.Kind.Value, Byte](
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   288
      Token.Kind.KEYWORD -> KEYWORD2,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   289
      Token.Kind.IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   290
      Token.Kind.LONG_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   291
      Token.Kind.SYM_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   292
      Token.Kind.VAR -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   293
      Token.Kind.TYPE_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   294
      Token.Kind.TYPE_VAR -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   295
      Token.Kind.NAT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   296
      Token.Kind.FLOAT -> NULL,
43431
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   297
      Token.Kind.STRING -> LITERAL1,
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   298
      Token.Kind.ALT_STRING -> LITERAL2,
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   299
      Token.Kind.VERBATIM -> COMMENT3,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   300
      Token.Kind.SPACE -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   301
      Token.Kind.COMMENT -> COMMENT1,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   302
      Token.Kind.UNPARSED -> INVALID
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   303
    ).withDefaultValue(NULL)
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   304
  }
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   305
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   306
  def token_markup(syntax: Outer_Syntax, token: Token): Byte =
43430
1ed88ddf1268 more uniform treatment of "keyword" vs. "operator";
wenzelm
parents: 43418
diff changeset
   307
    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
   308
    else if (token.is_operator) JEditToken.OPERATOR
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   309
    else token_style(token.kind)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   310
}