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