src/Tools/jEdit/src/isabelle_rendering.scala
author wenzelm
Mon, 16 Jan 2012 13:19:44 +0100
changeset 46234 de441d4ff1be
parent 46228 302d3ecff25d
child 46235 e4e0b5190f3d
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45665
129db1416717 renamed Isabelle_Markup to Isabelle_Rendering to emphasize its meaning and make room for Pure Isabelle_Markup module;
wenzelm
parents: 45489
diff changeset
     1
/*  Title:      Tools/jEdit/src/isabelle_rendering.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
46227
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    13
import javax.swing.Icon
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    14
43386
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
    15
import org.lobobrowser.util.gui.ColorFactory
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
    16
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
    17
45460
dcd02d1a25d7 more tooltip content;
wenzelm
parents: 45454
diff changeset
    18
import scala.collection.immutable.SortedMap
dcd02d1a25d7 more tooltip content;
wenzelm
parents: 45454
diff changeset
    19
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    20
45665
129db1416717 renamed Isabelle_Markup to Isabelle_Rendering to emphasize its meaning and make room for Pure Isabelle_Markup module;
wenzelm
parents: 45489
diff changeset
    21
object Isabelle_Rendering
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    22
{
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    23
  /* physical rendering */
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    24
43377
ba199d75bc7e more accurate CSS colors;
wenzelm
parents: 43376
diff changeset
    25
  // see http://www.w3schools.com/css/css_colornames.asp
ba199d75bc7e more accurate CSS colors;
wenzelm
parents: 43376
diff changeset
    26
43386
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
    27
  def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
    28
44579
a9cf2380377d tuned colors -- more distance between outdated_color and quoted_color;
wenzelm
parents: 44549
diff changeset
    29
  val outdated_color = new Color(238, 227, 227)
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    30
  val unprocessed_color = new Color(255, 160, 160)
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    31
  val unprocessed1_color = new Color(255, 160, 160, 50)
44611
857c52a1c3f7 explicit running_color;
wenzelm
parents: 44602
diff changeset
    32
  val running_color = new Color(97, 0, 97)
857c52a1c3f7 explicit running_color;
wenzelm
parents: 44602
diff changeset
    33
  val running1_color = new Color(97, 0, 97, 100)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    34
39690
6c6164b37fef some attempts to improve visual appearance of bad text;
wenzelm
parents: 39512
diff changeset
    35
  val light_color = new Color(240, 240, 240)
46227
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    36
  val writeln_color = new Color(192, 192, 192)
39692
b88a6bc371de tuned warning_color;
wenzelm
parents: 39691
diff changeset
    37
  val warning_color = new Color(255, 140, 0)
39691
4ce5f79df87a tuned error_color;
wenzelm
parents: 39690
diff changeset
    38
  val error_color = new Color(178, 34, 34)
44866
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44723
diff changeset
    39
  val error1_color = new Color(178, 34, 34, 50)
39690
6c6164b37fef some attempts to improve visual appearance of bad text;
wenzelm
parents: 39512
diff changeset
    40
  val bad_color = new Color(255, 106, 106, 100)
42171
620343510c88 visualize skolem and hilite (undeclared frees);
wenzelm
parents: 42136
diff changeset
    41
  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
    42
44546
794a32d58c77 tuned colors;
wenzelm
parents: 44545
diff changeset
    43
  val quoted_color = new Color(139, 139, 139, 25)
44545
3c40007aa031 transparent foreground color for quoted entities;
wenzelm
parents: 44181
diff changeset
    44
  val subexp_color = new Color(80, 80, 80, 50)
43435
ae6b0c3e58a8 highlight via foreground painter, using alpha channel;
wenzelm
parents: 43434
diff changeset
    45
43388
34492601c0e0 tuned colors;
wenzelm
parents: 43386
diff changeset
    46
  val keyword1_color = get_color("#006699")
34492601c0e0 tuned colors;
wenzelm
parents: 43386
diff changeset
    47
  val keyword2_color = get_color("#009966")
34492601c0e0 tuned colors;
wenzelm
parents: 43386
diff changeset
    48
46227
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    49
  private val writeln_pri = 1
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    50
  private val warning_pri = 2
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    51
  private val legacy_pri = 3
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    52
  private val error_pri = 4
39178
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
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    55
  /* command overview */
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    56
46227
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    57
  def overview_color(snapshot: Document.Snapshot, range: Text.Range): Option[Color] =
39178
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
    if (snapshot.is_outdated) None
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    60
    else {
46227
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    61
      val results =
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    62
        snapshot.cumulate_markup[(Protocol.Status, Int)](
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    63
          range, (Protocol.Status.init, 0),
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    64
          Some(Protocol.command_status_markup + Isabelle_Markup.WARNING + Isabelle_Markup.ERROR),
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    65
          {
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    66
            case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    67
              if (markup.name == Isabelle_Markup.WARNING) (status, pri max warning_pri)
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    68
              else if (markup.name == Isabelle_Markup.ERROR) (status, pri max error_pri)
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    69
              else (Protocol.command_status(status, markup), pri)
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    70
          })
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    71
      if (results.isEmpty) None
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    72
      else {
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    73
        val (status, pri) =
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    74
          ((Protocol.Status.init, 0) /: results) {
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    75
            case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) }
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    76
46227
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    77
        if (pri == warning_pri) Some(warning_color)
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    78
        else if (pri == error_pri) Some(error_color)
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    79
        else if (status.is_unprocessed) Some(unprocessed_color)
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    80
        else if (status.is_running) Some(running_color)
4aa84f84d5e8 more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
wenzelm
parents: 46224
diff changeset
    81
        else if (status.is_failed) Some(error_color)
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    82
        else None
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    83
      }
46166
4beb2f41ed93 command status color via regular markup;
wenzelm
parents: 45709
diff changeset
    84
    }
39178
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
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    87
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    88
  /* markup selectors */
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
    89
46234
wenzelm
parents: 46228
diff changeset
    90
  private val subexp_include =
wenzelm
parents: 46228
diff changeset
    91
    Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
wenzelm
parents: 46228
diff changeset
    92
      Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
wenzelm
parents: 46228
diff changeset
    93
      Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND,
wenzelm
parents: 46228
diff changeset
    94
      Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE,
wenzelm
parents: 46228
diff changeset
    95
      Isabelle_Markup.DOC_SOURCE)
wenzelm
parents: 46228
diff changeset
    96
wenzelm
parents: 46228
diff changeset
    97
  def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Color]] =
wenzelm
parents: 46228
diff changeset
    98
  {
wenzelm
parents: 46228
diff changeset
    99
    snapshot.select_markup(range, Some(subexp_include),
wenzelm
parents: 46228
diff changeset
   100
        {
wenzelm
parents: 46228
diff changeset
   101
          case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
wenzelm
parents: 46228
diff changeset
   102
            Text.Info(snapshot.convert(range), subexp_color)
wenzelm
parents: 46228
diff changeset
   103
        }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
wenzelm
parents: 46228
diff changeset
   104
  }
wenzelm
parents: 46228
diff changeset
   105
wenzelm
parents: 46228
diff changeset
   106
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   107
  def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
46199
wenzelm
parents: 46198
diff changeset
   108
  {
wenzelm
parents: 46198
diff changeset
   109
    val msgs =
wenzelm
parents: 46198
diff changeset
   110
      snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
wenzelm
parents: 46198
diff changeset
   111
        Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
wenzelm
parents: 46198
diff changeset
   112
        {
wenzelm
parents: 46198
diff changeset
   113
          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
wenzelm
parents: 46198
diff changeset
   114
          if markup == Isabelle_Markup.WRITELN ||
wenzelm
parents: 46198
diff changeset
   115
              markup == Isabelle_Markup.WARNING ||
wenzelm
parents: 46198
diff changeset
   116
              markup == Isabelle_Markup.ERROR =>
wenzelm
parents: 46198
diff changeset
   117
            msgs + (serial ->
wenzelm
parents: 46198
diff changeset
   118
              Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
wenzelm
parents: 46198
diff changeset
   119
        }).toList.flatMap(_.info)
wenzelm
parents: 46198
diff changeset
   120
    if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2)))
wenzelm
parents: 46198
diff changeset
   121
  }
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39704
diff changeset
   122
43376
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43282
diff changeset
   123
43431
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   124
  private val tooltips: Map[String, String] =
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   125
    Map(
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   126
      Isabelle_Markup.SORT -> "sort",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   127
      Isabelle_Markup.TYP -> "type",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   128
      Isabelle_Markup.TERM -> "term",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   129
      Isabelle_Markup.PROP -> "proposition",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   130
      Isabelle_Markup.TOKEN_RANGE -> "inner syntax token",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   131
      Isabelle_Markup.FREE -> "free variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   132
      Isabelle_Markup.SKOLEM -> "skolem variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   133
      Isabelle_Markup.BOUND -> "bound variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   134
      Isabelle_Markup.VAR -> "schematic variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   135
      Isabelle_Markup.TFREE -> "free type variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   136
      Isabelle_Markup.TVAR -> "schematic type variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   137
      Isabelle_Markup.ML_SOURCE -> "ML source",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   138
      Isabelle_Markup.DOC_SOURCE -> "document source")
43431
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   139
45445
41e641a870de pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents: 44866
diff changeset
   140
  private def string_of_typing(kind: String, body: XML.Body): String =
41e641a870de pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents: 44866
diff changeset
   141
    Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
41e641a870de pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents: 44866
diff changeset
   142
      margin = Isabelle.Int_Property("tooltip-margin"))
41e641a870de pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents: 44866
diff changeset
   143
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   144
  def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   145
  {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   146
    val tip1 =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   147
      snapshot.select_markup(range,
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   148
        Some(Set(Isabelle_Markup.ENTITY, Isabelle_Markup.ML_TYPING) ++ tooltips.keys),
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   149
        {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   150
          case Text.Info(_, XML.Elem(Isabelle_Markup.Entity(kind, name), _)) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   151
            kind + " " + quote(name)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   152
          case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body)) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   153
            string_of_typing("ML:", body)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   154
          case Text.Info(_, XML.Elem(Markup(name, _), _))
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   155
          if tooltips.isDefinedAt(name) => tooltips(name)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   156
        })
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   157
    val tip2 =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   158
      snapshot.select_markup(range, Some(Set(Isabelle_Markup.TYPING)),
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   159
        {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   160
          case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body)) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   161
            string_of_typing("::", body)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   162
        })
42302
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   163
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   164
    val tips =
46198
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   165
      (tip1 match { case Text.Info(_, text) #:: _ => List(text) case _ => Nil }) :::
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   166
      (tip2 match { case Text.Info(_, text) #:: _ => List(text) case _ => Nil })
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   167
46196
805de058722b added cat_lines convenience;
wenzelm
parents: 46178
diff changeset
   168
    if (tips.isEmpty) None else Some(cat_lines(tips))
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   169
  }
45460
dcd02d1a25d7 more tooltip content;
wenzelm
parents: 45454
diff changeset
   170
46234
wenzelm
parents: 46228
diff changeset
   171
wenzelm
parents: 46228
diff changeset
   172
  private val gutter_icons = Map(
wenzelm
parents: 46228
diff changeset
   173
    warning_pri -> Isabelle.load_icon("16x16/status/dialog-information.png"),
wenzelm
parents: 46228
diff changeset
   174
    legacy_pri -> Isabelle.load_icon("16x16/status/dialog-warning.png"),
wenzelm
parents: 46228
diff changeset
   175
    error_pri -> Isabelle.load_icon("16x16/status/dialog-error.png"))
wenzelm
parents: 46228
diff changeset
   176
wenzelm
parents: 46228
diff changeset
   177
  def gutter_message(snapshot: Document.Snapshot, range: Text.Range): Option[Icon] =
wenzelm
parents: 46228
diff changeset
   178
  {
wenzelm
parents: 46228
diff changeset
   179
    val results =
wenzelm
parents: 46228
diff changeset
   180
      snapshot.cumulate_markup[Int](range, 0,
wenzelm
parents: 46228
diff changeset
   181
        Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
wenzelm
parents: 46228
diff changeset
   182
        {
wenzelm
parents: 46228
diff changeset
   183
          case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body))) =>
wenzelm
parents: 46228
diff changeset
   184
            body match {
wenzelm
parents: 46228
diff changeset
   185
              case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => pri max legacy_pri
wenzelm
parents: 46228
diff changeset
   186
              case _ => pri max warning_pri
wenzelm
parents: 46228
diff changeset
   187
            }
wenzelm
parents: 46228
diff changeset
   188
          case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _))) =>
wenzelm
parents: 46228
diff changeset
   189
            pri max error_pri
wenzelm
parents: 46228
diff changeset
   190
        })
wenzelm
parents: 46228
diff changeset
   191
    val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
wenzelm
parents: 46228
diff changeset
   192
    gutter_icons.get(pri)
wenzelm
parents: 46228
diff changeset
   193
  }
wenzelm
parents: 46228
diff changeset
   194
wenzelm
parents: 46228
diff changeset
   195
wenzelm
parents: 46228
diff changeset
   196
  private val squiggly_colors = Map(
wenzelm
parents: 46228
diff changeset
   197
    writeln_pri -> writeln_color,
wenzelm
parents: 46228
diff changeset
   198
    warning_pri -> warning_color,
wenzelm
parents: 46228
diff changeset
   199
    error_pri -> error_color)
wenzelm
parents: 46228
diff changeset
   200
wenzelm
parents: 46228
diff changeset
   201
  def squiggly_underline(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
wenzelm
parents: 46228
diff changeset
   202
  {
wenzelm
parents: 46228
diff changeset
   203
    val results =
wenzelm
parents: 46228
diff changeset
   204
      snapshot.cumulate_markup[Int](range, 0,
wenzelm
parents: 46228
diff changeset
   205
        Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
wenzelm
parents: 46228
diff changeset
   206
        {
wenzelm
parents: 46228
diff changeset
   207
          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) =>
wenzelm
parents: 46228
diff changeset
   208
            name match {
wenzelm
parents: 46228
diff changeset
   209
              case Isabelle_Markup.WRITELN => pri max writeln_pri
wenzelm
parents: 46228
diff changeset
   210
              case Isabelle_Markup.WARNING => pri max warning_pri
wenzelm
parents: 46228
diff changeset
   211
              case Isabelle_Markup.ERROR => pri max error_pri
wenzelm
parents: 46228
diff changeset
   212
              case _ => pri
wenzelm
parents: 46228
diff changeset
   213
            }
wenzelm
parents: 46228
diff changeset
   214
        })
wenzelm
parents: 46228
diff changeset
   215
    for {
wenzelm
parents: 46228
diff changeset
   216
      Text.Info(r, pri) <- results
wenzelm
parents: 46228
diff changeset
   217
      color <- squiggly_colors.get(pri)
wenzelm
parents: 46228
diff changeset
   218
    } yield Text.Info(r, color)
wenzelm
parents: 46228
diff changeset
   219
  }
wenzelm
parents: 46228
diff changeset
   220
42302
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   221
46234
wenzelm
parents: 46228
diff changeset
   222
  def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   223
  {
46234
wenzelm
parents: 46228
diff changeset
   224
    if (snapshot.is_outdated) Stream(Text.Info(range, outdated_color))
wenzelm
parents: 46228
diff changeset
   225
    else
wenzelm
parents: 46228
diff changeset
   226
      for {
wenzelm
parents: 46228
diff changeset
   227
        Text.Info(r, result) <-
wenzelm
parents: 46228
diff changeset
   228
          snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
wenzelm
parents: 46228
diff changeset
   229
            range, (Some(Protocol.Status.init), None),
wenzelm
parents: 46228
diff changeset
   230
            Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE),
wenzelm
parents: 46228
diff changeset
   231
            {
wenzelm
parents: 46228
diff changeset
   232
              case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
wenzelm
parents: 46228
diff changeset
   233
              if (Protocol.command_status_markup(markup.name)) =>
wenzelm
parents: 46228
diff changeset
   234
                (Some(Protocol.command_status(status, markup)), color)
wenzelm
parents: 46228
diff changeset
   235
              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
wenzelm
parents: 46228
diff changeset
   236
                (None, Some(bad_color))
wenzelm
parents: 46228
diff changeset
   237
              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
wenzelm
parents: 46228
diff changeset
   238
                (None, Some(hilite_color))
wenzelm
parents: 46228
diff changeset
   239
            })
wenzelm
parents: 46228
diff changeset
   240
        color <-
wenzelm
parents: 46228
diff changeset
   241
          (result match {
wenzelm
parents: 46228
diff changeset
   242
            case (Some(status), _) =>
wenzelm
parents: 46228
diff changeset
   243
              if (status.is_running) Some(running1_color)
wenzelm
parents: 46228
diff changeset
   244
              else if (status.is_unprocessed) Some(unprocessed1_color)
wenzelm
parents: 46228
diff changeset
   245
              else None
wenzelm
parents: 46228
diff changeset
   246
            case (_, opt_color) => opt_color
wenzelm
parents: 46228
diff changeset
   247
          })
wenzelm
parents: 46228
diff changeset
   248
      } yield Text.Info(r, color)
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   249
  }
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   250
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   251
46234
wenzelm
parents: 46228
diff changeset
   252
  def background2(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
wenzelm
parents: 46228
diff changeset
   253
    snapshot.select_markup(range,
wenzelm
parents: 46228
diff changeset
   254
      Some(Set(Isabelle_Markup.TOKEN_RANGE)),
wenzelm
parents: 46228
diff changeset
   255
      {
wenzelm
parents: 46228
diff changeset
   256
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
wenzelm
parents: 46228
diff changeset
   257
      })
wenzelm
parents: 46228
diff changeset
   258
wenzelm
parents: 46228
diff changeset
   259
wenzelm
parents: 46228
diff changeset
   260
  def foreground(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
wenzelm
parents: 46228
diff changeset
   261
    snapshot.select_markup(range,
wenzelm
parents: 46228
diff changeset
   262
      Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)),
wenzelm
parents: 46228
diff changeset
   263
      {
wenzelm
parents: 46228
diff changeset
   264
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
wenzelm
parents: 46228
diff changeset
   265
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
wenzelm
parents: 46228
diff changeset
   266
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
wenzelm
parents: 46228
diff changeset
   267
      })
wenzelm
parents: 46228
diff changeset
   268
wenzelm
parents: 46228
diff changeset
   269
wenzelm
parents: 46228
diff changeset
   270
  private val text_colors: Map[String, Color] =
wenzelm
parents: 46228
diff changeset
   271
    Map(
wenzelm
parents: 46228
diff changeset
   272
      Isabelle_Markup.STRING -> get_color("black"),
wenzelm
parents: 46228
diff changeset
   273
      Isabelle_Markup.ALTSTRING -> get_color("black"),
wenzelm
parents: 46228
diff changeset
   274
      Isabelle_Markup.VERBATIM -> get_color("black"),
wenzelm
parents: 46228
diff changeset
   275
      Isabelle_Markup.LITERAL -> keyword1_color,
wenzelm
parents: 46228
diff changeset
   276
      Isabelle_Markup.DELIMITER -> get_color("black"),
wenzelm
parents: 46228
diff changeset
   277
      Isabelle_Markup.TFREE -> get_color("#A020F0"),
wenzelm
parents: 46228
diff changeset
   278
      Isabelle_Markup.TVAR -> get_color("#A020F0"),
wenzelm
parents: 46228
diff changeset
   279
      Isabelle_Markup.FREE -> get_color("blue"),
wenzelm
parents: 46228
diff changeset
   280
      Isabelle_Markup.SKOLEM -> get_color("#D2691E"),
wenzelm
parents: 46228
diff changeset
   281
      Isabelle_Markup.BOUND -> get_color("green"),
wenzelm
parents: 46228
diff changeset
   282
      Isabelle_Markup.VAR -> get_color("#00009B"),
wenzelm
parents: 46228
diff changeset
   283
      Isabelle_Markup.INNER_STRING -> get_color("#D2691E"),
wenzelm
parents: 46228
diff changeset
   284
      Isabelle_Markup.INNER_COMMENT -> get_color("#8B0000"),
wenzelm
parents: 46228
diff changeset
   285
      Isabelle_Markup.DYNAMIC_FACT -> get_color("#7BA428"),
wenzelm
parents: 46228
diff changeset
   286
      Isabelle_Markup.ML_KEYWORD -> keyword1_color,
wenzelm
parents: 46228
diff changeset
   287
      Isabelle_Markup.ML_DELIMITER -> get_color("black"),
wenzelm
parents: 46228
diff changeset
   288
      Isabelle_Markup.ML_NUMERAL -> get_color("red"),
wenzelm
parents: 46228
diff changeset
   289
      Isabelle_Markup.ML_CHAR -> get_color("#D2691E"),
wenzelm
parents: 46228
diff changeset
   290
      Isabelle_Markup.ML_STRING -> get_color("#D2691E"),
wenzelm
parents: 46228
diff changeset
   291
      Isabelle_Markup.ML_COMMENT -> get_color("#8B0000"),
wenzelm
parents: 46228
diff changeset
   292
      Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"),
wenzelm
parents: 46228
diff changeset
   293
      Isabelle_Markup.ANTIQ -> get_color("blue"))
wenzelm
parents: 46228
diff changeset
   294
wenzelm
parents: 46228
diff changeset
   295
  private val text_color_elements = Set.empty[String] ++ text_colors.keys
wenzelm
parents: 46228
diff changeset
   296
wenzelm
parents: 46228
diff changeset
   297
  def text_color(snapshot: Document.Snapshot, range: Text.Range, color: Color)
wenzelm
parents: 46228
diff changeset
   298
      : Stream[Text.Info[Color]] =
wenzelm
parents: 46228
diff changeset
   299
    snapshot.cumulate_markup(range, color, Some(text_color_elements),
wenzelm
parents: 46228
diff changeset
   300
      {
wenzelm
parents: 46228
diff changeset
   301
        case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
wenzelm
parents: 46228
diff changeset
   302
        if text_colors.isDefinedAt(m) => text_colors(m)
wenzelm
parents: 46228
diff changeset
   303
      })
wenzelm
parents: 46228
diff changeset
   304
wenzelm
parents: 46228
diff changeset
   305
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   306
  /* token markup -- text styles */
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   307
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   308
  private val command_style: Map[String, Byte] =
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   309
  {
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   310
    import JEditToken._
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   311
    Map[String, Byte](
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   312
      Keyword.THY_END -> KEYWORD2,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   313
      Keyword.THY_SCRIPT -> LABEL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   314
      Keyword.PRF_SCRIPT -> LABEL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   315
      Keyword.PRF_ASM -> KEYWORD3,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   316
      Keyword.PRF_ASM_GOAL -> KEYWORD3
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   317
    ).withDefaultValue(KEYWORD1)
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   318
  }
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   319
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   320
  private val token_style: Map[Token.Kind.Value, Byte] =
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   321
  {
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   322
    import JEditToken._
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   323
    Map[Token.Kind.Value, Byte](
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   324
      Token.Kind.KEYWORD -> KEYWORD2,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   325
      Token.Kind.IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   326
      Token.Kind.LONG_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   327
      Token.Kind.SYM_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   328
      Token.Kind.VAR -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   329
      Token.Kind.TYPE_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   330
      Token.Kind.TYPE_VAR -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   331
      Token.Kind.NAT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   332
      Token.Kind.FLOAT -> NULL,
43431
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   333
      Token.Kind.STRING -> LITERAL1,
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   334
      Token.Kind.ALT_STRING -> LITERAL2,
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   335
      Token.Kind.VERBATIM -> COMMENT3,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   336
      Token.Kind.SPACE -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   337
      Token.Kind.COMMENT -> COMMENT1,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   338
      Token.Kind.UNPARSED -> INVALID
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   339
    ).withDefaultValue(NULL)
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   340
  }
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   341
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   342
  def token_markup(syntax: Outer_Syntax, token: Token): Byte =
43430
1ed88ddf1268 more uniform treatment of "keyword" vs. "operator";
wenzelm
parents: 43418
diff changeset
   343
    if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
1ed88ddf1268 more uniform treatment of "keyword" vs. "operator";
wenzelm
parents: 43418
diff changeset
   344
    else if (token.is_operator) JEditToken.OPERATOR
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   345
    else token_style(token.kind)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   346
}