src/Tools/jEdit/src/isabelle_rendering.scala
author wenzelm
Thu Dec 01 14:29:14 2011 +0100 (2011-12-01 ago)
changeset 45709 87017fcbad83
parent 45672 a497c5d4a523
child 46166 4beb2f41ed93
permissions -rw-r--r--
clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm@45665
     1
/*  Title:      Tools/jEdit/src/isabelle_rendering.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@45460
    17
import scala.collection.immutable.SortedMap
wenzelm@45460
    18
wenzelm@39178
    19
wenzelm@45665
    20
object Isabelle_Rendering
wenzelm@39178
    21
{
wenzelm@39178
    22
  /* physical rendering */
wenzelm@39178
    23
wenzelm@43377
    24
  // see http://www.w3schools.com/css/css_colornames.asp
wenzelm@43377
    25
wenzelm@43386
    26
  def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
wenzelm@43386
    27
wenzelm@44579
    28
  val outdated_color = new Color(238, 227, 227)
wenzelm@44611
    29
  val running_color = new Color(97, 0, 97)
wenzelm@44611
    30
  val running1_color = new Color(97, 0, 97, 100)
wenzelm@44866
    31
  val unprocessed_color = new Color(255, 160, 160)
wenzelm@44866
    32
  val unprocessed1_color = new Color(255, 160, 160, 50)
wenzelm@39178
    33
wenzelm@39690
    34
  val light_color = new Color(240, 240, 240)
wenzelm@39178
    35
  val regular_color = new Color(192, 192, 192)
wenzelm@39692
    36
  val warning_color = new Color(255, 140, 0)
wenzelm@39691
    37
  val error_color = new Color(178, 34, 34)
wenzelm@44866
    38
  val error1_color = new Color(178, 34, 34, 50)
wenzelm@39690
    39
  val bad_color = new Color(255, 106, 106, 100)
wenzelm@42171
    40
  val hilite_color = new Color(255, 204, 102, 100)
wenzelm@39178
    41
wenzelm@44546
    42
  val quoted_color = new Color(139, 139, 139, 25)
wenzelm@44545
    43
  val subexp_color = new Color(80, 80, 80, 50)
wenzelm@43435
    44
wenzelm@43388
    45
  val keyword1_color = get_color("#006699")
wenzelm@43388
    46
  val keyword2_color = get_color("#009966")
wenzelm@43388
    47
wenzelm@39181
    48
  class Icon(val priority: Int, val icon: javax.swing.Icon)
wenzelm@39181
    49
  {
wenzelm@39181
    50
    def >= (that: Icon): Boolean = this.priority >= that.priority
wenzelm@39181
    51
  }
wenzelm@44547
    52
  val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-information.png"))
wenzelm@44549
    53
  val legacy_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-warning.png"))
wenzelm@44549
    54
  val error_icon = new Icon(3, Isabelle.load_icon("16x16/status/dialog-error.png"))
wenzelm@39178
    55
wenzelm@39178
    56
wenzelm@39178
    57
  /* command status */
wenzelm@39178
    58
wenzelm@39178
    59
  def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
wenzelm@39178
    60
  {
wenzelm@44582
    61
    val state = snapshot.command_state(command)
wenzelm@44723
    62
    if (snapshot.is_outdated) Some(outdated_color)
wenzelm@39178
    63
    else
wenzelm@45709
    64
      Protocol.command_status(state.status) match {
wenzelm@45709
    65
        case Protocol.Forked(i) if i > 0 => Some(running1_color)
wenzelm@45709
    66
        case Protocol.Unprocessed => Some(unprocessed1_color)
wenzelm@39178
    67
        case _ => None
wenzelm@39178
    68
      }
wenzelm@39178
    69
  }
wenzelm@39178
    70
wenzelm@39178
    71
  def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
wenzelm@39178
    72
  {
wenzelm@44582
    73
    val state = snapshot.command_state(command)
wenzelm@39178
    74
    if (snapshot.is_outdated) None
wenzelm@39178
    75
    else
wenzelm@45709
    76
      Protocol.command_status(state.status) match {
wenzelm@45709
    77
        case Protocol.Forked(i) => if (i > 0) Some(running_color) else None
wenzelm@45709
    78
        case Protocol.Unprocessed => Some(unprocessed_color)
wenzelm@45709
    79
        case Protocol.Failed => Some(error_color)
wenzelm@45709
    80
        case Protocol.Finished =>
wenzelm@45709
    81
          if (state.results.exists(r => Protocol.is_error(r._2))) Some(error_color)
wenzelm@45709
    82
          else if (state.results.exists(r => Protocol.is_warning(r._2))) Some(warning_color)
wenzelm@39512
    83
          else None
wenzelm@39178
    84
      }
wenzelm@39178
    85
  }
wenzelm@39178
    86
wenzelm@39178
    87
wenzelm@39178
    88
  /* markup selectors */
wenzelm@39178
    89
wenzelm@45468
    90
  val message =
wenzelm@45468
    91
    Markup_Tree.Select[Color](
wenzelm@45474
    92
      {
wenzelm@45666
    93
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN, _), _)) => regular_color
wenzelm@45666
    94
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), _)) => warning_color
wenzelm@45666
    95
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_color
wenzelm@45474
    96
      },
wenzelm@45666
    97
      Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)))
wenzelm@39178
    98
wenzelm@45467
    99
  val tooltip_message =
wenzelm@45467
   100
    Markup_Tree.Cumulate[SortedMap[Long, String]](SortedMap.empty,
wenzelm@45467
   101
      {
wenzelm@45666
   102
        case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
wenzelm@45666
   103
        if markup == Isabelle_Markup.WRITELN ||
wenzelm@45666
   104
            markup == Isabelle_Markup.WARNING ||
wenzelm@45666
   105
            markup == Isabelle_Markup.ERROR =>
wenzelm@45467
   106
          msgs + (serial ->
wenzelm@45467
   107
            Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
wenzelm@45474
   108
      },
wenzelm@45666
   109
      Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)))
wenzelm@39740
   110
wenzelm@45468
   111
  val gutter_message =
wenzelm@45468
   112
    Markup_Tree.Select[Icon](
wenzelm@45468
   113
      {
wenzelm@45666
   114
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body)) =>
wenzelm@45468
   115
          body match {
wenzelm@45666
   116
            case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => legacy_icon
wenzelm@45468
   117
            case _ => warning_icon
wenzelm@45468
   118
          }
wenzelm@45666
   119
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon
wenzelm@45474
   120
      },
wenzelm@45666
   121
      Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)))
wenzelm@39181
   122
wenzelm@45468
   123
  val background1 =
wenzelm@45468
   124
    Markup_Tree.Select[Color](
wenzelm@45468
   125
      {
wenzelm@45666
   126
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _)) => bad_color
wenzelm@45666
   127
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _)) => hilite_color
wenzelm@45474
   128
      },
wenzelm@45666
   129
      Some(Set(Isabelle_Markup.BAD, Isabelle_Markup.HILITE)))
wenzelm@39178
   130
wenzelm@45468
   131
  val background2 =
wenzelm@45468
   132
    Markup_Tree.Select[Color](
wenzelm@45468
   133
      {
wenzelm@45666
   134
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
wenzelm@45474
   135
      },
wenzelm@45666
   136
      Some(Set(Isabelle_Markup.TOKEN_RANGE)))
wenzelm@39178
   137
wenzelm@45468
   138
  val foreground =
wenzelm@45468
   139
    Markup_Tree.Select[Color](
wenzelm@45468
   140
      {
wenzelm@45666
   141
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
wenzelm@45666
   142
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
wenzelm@45666
   143
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
wenzelm@45474
   144
      },
wenzelm@45666
   145
      Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)))
wenzelm@44545
   146
wenzelm@43434
   147
  private val text_colors: Map[String, Color] =
wenzelm@43386
   148
    Map(
wenzelm@45666
   149
      Isabelle_Markup.STRING -> get_color("black"),
wenzelm@45666
   150
      Isabelle_Markup.ALTSTRING -> get_color("black"),
wenzelm@45666
   151
      Isabelle_Markup.VERBATIM -> get_color("black"),
wenzelm@45666
   152
      Isabelle_Markup.LITERAL -> keyword1_color,
wenzelm@45666
   153
      Isabelle_Markup.DELIMITER -> get_color("black"),
wenzelm@45666
   154
      Isabelle_Markup.TFREE -> get_color("#A020F0"),
wenzelm@45666
   155
      Isabelle_Markup.TVAR -> get_color("#A020F0"),
wenzelm@45666
   156
      Isabelle_Markup.FREE -> get_color("blue"),
wenzelm@45666
   157
      Isabelle_Markup.SKOLEM -> get_color("#D2691E"),
wenzelm@45666
   158
      Isabelle_Markup.BOUND -> get_color("green"),
wenzelm@45666
   159
      Isabelle_Markup.VAR -> get_color("#00009B"),
wenzelm@45666
   160
      Isabelle_Markup.INNER_STRING -> get_color("#D2691E"),
wenzelm@45666
   161
      Isabelle_Markup.INNER_COMMENT -> get_color("#8B0000"),
wenzelm@45666
   162
      Isabelle_Markup.DYNAMIC_FACT -> get_color("#7BA428"),
wenzelm@45666
   163
      Isabelle_Markup.ML_KEYWORD -> keyword1_color,
wenzelm@45666
   164
      Isabelle_Markup.ML_DELIMITER -> get_color("black"),
wenzelm@45666
   165
      Isabelle_Markup.ML_NUMERAL -> get_color("red"),
wenzelm@45666
   166
      Isabelle_Markup.ML_CHAR -> get_color("#D2691E"),
wenzelm@45666
   167
      Isabelle_Markup.ML_STRING -> get_color("#D2691E"),
wenzelm@45666
   168
      Isabelle_Markup.ML_COMMENT -> get_color("#8B0000"),
wenzelm@45666
   169
      Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"),
wenzelm@45666
   170
      Isabelle_Markup.ANTIQ -> get_color("blue"))
wenzelm@43386
   171
wenzelm@45468
   172
  val text_color =
wenzelm@45468
   173
    Markup_Tree.Select[Color](
wenzelm@45468
   174
      {
wenzelm@45474
   175
        case Text.Info(_, XML.Elem(Markup(m, _), _))
wenzelm@45474
   176
        if text_colors.isDefinedAt(m) => text_colors(m)
wenzelm@45474
   177
      },
wenzelm@45474
   178
      Some(Set() ++ text_colors.keys))
wenzelm@43376
   179
wenzelm@43431
   180
  private val tooltips: Map[String, String] =
wenzelm@43431
   181
    Map(
wenzelm@45666
   182
      Isabelle_Markup.SORT -> "sort",
wenzelm@45666
   183
      Isabelle_Markup.TYP -> "type",
wenzelm@45666
   184
      Isabelle_Markup.TERM -> "term",
wenzelm@45666
   185
      Isabelle_Markup.PROP -> "proposition",
wenzelm@45666
   186
      Isabelle_Markup.TOKEN_RANGE -> "inner syntax token",
wenzelm@45666
   187
      Isabelle_Markup.FREE -> "free variable",
wenzelm@45666
   188
      Isabelle_Markup.SKOLEM -> "skolem variable",
wenzelm@45666
   189
      Isabelle_Markup.BOUND -> "bound variable",
wenzelm@45666
   190
      Isabelle_Markup.VAR -> "schematic variable",
wenzelm@45666
   191
      Isabelle_Markup.TFREE -> "free type variable",
wenzelm@45666
   192
      Isabelle_Markup.TVAR -> "schematic type variable",
wenzelm@45666
   193
      Isabelle_Markup.ML_SOURCE -> "ML source",
wenzelm@45666
   194
      Isabelle_Markup.DOC_SOURCE -> "document source")
wenzelm@43431
   195
wenzelm@45445
   196
  private def string_of_typing(kind: String, body: XML.Body): String =
wenzelm@45445
   197
    Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
wenzelm@45445
   198
      margin = Isabelle.Int_Property("tooltip-margin"))
wenzelm@45445
   199
wenzelm@45468
   200
  val tooltip1 =
wenzelm@45468
   201
    Markup_Tree.Select[String](
wenzelm@45468
   202
      {
wenzelm@45666
   203
        case Text.Info(_, XML.Elem(Isabelle_Markup.Entity(kind, name), _)) => kind + " " + quote(name)
wenzelm@45666
   204
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body)) =>
wenzelm@45474
   205
          string_of_typing("ML:", body)
wenzelm@45468
   206
        case Text.Info(_, XML.Elem(Markup(name, _), _))
wenzelm@45468
   207
        if tooltips.isDefinedAt(name) => tooltips(name)
wenzelm@45474
   208
      },
wenzelm@45666
   209
      Some(Set(Isabelle_Markup.ENTITY, Isabelle_Markup.ML_TYPING) ++ tooltips.keys))
wenzelm@42302
   210
wenzelm@45468
   211
  val tooltip2 =
wenzelm@45468
   212
    Markup_Tree.Select[String](
wenzelm@45468
   213
      {
wenzelm@45666
   214
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body)) =>
wenzelm@45666
   215
          string_of_typing("::", body)
wenzelm@45474
   216
      },
wenzelm@45666
   217
      Some(Set(Isabelle_Markup.TYPING)))
wenzelm@45460
   218
wenzelm@42302
   219
  private val subexp_include =
wenzelm@45666
   220
    Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
wenzelm@45666
   221
      Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
wenzelm@45666
   222
      Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND,
wenzelm@45666
   223
      Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE,
wenzelm@45666
   224
      Isabelle_Markup.DOC_SOURCE)
wenzelm@42302
   225
wenzelm@45468
   226
  val subexp =
wenzelm@45468
   227
    Markup_Tree.Select[(Text.Range, Color)](
wenzelm@45468
   228
      {
wenzelm@45468
   229
        case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
wenzelm@45468
   230
          (range, subexp_color)
wenzelm@45474
   231
      },
wenzelm@45474
   232
      Some(subexp_include))
wenzelm@39179
   233
wenzelm@39179
   234
wenzelm@39179
   235
  /* token markup -- text styles */
wenzelm@39179
   236
wenzelm@39179
   237
  private val command_style: Map[String, Byte] =
wenzelm@39179
   238
  {
wenzelm@43414
   239
    import JEditToken._
wenzelm@39179
   240
    Map[String, Byte](
wenzelm@39179
   241
      Keyword.THY_END -> KEYWORD2,
wenzelm@39179
   242
      Keyword.THY_SCRIPT -> LABEL,
wenzelm@39179
   243
      Keyword.PRF_SCRIPT -> LABEL,
wenzelm@39179
   244
      Keyword.PRF_ASM -> KEYWORD3,
wenzelm@39179
   245
      Keyword.PRF_ASM_GOAL -> KEYWORD3
wenzelm@39179
   246
    ).withDefaultValue(KEYWORD1)
wenzelm@39179
   247
  }
wenzelm@39179
   248
wenzelm@43414
   249
  private val token_style: Map[Token.Kind.Value, Byte] =
wenzelm@39179
   250
  {
wenzelm@43414
   251
    import JEditToken._
wenzelm@43414
   252
    Map[Token.Kind.Value, Byte](
wenzelm@43414
   253
      Token.Kind.KEYWORD -> KEYWORD2,
wenzelm@43414
   254
      Token.Kind.IDENT -> NULL,
wenzelm@43414
   255
      Token.Kind.LONG_IDENT -> NULL,
wenzelm@43414
   256
      Token.Kind.SYM_IDENT -> NULL,
wenzelm@43414
   257
      Token.Kind.VAR -> NULL,
wenzelm@43414
   258
      Token.Kind.TYPE_IDENT -> NULL,
wenzelm@43414
   259
      Token.Kind.TYPE_VAR -> NULL,
wenzelm@43414
   260
      Token.Kind.NAT -> NULL,
wenzelm@43414
   261
      Token.Kind.FLOAT -> NULL,
wenzelm@43431
   262
      Token.Kind.STRING -> LITERAL1,
wenzelm@43431
   263
      Token.Kind.ALT_STRING -> LITERAL2,
wenzelm@43414
   264
      Token.Kind.VERBATIM -> COMMENT3,
wenzelm@43414
   265
      Token.Kind.SPACE -> NULL,
wenzelm@43414
   266
      Token.Kind.COMMENT -> COMMENT1,
wenzelm@43414
   267
      Token.Kind.UNPARSED -> INVALID
wenzelm@39179
   268
    ).withDefaultValue(NULL)
wenzelm@39179
   269
  }
wenzelm@39179
   270
wenzelm@43414
   271
  def token_markup(syntax: Outer_Syntax, token: Token): Byte =
wenzelm@43430
   272
    if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
wenzelm@43430
   273
    else if (token.is_operator) JEditToken.OPERATOR
wenzelm@43414
   274
    else token_style(token.kind)
wenzelm@39178
   275
}