src/Tools/jEdit/src/isabelle_markup.scala
author wenzelm
Thu, 16 Jun 2011 22:05:40 +0200
changeset 43414 f0770743b7ec
parent 43394 47e60a27a496
child 43418 c69e9fbb81a8
permissions -rw-r--r--
static token markup, based on outer syntax only; eliminated obsolete buffer.propertiesChanged (expensive due to remarking of full buffer etc.);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43282
5d294220ca43 moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents: 42492
diff changeset
     1
/*  Title:      Tools/jEdit/src/isabelle_markup.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
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    17
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    18
object Isabelle_Markup
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    19
{
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    20
  /* physical rendering */
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    21
43377
ba199d75bc7e more accurate CSS colors;
wenzelm
parents: 43376
diff changeset
    22
  // see http://www.w3schools.com/css/css_colornames.asp
ba199d75bc7e more accurate CSS colors;
wenzelm
parents: 43376
diff changeset
    23
43386
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
    24
  def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
    25
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    26
  val outdated_color = new Color(240, 240, 240)
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    27
  val unfinished_color = new Color(255, 228, 225)
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    28
39690
6c6164b37fef some attempts to improve visual appearance of bad text;
wenzelm
parents: 39512
diff changeset
    29
  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
    30
  val regular_color = new Color(192, 192, 192)
39692
b88a6bc371de tuned warning_color;
wenzelm
parents: 39691
diff changeset
    31
  val warning_color = new Color(255, 140, 0)
39691
4ce5f79df87a tuned error_color;
wenzelm
parents: 39690
diff changeset
    32
  val error_color = new Color(178, 34, 34)
39690
6c6164b37fef some attempts to improve visual appearance of bad text;
wenzelm
parents: 39512
diff changeset
    33
  val bad_color = new Color(255, 106, 106, 100)
42171
620343510c88 visualize skolem and hilite (undeclared frees);
wenzelm
parents: 42136
diff changeset
    34
  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
    35
43388
34492601c0e0 tuned colors;
wenzelm
parents: 43386
diff changeset
    36
  val keyword1_color = get_color("#006699")
34492601c0e0 tuned colors;
wenzelm
parents: 43386
diff changeset
    37
  val keyword2_color = get_color("#009966")
34492601c0e0 tuned colors;
wenzelm
parents: 43386
diff changeset
    38
39181
2257eded8323 Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents: 39179
diff changeset
    39
  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
    40
  {
2257eded8323 Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents: 39179
diff changeset
    41
    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
    42
  }
39241
e9a442606db3 Isabelle.load_icon with some sanity checks;
wenzelm
parents: 39181
diff changeset
    43
  val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-warning.png"))
e9a442606db3 Isabelle.load_icon with some sanity checks;
wenzelm
parents: 39181
diff changeset
    44
  val error_icon = new Icon(2, 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
    45
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    46
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    47
  /* command status */
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    48
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    49
  def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    50
  {
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    51
    val state = snapshot.state(command)
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    52
    if (snapshot.is_outdated) Some(outdated_color)
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    53
    else
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    54
      Isar_Document.command_status(state.status) match {
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    55
        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    56
        case Isar_Document.Unprocessed => Some(unfinished_color)
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    57
        case _ => None
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
  }
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    60
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    61
  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
    62
  {
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    63
    val state = snapshot.state(command)
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    64
    if (snapshot.is_outdated) None
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    65
    else
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    66
      Isar_Document.command_status(state.status) match {
39512
31290f54be19 Isabelle_Markup.overview_color: indicate error / warning messages;
wenzelm
parents: 39244
diff changeset
    67
        case Isar_Document.Forked(i) => if (i > 0) Some(unfinished_color) else None
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    68
        case Isar_Document.Unprocessed => Some(unfinished_color)
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    69
        case Isar_Document.Failed => Some(error_color)
39512
31290f54be19 Isabelle_Markup.overview_color: indicate error / warning messages;
wenzelm
parents: 39244
diff changeset
    70
        case Isar_Document.Finished =>
31290f54be19 Isabelle_Markup.overview_color: indicate error / warning messages;
wenzelm
parents: 39244
diff changeset
    71
          if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color)
31290f54be19 Isabelle_Markup.overview_color: indicate error / warning messages;
wenzelm
parents: 39244
diff changeset
    72
          else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color)
31290f54be19 Isabelle_Markup.overview_color: indicate error / warning messages;
wenzelm
parents: 39244
diff changeset
    73
          else None
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    74
      }
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    75
  }
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
  /* markup selectors */
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    79
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    80
  val message: Markup_Tree.Select[Color] =
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    81
  {
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    82
    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    83
    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    84
    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    85
  }
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    86
40338
e2f03de2b3c7 clarified tooltips: message output by default, extra info via control/command;
wenzelm
parents: 39740
diff changeset
    87
  val popup: Markup_Tree.Select[String] =
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39704
diff changeset
    88
  {
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39704
diff changeset
    89
    case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _))
40338
e2f03de2b3c7 clarified tooltips: message output by default, extra info via control/command;
wenzelm
parents: 39740
diff changeset
    90
    if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
40339
088e5adca5ad added property "tooltip-margin";
wenzelm
parents: 40338
diff changeset
    91
      Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39704
diff changeset
    92
  }
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39704
diff changeset
    93
39181
2257eded8323 Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents: 39179
diff changeset
    94
  val gutter_message: Markup_Tree.Select[Icon] =
2257eded8323 Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents: 39179
diff changeset
    95
  {
2257eded8323 Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents: 39179
diff changeset
    96
    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
2257eded8323 Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents: 39179
diff changeset
    97
    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
2257eded8323 Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents: 39179
diff changeset
    98
  }
2257eded8323 Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents: 39179
diff changeset
    99
39700
fa55cf2c1ae4 more precise treatment of backgrounds vs. rectangles;
wenzelm
parents: 39692
diff changeset
   100
  val background1: Markup_Tree.Select[Color] =
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   101
  {
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   102
    case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
42171
620343510c88 visualize skolem and hilite (undeclared frees);
wenzelm
parents: 42136
diff changeset
   103
    case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   104
  }
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   105
39700
fa55cf2c1ae4 more precise treatment of backgrounds vs. rectangles;
wenzelm
parents: 39692
diff changeset
   106
  val background2: Markup_Tree.Select[Color] =
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   107
  {
39690
6c6164b37fef some attempts to improve visual appearance of bad text;
wenzelm
parents: 39512
diff changeset
   108
    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   109
  }
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   110
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   111
  /* FIXME update
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   112
      Markup.ML_SOURCE -> COMMENT3,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   113
      Markup.DOC_SOURCE -> COMMENT3,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   114
      Markup.ANTIQ -> COMMENT4,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   115
      Markup.ML_ANTIQ -> COMMENT4,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   116
      Markup.DOC_ANTIQ -> COMMENT4,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   117
  */
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   118
43386
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   119
  private val foreground_colors: Map[String, Color] =
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   120
    Map(
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   121
      Markup.TCLASS -> get_color("red"),
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   122
      Markup.TFREE -> get_color("#A020F0"),
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   123
      Markup.TVAR -> get_color("#A020F0"),
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   124
      Markup.CONST -> get_color("dimgrey"),
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   125
      Markup.FREE -> get_color("blue"),
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   126
      Markup.SKOLEM -> get_color("#D2691E"),
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   127
      Markup.BOUND -> get_color("green"),
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   128
      Markup.VAR -> get_color("#00009B"),
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   129
      Markup.INNER_STRING -> get_color("#D2691E"),
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   130
      Markup.INNER_COMMENT -> get_color("#8B0000"),
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   131
      Markup.DYNAMIC_FACT -> get_color("yellowgreen"),
43388
34492601c0e0 tuned colors;
wenzelm
parents: 43386
diff changeset
   132
      Markup.LITERAL -> keyword1_color,
34492601c0e0 tuned colors;
wenzelm
parents: 43386
diff changeset
   133
      Markup.ML_KEYWORD -> keyword1_color,
43386
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   134
      Markup.ML_DELIMITER -> get_color("black"),
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   135
      Markup.ML_NUMERAL -> get_color("red"),
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   136
      Markup.ML_CHAR -> get_color("#D2691E"),
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   137
      Markup.ML_STRING -> get_color("#D2691E"),
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   138
      Markup.ML_COMMENT -> get_color("#8B0000"),
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   139
      Markup.ML_MALFORMED -> get_color("#FF6A6A")
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   140
    )
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   141
43376
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43282
diff changeset
   142
  val foreground: Markup_Tree.Select[Color] =
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43282
diff changeset
   143
  {
43386
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   144
    case Text.Info(_, XML.Elem(Markup(m, _), _))
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   145
    if foreground_colors.isDefinedAt(m) => foreground_colors(m)
43376
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43282
diff changeset
   146
  }
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43282
diff changeset
   147
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   148
  val tooltip: Markup_Tree.Select[String] =
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   149
  {
42283
25d9d836ed9c tuned presentation;
wenzelm
parents: 42203
diff changeset
   150
    case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\""
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   151
    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
40339
088e5adca5ad added property "tooltip-margin";
wenzelm
parents: 40338
diff changeset
   152
      Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
088e5adca5ad added property "tooltip-margin";
wenzelm
parents: 40338
diff changeset
   153
        margin = Isabelle.Int_Property("tooltip-margin"))
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   154
    case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   155
    case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   156
    case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   157
    case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
39704
b4e0bddc9e4c some markup for inner syntax tokens;
wenzelm
parents: 39700
diff changeset
   158
    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => "inner syntax token"
42203
9c9c97a5040d show more tooltip/sub-expression markup;
wenzelm
parents: 42202
diff changeset
   159
    case Text.Info(_, XML.Elem(Markup(Markup.FREE, _), _)) => "free variable (globally fixed)"
9c9c97a5040d show more tooltip/sub-expression markup;
wenzelm
parents: 42202
diff changeset
   160
    case Text.Info(_, XML.Elem(Markup(Markup.SKOLEM, _), _)) => "skolem variable (locally fixed)"
9c9c97a5040d show more tooltip/sub-expression markup;
wenzelm
parents: 42202
diff changeset
   161
    case Text.Info(_, XML.Elem(Markup(Markup.BOUND, _), _)) => "bound variable (internally fixed)"
9c9c97a5040d show more tooltip/sub-expression markup;
wenzelm
parents: 42202
diff changeset
   162
    case Text.Info(_, XML.Elem(Markup(Markup.VAR, _), _)) => "schematic variable"
42302
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   163
    case Text.Info(_, XML.Elem(Markup(Markup.TFREE, _), _)) => "free type variable"
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   164
    case Text.Info(_, XML.Elem(Markup(Markup.TVAR, _), _)) => "schematic type variable"
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   165
  }
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   166
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   167
  private val subexp_include =
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   168
    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   169
      Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   170
      Markup.TFREE, Markup.TVAR)
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   171
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   172
  val subexp: Markup_Tree.Select[(Text.Range, Color)] =
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   173
  {
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   174
    case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   175
      (range, Color.black)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   176
  }
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   177
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   178
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   179
  /* token markup -- text styles */
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   180
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   181
  private val command_style: Map[String, Byte] =
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   182
  {
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   183
    import JEditToken._
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   184
    Map[String, Byte](
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   185
      Keyword.THY_END -> KEYWORD2,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   186
      Keyword.THY_SCRIPT -> LABEL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   187
      Keyword.PRF_SCRIPT -> LABEL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   188
      Keyword.PRF_ASM -> KEYWORD3,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   189
      Keyword.PRF_ASM_GOAL -> KEYWORD3
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   190
    ).withDefaultValue(KEYWORD1)
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   191
  }
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   192
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   193
  private val token_style: Map[Token.Kind.Value, Byte] =
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   194
  {
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   195
    import JEditToken._
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   196
    Map[Token.Kind.Value, Byte](
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   197
      Token.Kind.KEYWORD -> KEYWORD2,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   198
      Token.Kind.IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   199
      Token.Kind.LONG_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   200
      Token.Kind.SYM_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   201
      Token.Kind.VAR -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   202
      Token.Kind.TYPE_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   203
      Token.Kind.TYPE_VAR -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   204
      Token.Kind.NAT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   205
      Token.Kind.FLOAT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   206
      Token.Kind.STRING -> LITERAL3,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   207
      Token.Kind.ALT_STRING -> LITERAL1,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   208
      Token.Kind.VERBATIM -> COMMENT3,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   209
      Token.Kind.SPACE -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   210
      Token.Kind.COMMENT -> COMMENT1,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   211
      Token.Kind.UNPARSED -> INVALID
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   212
    ).withDefaultValue(NULL)
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   213
  }
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   214
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   215
  def token_markup(syntax: Outer_Syntax, token: Token): Byte =
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   216
    if (token.is_command)
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   217
      command_style(syntax.keyword_kind(token.content).getOrElse(""))
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   218
    else token_style(token.kind)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   219
}