src/Tools/jEdit/src/isabelle_markup.scala
author wenzelm
Sat Jun 18 12:13:42 2011 +0200 (2011-06-18)
changeset 43431 f3d5cecfecdc
parent 43430 1ed88ddf1268
child 43432 224006e5ac46
permissions -rw-r--r--
tuned markup;
wenzelm@43282
     1
/*  Title:      Tools/jEdit/src/isabelle_markup.scala
wenzelm@39178
     2
    Author:     Makarius
wenzelm@39178
     3
wenzelm@39178
     4
Isabelle specific physical rendering and markup selection.
wenzelm@39178
     5
*/
wenzelm@39178
     6
wenzelm@39178
     7
package isabelle.jedit
wenzelm@39178
     8
wenzelm@39178
     9
wenzelm@39178
    10
import isabelle._
wenzelm@39178
    11
wenzelm@39178
    12
import java.awt.Color
wenzelm@39178
    13
wenzelm@43386
    14
import org.lobobrowser.util.gui.ColorFactory
wenzelm@43414
    15
import org.gjt.sp.jedit.syntax.{Token => JEditToken}
wenzelm@39178
    16
wenzelm@39178
    17
wenzelm@39178
    18
object Isabelle_Markup
wenzelm@39178
    19
{
wenzelm@39178
    20
  /* physical rendering */
wenzelm@39178
    21
wenzelm@43377
    22
  // see http://www.w3schools.com/css/css_colornames.asp
wenzelm@43377
    23
wenzelm@43386
    24
  def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
wenzelm@43386
    25
wenzelm@39178
    26
  val outdated_color = new Color(240, 240, 240)
wenzelm@39178
    27
  val unfinished_color = new Color(255, 228, 225)
wenzelm@39178
    28
wenzelm@39690
    29
  val light_color = new Color(240, 240, 240)
wenzelm@39178
    30
  val regular_color = new Color(192, 192, 192)
wenzelm@39692
    31
  val warning_color = new Color(255, 140, 0)
wenzelm@39691
    32
  val error_color = new Color(178, 34, 34)
wenzelm@39690
    33
  val bad_color = new Color(255, 106, 106, 100)
wenzelm@42171
    34
  val hilite_color = new Color(255, 204, 102, 100)
wenzelm@39178
    35
wenzelm@43388
    36
  val keyword1_color = get_color("#006699")
wenzelm@43388
    37
  val keyword2_color = get_color("#009966")
wenzelm@43388
    38
wenzelm@39181
    39
  class Icon(val priority: Int, val icon: javax.swing.Icon)
wenzelm@39181
    40
  {
wenzelm@39181
    41
    def >= (that: Icon): Boolean = this.priority >= that.priority
wenzelm@39181
    42
  }
wenzelm@39241
    43
  val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-warning.png"))
wenzelm@39241
    44
  val error_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-error.png"))
wenzelm@39178
    45
wenzelm@39178
    46
wenzelm@39178
    47
  /* command status */
wenzelm@39178
    48
wenzelm@39178
    49
  def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
wenzelm@39178
    50
  {
wenzelm@39178
    51
    val state = snapshot.state(command)
wenzelm@39178
    52
    if (snapshot.is_outdated) Some(outdated_color)
wenzelm@39178
    53
    else
wenzelm@39178
    54
      Isar_Document.command_status(state.status) match {
wenzelm@39178
    55
        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
wenzelm@39178
    56
        case Isar_Document.Unprocessed => Some(unfinished_color)
wenzelm@39178
    57
        case _ => None
wenzelm@39178
    58
      }
wenzelm@39178
    59
  }
wenzelm@39178
    60
wenzelm@39178
    61
  def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
wenzelm@39178
    62
  {
wenzelm@39178
    63
    val state = snapshot.state(command)
wenzelm@39178
    64
    if (snapshot.is_outdated) None
wenzelm@39178
    65
    else
wenzelm@39178
    66
      Isar_Document.command_status(state.status) match {
wenzelm@39512
    67
        case Isar_Document.Forked(i) => if (i > 0) Some(unfinished_color) else None
wenzelm@39178
    68
        case Isar_Document.Unprocessed => Some(unfinished_color)
wenzelm@39178
    69
        case Isar_Document.Failed => Some(error_color)
wenzelm@39512
    70
        case Isar_Document.Finished =>
wenzelm@39512
    71
          if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color)
wenzelm@39512
    72
          else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color)
wenzelm@39512
    73
          else None
wenzelm@39178
    74
      }
wenzelm@39178
    75
  }
wenzelm@39178
    76
wenzelm@39178
    77
wenzelm@39178
    78
  /* markup selectors */
wenzelm@39178
    79
wenzelm@39178
    80
  val message: Markup_Tree.Select[Color] =
wenzelm@39178
    81
  {
wenzelm@39178
    82
    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
wenzelm@39178
    83
    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
wenzelm@39178
    84
    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
wenzelm@39178
    85
  }
wenzelm@39178
    86
wenzelm@40338
    87
  val popup: Markup_Tree.Select[String] =
wenzelm@39740
    88
  {
wenzelm@39740
    89
    case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _))
wenzelm@40338
    90
    if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
wenzelm@40339
    91
      Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))
wenzelm@39740
    92
  }
wenzelm@39740
    93
wenzelm@39181
    94
  val gutter_message: Markup_Tree.Select[Icon] =
wenzelm@39181
    95
  {
wenzelm@39181
    96
    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
wenzelm@39181
    97
    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
wenzelm@39181
    98
  }
wenzelm@39181
    99
wenzelm@39700
   100
  val background1: Markup_Tree.Select[Color] =
wenzelm@39178
   101
  {
wenzelm@39178
   102
    case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
wenzelm@42171
   103
    case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
wenzelm@39178
   104
  }
wenzelm@39178
   105
wenzelm@39700
   106
  val background2: Markup_Tree.Select[Color] =
wenzelm@39178
   107
  {
wenzelm@39690
   108
    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
wenzelm@39178
   109
  }
wenzelm@39178
   110
wenzelm@43386
   111
  private val foreground_colors: Map[String, Color] =
wenzelm@43386
   112
    Map(
wenzelm@43386
   113
      Markup.TCLASS -> get_color("red"),
wenzelm@43386
   114
      Markup.TFREE -> get_color("#A020F0"),
wenzelm@43386
   115
      Markup.TVAR -> get_color("#A020F0"),
wenzelm@43386
   116
      Markup.CONST -> get_color("dimgrey"),
wenzelm@43386
   117
      Markup.FREE -> get_color("blue"),
wenzelm@43386
   118
      Markup.SKOLEM -> get_color("#D2691E"),
wenzelm@43386
   119
      Markup.BOUND -> get_color("green"),
wenzelm@43386
   120
      Markup.VAR -> get_color("#00009B"),
wenzelm@43386
   121
      Markup.INNER_STRING -> get_color("#D2691E"),
wenzelm@43386
   122
      Markup.INNER_COMMENT -> get_color("#8B0000"),
wenzelm@43386
   123
      Markup.DYNAMIC_FACT -> get_color("yellowgreen"),
wenzelm@43388
   124
      Markup.LITERAL -> keyword1_color,
wenzelm@43388
   125
      Markup.ML_KEYWORD -> keyword1_color,
wenzelm@43386
   126
      Markup.ML_DELIMITER -> get_color("black"),
wenzelm@43386
   127
      Markup.ML_NUMERAL -> get_color("red"),
wenzelm@43386
   128
      Markup.ML_CHAR -> get_color("#D2691E"),
wenzelm@43386
   129
      Markup.ML_STRING -> get_color("#D2691E"),
wenzelm@43386
   130
      Markup.ML_COMMENT -> get_color("#8B0000"),
wenzelm@43431
   131
      Markup.ML_MALFORMED -> get_color("#FF6A6A"),
wenzelm@43431
   132
      Markup.ANTIQ -> get_color("blue"))
wenzelm@43386
   133
wenzelm@43376
   134
  val foreground: Markup_Tree.Select[Color] =
wenzelm@43376
   135
  {
wenzelm@43386
   136
    case Text.Info(_, XML.Elem(Markup(m, _), _))
wenzelm@43386
   137
    if foreground_colors.isDefinedAt(m) => foreground_colors(m)
wenzelm@43376
   138
  }
wenzelm@43376
   139
wenzelm@43431
   140
  private val tooltips: Map[String, String] =
wenzelm@43431
   141
    Map(
wenzelm@43431
   142
      Markup.SORT -> "sort",
wenzelm@43431
   143
      Markup.TYP -> "type",
wenzelm@43431
   144
      Markup.TERM -> "term",
wenzelm@43431
   145
      Markup.PROP -> "proposition",
wenzelm@43431
   146
      Markup.TOKEN_RANGE -> "inner syntax token",
wenzelm@43431
   147
      Markup.FREE -> "free variable (globally fixed)",
wenzelm@43431
   148
      Markup.SKOLEM -> "skolem variable (locally fixed)",
wenzelm@43431
   149
      Markup.BOUND -> "bound variable (internally fixed)",
wenzelm@43431
   150
      Markup.VAR -> "schematic variable",
wenzelm@43431
   151
      Markup.TFREE -> "free type variable",
wenzelm@43431
   152
      Markup.TVAR -> "schematic type variable",
wenzelm@43431
   153
      Markup.ML_SOURCE -> "ML source",
wenzelm@43431
   154
      Markup.DOC_SOURCE -> "document source")
wenzelm@43431
   155
wenzelm@39178
   156
  val tooltip: Markup_Tree.Select[String] =
wenzelm@39178
   157
  {
wenzelm@42283
   158
    case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\""
wenzelm@39178
   159
    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
wenzelm@40339
   160
      Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
wenzelm@40339
   161
        margin = Isabelle.Int_Property("tooltip-margin"))
wenzelm@43431
   162
    case Text.Info(_, XML.Elem(Markup(name, _), _))
wenzelm@43431
   163
    if tooltips.isDefinedAt(name) => tooltips(name)
wenzelm@42302
   164
  }
wenzelm@42302
   165
wenzelm@42302
   166
  private val subexp_include =
wenzelm@42302
   167
    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
wenzelm@42302
   168
      Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
wenzelm@43431
   169
      Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOC_SOURCE)
wenzelm@42302
   170
wenzelm@42302
   171
  val subexp: Markup_Tree.Select[(Text.Range, Color)] =
wenzelm@42302
   172
  {
wenzelm@42302
   173
    case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
wenzelm@42302
   174
      (range, Color.black)
wenzelm@39178
   175
  }
wenzelm@39179
   176
wenzelm@39179
   177
wenzelm@39179
   178
  /* token markup -- text styles */
wenzelm@39179
   179
wenzelm@39179
   180
  private val command_style: Map[String, Byte] =
wenzelm@39179
   181
  {
wenzelm@43414
   182
    import JEditToken._
wenzelm@39179
   183
    Map[String, Byte](
wenzelm@39179
   184
      Keyword.THY_END -> KEYWORD2,
wenzelm@39179
   185
      Keyword.THY_SCRIPT -> LABEL,
wenzelm@39179
   186
      Keyword.PRF_SCRIPT -> LABEL,
wenzelm@39179
   187
      Keyword.PRF_ASM -> KEYWORD3,
wenzelm@39179
   188
      Keyword.PRF_ASM_GOAL -> KEYWORD3
wenzelm@39179
   189
    ).withDefaultValue(KEYWORD1)
wenzelm@39179
   190
  }
wenzelm@39179
   191
wenzelm@43414
   192
  private val token_style: Map[Token.Kind.Value, Byte] =
wenzelm@39179
   193
  {
wenzelm@43414
   194
    import JEditToken._
wenzelm@43414
   195
    Map[Token.Kind.Value, Byte](
wenzelm@43414
   196
      Token.Kind.KEYWORD -> KEYWORD2,
wenzelm@43414
   197
      Token.Kind.IDENT -> NULL,
wenzelm@43414
   198
      Token.Kind.LONG_IDENT -> NULL,
wenzelm@43414
   199
      Token.Kind.SYM_IDENT -> NULL,
wenzelm@43414
   200
      Token.Kind.VAR -> NULL,
wenzelm@43414
   201
      Token.Kind.TYPE_IDENT -> NULL,
wenzelm@43414
   202
      Token.Kind.TYPE_VAR -> NULL,
wenzelm@43414
   203
      Token.Kind.NAT -> NULL,
wenzelm@43414
   204
      Token.Kind.FLOAT -> NULL,
wenzelm@43431
   205
      Token.Kind.STRING -> LITERAL1,
wenzelm@43431
   206
      Token.Kind.ALT_STRING -> LITERAL2,
wenzelm@43414
   207
      Token.Kind.VERBATIM -> COMMENT3,
wenzelm@43414
   208
      Token.Kind.SPACE -> NULL,
wenzelm@43414
   209
      Token.Kind.COMMENT -> COMMENT1,
wenzelm@43414
   210
      Token.Kind.UNPARSED -> INVALID
wenzelm@39179
   211
    ).withDefaultValue(NULL)
wenzelm@39179
   212
  }
wenzelm@39179
   213
wenzelm@43414
   214
  def token_markup(syntax: Outer_Syntax, token: Token): Byte =
wenzelm@43430
   215
    if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
wenzelm@43430
   216
    else if (token.is_operator) JEditToken.OPERATOR
wenzelm@43414
   217
    else token_style(token.kind)
wenzelm@39178
   218
}