src/Tools/jEdit/src/jedit/isabelle_markup.scala
author wenzelm
Thu, 04 Nov 2010 10:58:03 +0100
changeset 40338 e2f03de2b3c7
parent 39740 0294948ba962
child 40339 088e5adca5ad
permissions -rw-r--r--
clarified tooltips: message output by default, extra info via control/command;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/jedit/isabelle_markup.scala
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
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
    14
import org.gjt.sp.jedit.syntax.Token
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    15
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
object Isabelle_Markup
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    18
{
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    19
  /* physical rendering */
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    20
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    21
  val outdated_color = new Color(240, 240, 240)
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    22
  val unfinished_color = new Color(255, 228, 225)
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    23
39690
6c6164b37fef some attempts to improve visual appearance of bad text;
wenzelm
parents: 39512
diff changeset
    24
  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
    25
  val regular_color = new Color(192, 192, 192)
39692
b88a6bc371de tuned warning_color;
wenzelm
parents: 39691
diff changeset
    26
  val warning_color = new Color(255, 140, 0)
39691
4ce5f79df87a tuned error_color;
wenzelm
parents: 39690
diff changeset
    27
  val error_color = new Color(178, 34, 34)
39690
6c6164b37fef some attempts to improve visual appearance of bad text;
wenzelm
parents: 39512
diff changeset
    28
  val bad_color = new Color(255, 106, 106, 100)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    29
39181
2257eded8323 Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents: 39179
diff changeset
    30
  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
    31
  {
2257eded8323 Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents: 39179
diff changeset
    32
    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
    33
  }
39241
e9a442606db3 Isabelle.load_icon with some sanity checks;
wenzelm
parents: 39181
diff changeset
    34
  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
    35
  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
    36
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    37
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    38
  /* command status */
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    39
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    40
  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
    41
  {
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    42
    val state = snapshot.state(command)
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    43
    if (snapshot.is_outdated) Some(outdated_color)
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    44
    else
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    45
      Isar_Document.command_status(state.status) match {
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    46
        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
    47
        case Isar_Document.Unprocessed => Some(unfinished_color)
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    48
        case _ => None
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    49
      }
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
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    52
  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
    53
  {
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    54
    val state = snapshot.state(command)
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    55
    if (snapshot.is_outdated) None
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    56
    else
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    57
      Isar_Document.command_status(state.status) match {
39512
31290f54be19 Isabelle_Markup.overview_color: indicate error / warning messages;
wenzelm
parents: 39244
diff changeset
    58
        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
    59
        case Isar_Document.Unprocessed => Some(unfinished_color)
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    60
        case Isar_Document.Failed => Some(error_color)
39512
31290f54be19 Isabelle_Markup.overview_color: indicate error / warning messages;
wenzelm
parents: 39244
diff changeset
    61
        case Isar_Document.Finished =>
31290f54be19 Isabelle_Markup.overview_color: indicate error / warning messages;
wenzelm
parents: 39244
diff changeset
    62
          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
    63
          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
    64
          else None
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    65
      }
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    66
  }
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    67
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    68
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    69
  /* markup selectors */
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    70
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    71
  private val subexp_include =
39704
b4e0bddc9e4c some markup for inner syntax tokens;
wenzelm
parents: 39700
diff changeset
    72
    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    73
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    74
  val subexp: Markup_Tree.Select[(Text.Range, Color)] =
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
    case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    77
      (range, Color.black)
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
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 =>
e2f03de2b3c7 clarified tooltips: message output by default, extra info via control/command;
wenzelm
parents: 39740
diff changeset
    91
      Pretty.string_of(List(msg), margin = 40)
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
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   103
  }
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   104
39700
fa55cf2c1ae4 more precise treatment of backgrounds vs. rectangles;
wenzelm
parents: 39692
diff changeset
   105
  val background2: Markup_Tree.Select[Color] =
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   106
  {
39690
6c6164b37fef some attempts to improve visual appearance of bad text;
wenzelm
parents: 39512
diff changeset
   107
    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
   108
  }
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
  val tooltip: Markup_Tree.Select[String] =
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   111
  {
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   112
    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
39244
d31c03a34f76 Isabelle_Markup.tooltip: explicit indication of ML;
wenzelm
parents: 39241
diff changeset
   113
      Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)), margin = 40)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   114
    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
   115
    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
   116
    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
   117
    case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
39704
b4e0bddc9e4c some markup for inner syntax tokens;
wenzelm
parents: 39700
diff changeset
   118
    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => "inner syntax token"
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   119
  }
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   120
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   121
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   122
  /* token markup -- text styles */
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   123
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   124
  private val command_style: Map[String, Byte] =
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   125
  {
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   126
    import Token._
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   127
    Map[String, Byte](
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   128
      Keyword.THY_END -> KEYWORD2,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   129
      Keyword.THY_SCRIPT -> LABEL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   130
      Keyword.PRF_SCRIPT -> LABEL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   131
      Keyword.PRF_ASM -> KEYWORD3,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   132
      Keyword.PRF_ASM_GOAL -> KEYWORD3
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   133
    ).withDefaultValue(KEYWORD1)
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   134
  }
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   135
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   136
  private val token_style: Map[String, Byte] =
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   137
  {
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   138
    import Token._
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   139
    Map[String, Byte](
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   140
      // logical entities
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   141
      Markup.TCLASS -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   142
      Markup.TYCON -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   143
      Markup.FIXED_DECL -> FUNCTION,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   144
      Markup.FIXED -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   145
      Markup.CONST_DECL -> FUNCTION,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   146
      Markup.CONST -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   147
      Markup.FACT_DECL -> FUNCTION,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   148
      Markup.FACT -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   149
      Markup.DYNAMIC_FACT -> LABEL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   150
      Markup.LOCAL_FACT_DECL -> FUNCTION,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   151
      Markup.LOCAL_FACT -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   152
      // inner syntax
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   153
      Markup.TFREE -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   154
      Markup.FREE -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   155
      Markup.TVAR -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   156
      Markup.SKOLEM -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   157
      Markup.BOUND -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   158
      Markup.VAR -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   159
      Markup.NUM -> DIGIT,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   160
      Markup.FLOAT -> DIGIT,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   161
      Markup.XNUM -> DIGIT,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   162
      Markup.XSTR -> LITERAL4,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   163
      Markup.LITERAL -> OPERATOR,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   164
      Markup.INNER_COMMENT -> COMMENT1,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   165
      Markup.SORT -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   166
      Markup.TYP -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   167
      Markup.TERM -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   168
      Markup.PROP -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   169
      Markup.ATTRIBUTE -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   170
      Markup.METHOD -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   171
      // ML syntax
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   172
      Markup.ML_KEYWORD -> KEYWORD1,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   173
      Markup.ML_DELIMITER -> OPERATOR,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   174
      Markup.ML_IDENT -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   175
      Markup.ML_TVAR -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   176
      Markup.ML_NUMERAL -> DIGIT,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   177
      Markup.ML_CHAR -> LITERAL1,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   178
      Markup.ML_STRING -> LITERAL1,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   179
      Markup.ML_COMMENT -> COMMENT1,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   180
      Markup.ML_MALFORMED -> INVALID,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   181
      // embedded source text
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   182
      Markup.ML_SOURCE -> COMMENT3,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   183
      Markup.DOC_SOURCE -> COMMENT3,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   184
      Markup.ANTIQ -> COMMENT4,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   185
      Markup.ML_ANTIQ -> COMMENT4,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   186
      Markup.DOC_ANTIQ -> COMMENT4,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   187
      // outer syntax
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   188
      Markup.KEYWORD -> KEYWORD2,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   189
      Markup.OPERATOR -> OPERATOR,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   190
      Markup.COMMAND -> KEYWORD1,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   191
      Markup.IDENT -> NULL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   192
      Markup.VERBATIM -> COMMENT3,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   193
      Markup.COMMENT -> COMMENT1,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   194
      Markup.CONTROL -> COMMENT3,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   195
      Markup.MALFORMED -> INVALID,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   196
      Markup.STRING -> LITERAL3,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   197
      Markup.ALTSTRING -> LITERAL1
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   198
    ).withDefaultValue(NULL)
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   199
  }
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   200
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   201
  def tokens(syntax: Outer_Syntax): Markup_Tree.Select[Byte] =
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   202
  {
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   203
    case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   204
    if syntax.keyword_kind(name).isDefined => command_style(syntax.keyword_kind(name).get)
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   205
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   206
    case Text.Info(_, XML.Elem(Markup(name, _), _))
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   207
    if token_style(name) != Token.NULL => token_style(name)
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   208
  }
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   209
}