src/Tools/jEdit/src/jedit/isabelle_markup.scala
author wenzelm
Sun Apr 17 21:17:45 2011 +0200 (2011-04-17)
changeset 42380 9371ea9f91fb
parent 42378 d9fe47d21b41
child 42492 83c57d850049
permissions -rw-r--r--
markup attributes/methods via name space;
eliminated obsolete markup;
wenzelm@39178
     1
/*  Title:      Tools/jEdit/src/jedit/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@39179
    14
import org.gjt.sp.jedit.syntax.Token
wenzelm@39178
    15
wenzelm@39178
    16
wenzelm@39178
    17
object Isabelle_Markup
wenzelm@39178
    18
{
wenzelm@39178
    19
  /* physical rendering */
wenzelm@39178
    20
wenzelm@39178
    21
  val outdated_color = new Color(240, 240, 240)
wenzelm@39178
    22
  val unfinished_color = new Color(255, 228, 225)
wenzelm@39178
    23
wenzelm@39690
    24
  val light_color = new Color(240, 240, 240)
wenzelm@39178
    25
  val regular_color = new Color(192, 192, 192)
wenzelm@39692
    26
  val warning_color = new Color(255, 140, 0)
wenzelm@39691
    27
  val error_color = new Color(178, 34, 34)
wenzelm@39690
    28
  val bad_color = new Color(255, 106, 106, 100)
wenzelm@42171
    29
  val hilite_color = new Color(255, 204, 102, 100)
wenzelm@39178
    30
wenzelm@39181
    31
  class Icon(val priority: Int, val icon: javax.swing.Icon)
wenzelm@39181
    32
  {
wenzelm@39181
    33
    def >= (that: Icon): Boolean = this.priority >= that.priority
wenzelm@39181
    34
  }
wenzelm@39241
    35
  val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-warning.png"))
wenzelm@39241
    36
  val error_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-error.png"))
wenzelm@39178
    37
wenzelm@39178
    38
wenzelm@39178
    39
  /* command status */
wenzelm@39178
    40
wenzelm@39178
    41
  def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
wenzelm@39178
    42
  {
wenzelm@39178
    43
    val state = snapshot.state(command)
wenzelm@39178
    44
    if (snapshot.is_outdated) Some(outdated_color)
wenzelm@39178
    45
    else
wenzelm@39178
    46
      Isar_Document.command_status(state.status) match {
wenzelm@39178
    47
        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
wenzelm@39178
    48
        case Isar_Document.Unprocessed => Some(unfinished_color)
wenzelm@39178
    49
        case _ => None
wenzelm@39178
    50
      }
wenzelm@39178
    51
  }
wenzelm@39178
    52
wenzelm@39178
    53
  def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
wenzelm@39178
    54
  {
wenzelm@39178
    55
    val state = snapshot.state(command)
wenzelm@39178
    56
    if (snapshot.is_outdated) None
wenzelm@39178
    57
    else
wenzelm@39178
    58
      Isar_Document.command_status(state.status) match {
wenzelm@39512
    59
        case Isar_Document.Forked(i) => if (i > 0) Some(unfinished_color) else None
wenzelm@39178
    60
        case Isar_Document.Unprocessed => Some(unfinished_color)
wenzelm@39178
    61
        case Isar_Document.Failed => Some(error_color)
wenzelm@39512
    62
        case Isar_Document.Finished =>
wenzelm@39512
    63
          if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color)
wenzelm@39512
    64
          else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color)
wenzelm@39512
    65
          else None
wenzelm@39178
    66
      }
wenzelm@39178
    67
  }
wenzelm@39178
    68
wenzelm@39178
    69
wenzelm@39178
    70
  /* markup selectors */
wenzelm@39178
    71
wenzelm@39178
    72
  val message: Markup_Tree.Select[Color] =
wenzelm@39178
    73
  {
wenzelm@39178
    74
    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
wenzelm@39178
    75
    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
wenzelm@39178
    76
    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
wenzelm@39178
    77
  }
wenzelm@39178
    78
wenzelm@40338
    79
  val popup: Markup_Tree.Select[String] =
wenzelm@39740
    80
  {
wenzelm@39740
    81
    case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _))
wenzelm@40338
    82
    if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
wenzelm@40339
    83
      Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))
wenzelm@39740
    84
  }
wenzelm@39740
    85
wenzelm@39181
    86
  val gutter_message: Markup_Tree.Select[Icon] =
wenzelm@39181
    87
  {
wenzelm@39181
    88
    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
wenzelm@39181
    89
    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
wenzelm@39181
    90
  }
wenzelm@39181
    91
wenzelm@39700
    92
  val background1: Markup_Tree.Select[Color] =
wenzelm@39178
    93
  {
wenzelm@39178
    94
    case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
wenzelm@42171
    95
    case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
wenzelm@39178
    96
  }
wenzelm@39178
    97
wenzelm@39700
    98
  val background2: Markup_Tree.Select[Color] =
wenzelm@39178
    99
  {
wenzelm@39690
   100
    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
wenzelm@39178
   101
  }
wenzelm@39178
   102
wenzelm@39178
   103
  val tooltip: Markup_Tree.Select[String] =
wenzelm@39178
   104
  {
wenzelm@42283
   105
    case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\""
wenzelm@39178
   106
    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
wenzelm@40339
   107
      Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
wenzelm@40339
   108
        margin = Isabelle.Int_Property("tooltip-margin"))
wenzelm@39178
   109
    case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
wenzelm@39178
   110
    case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
wenzelm@39178
   111
    case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
wenzelm@39178
   112
    case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
wenzelm@39704
   113
    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => "inner syntax token"
wenzelm@42203
   114
    case Text.Info(_, XML.Elem(Markup(Markup.FREE, _), _)) => "free variable (globally fixed)"
wenzelm@42203
   115
    case Text.Info(_, XML.Elem(Markup(Markup.SKOLEM, _), _)) => "skolem variable (locally fixed)"
wenzelm@42203
   116
    case Text.Info(_, XML.Elem(Markup(Markup.BOUND, _), _)) => "bound variable (internally fixed)"
wenzelm@42203
   117
    case Text.Info(_, XML.Elem(Markup(Markup.VAR, _), _)) => "schematic variable"
wenzelm@42302
   118
    case Text.Info(_, XML.Elem(Markup(Markup.TFREE, _), _)) => "free type variable"
wenzelm@42302
   119
    case Text.Info(_, XML.Elem(Markup(Markup.TVAR, _), _)) => "schematic type variable"
wenzelm@42302
   120
  }
wenzelm@42302
   121
wenzelm@42302
   122
  private val subexp_include =
wenzelm@42302
   123
    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
wenzelm@42302
   124
      Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
wenzelm@42302
   125
      Markup.TFREE, Markup.TVAR)
wenzelm@42302
   126
wenzelm@42302
   127
  val subexp: Markup_Tree.Select[(Text.Range, Color)] =
wenzelm@42302
   128
  {
wenzelm@42302
   129
    case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
wenzelm@42302
   130
      (range, Color.black)
wenzelm@39178
   131
  }
wenzelm@39179
   132
wenzelm@39179
   133
wenzelm@39179
   134
  /* token markup -- text styles */
wenzelm@39179
   135
wenzelm@39179
   136
  private val command_style: Map[String, Byte] =
wenzelm@39179
   137
  {
wenzelm@39179
   138
    import Token._
wenzelm@39179
   139
    Map[String, Byte](
wenzelm@39179
   140
      Keyword.THY_END -> KEYWORD2,
wenzelm@39179
   141
      Keyword.THY_SCRIPT -> LABEL,
wenzelm@39179
   142
      Keyword.PRF_SCRIPT -> LABEL,
wenzelm@39179
   143
      Keyword.PRF_ASM -> KEYWORD3,
wenzelm@39179
   144
      Keyword.PRF_ASM_GOAL -> KEYWORD3
wenzelm@39179
   145
    ).withDefaultValue(KEYWORD1)
wenzelm@39179
   146
  }
wenzelm@39179
   147
wenzelm@39179
   148
  private val token_style: Map[String, Byte] =
wenzelm@39179
   149
  {
wenzelm@39179
   150
    import Token._
wenzelm@39179
   151
    Map[String, Byte](
wenzelm@39179
   152
      // logical entities
wenzelm@39179
   153
      Markup.TCLASS -> NULL,
wenzelm@39179
   154
      Markup.TYCON -> NULL,
wenzelm@39179
   155
      Markup.FIXED_DECL -> FUNCTION,
wenzelm@39179
   156
      Markup.FIXED -> NULL,
wenzelm@42136
   157
      Markup.CONST -> LITERAL2,
wenzelm@39179
   158
      Markup.DYNAMIC_FACT -> LABEL,
wenzelm@39179
   159
      // inner syntax
wenzelm@39179
   160
      Markup.TFREE -> NULL,
wenzelm@42132
   161
      Markup.FREE -> MARKUP,
wenzelm@39179
   162
      Markup.TVAR -> NULL,
wenzelm@42171
   163
      Markup.SKOLEM -> COMMENT2,
wenzelm@42132
   164
      Markup.BOUND -> LABEL,
wenzelm@39179
   165
      Markup.VAR -> NULL,
wenzelm@39179
   166
      Markup.NUM -> DIGIT,
wenzelm@39179
   167
      Markup.FLOAT -> DIGIT,
wenzelm@39179
   168
      Markup.XNUM -> DIGIT,
wenzelm@39179
   169
      Markup.XSTR -> LITERAL4,
wenzelm@39179
   170
      Markup.LITERAL -> OPERATOR,
wenzelm@39179
   171
      Markup.INNER_COMMENT -> COMMENT1,
wenzelm@39179
   172
      Markup.SORT -> NULL,
wenzelm@39179
   173
      Markup.TYP -> NULL,
wenzelm@39179
   174
      Markup.TERM -> NULL,
wenzelm@39179
   175
      Markup.PROP -> NULL,
wenzelm@39179
   176
      // ML syntax
wenzelm@39179
   177
      Markup.ML_KEYWORD -> KEYWORD1,
wenzelm@39179
   178
      Markup.ML_DELIMITER -> OPERATOR,
wenzelm@39179
   179
      Markup.ML_IDENT -> NULL,
wenzelm@39179
   180
      Markup.ML_TVAR -> NULL,
wenzelm@39179
   181
      Markup.ML_NUMERAL -> DIGIT,
wenzelm@39179
   182
      Markup.ML_CHAR -> LITERAL1,
wenzelm@39179
   183
      Markup.ML_STRING -> LITERAL1,
wenzelm@39179
   184
      Markup.ML_COMMENT -> COMMENT1,
wenzelm@39179
   185
      Markup.ML_MALFORMED -> INVALID,
wenzelm@39179
   186
      // embedded source text
wenzelm@39179
   187
      Markup.ML_SOURCE -> COMMENT3,
wenzelm@39179
   188
      Markup.DOC_SOURCE -> COMMENT3,
wenzelm@39179
   189
      Markup.ANTIQ -> COMMENT4,
wenzelm@39179
   190
      Markup.ML_ANTIQ -> COMMENT4,
wenzelm@39179
   191
      Markup.DOC_ANTIQ -> COMMENT4,
wenzelm@39179
   192
      // outer syntax
wenzelm@39179
   193
      Markup.KEYWORD -> KEYWORD2,
wenzelm@39179
   194
      Markup.OPERATOR -> OPERATOR,
wenzelm@39179
   195
      Markup.COMMAND -> KEYWORD1,
wenzelm@39179
   196
      Markup.IDENT -> NULL,
wenzelm@39179
   197
      Markup.VERBATIM -> COMMENT3,
wenzelm@39179
   198
      Markup.COMMENT -> COMMENT1,
wenzelm@39179
   199
      Markup.CONTROL -> COMMENT3,
wenzelm@39179
   200
      Markup.MALFORMED -> INVALID,
wenzelm@39179
   201
      Markup.STRING -> LITERAL3,
wenzelm@39179
   202
      Markup.ALTSTRING -> LITERAL1
wenzelm@39179
   203
    ).withDefaultValue(NULL)
wenzelm@39179
   204
  }
wenzelm@39179
   205
wenzelm@39179
   206
  def tokens(syntax: Outer_Syntax): Markup_Tree.Select[Byte] =
wenzelm@39179
   207
  {
wenzelm@39179
   208
    case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
wenzelm@39179
   209
    if syntax.keyword_kind(name).isDefined => command_style(syntax.keyword_kind(name).get)
wenzelm@39179
   210
wenzelm@42136
   211
    case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Kind(kind)), _))
wenzelm@42136
   212
    if token_style(kind) != Token.NULL => token_style(kind)
wenzelm@42136
   213
wenzelm@39179
   214
    case Text.Info(_, XML.Elem(Markup(name, _), _))
wenzelm@39179
   215
    if token_style(name) != Token.NULL => token_style(name)
wenzelm@39179
   216
  }
wenzelm@39178
   217
}