src/Tools/jEdit/src/isabelle_rendering.scala
author wenzelm
Sun, 15 Jan 2012 19:09:03 +0100
changeset 46227 4aa84f84d5e8
parent 46224 9cb98d34f593
child 46228 302d3ecff25d
permissions -rw-r--r--
more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;
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
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
    90
  def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
46199
wenzelm
parents: 46198
diff changeset
    91
  {
wenzelm
parents: 46198
diff changeset
    92
    val msgs =
wenzelm
parents: 46198
diff changeset
    93
      snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
wenzelm
parents: 46198
diff changeset
    94
        Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
wenzelm
parents: 46198
diff changeset
    95
        {
wenzelm
parents: 46198
diff changeset
    96
          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
wenzelm
parents: 46198
diff changeset
    97
          if markup == Isabelle_Markup.WRITELN ||
wenzelm
parents: 46198
diff changeset
    98
              markup == Isabelle_Markup.WARNING ||
wenzelm
parents: 46198
diff changeset
    99
              markup == Isabelle_Markup.ERROR =>
wenzelm
parents: 46198
diff changeset
   100
            msgs + (serial ->
wenzelm
parents: 46198
diff changeset
   101
              Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
wenzelm
parents: 46198
diff changeset
   102
        }).toList.flatMap(_.info)
wenzelm
parents: 46198
diff changeset
   103
    if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2)))
wenzelm
parents: 46198
diff changeset
   104
  }
39740
0294948ba962 basic support for message popups via HTML_Panel;
wenzelm
parents: 39704
diff changeset
   105
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
   106
  private val gutter_icons = Map(
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
   107
    warning_pri -> Isabelle.load_icon("16x16/status/dialog-information.png"),
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
   108
    legacy_pri -> Isabelle.load_icon("16x16/status/dialog-warning.png"),
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
   109
    error_pri -> Isabelle.load_icon("16x16/status/dialog-error.png"))
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
   110
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   111
  def gutter_message(snapshot: Document.Snapshot, range: Text.Range): Option[Icon] =
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
   112
  {
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
   113
    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
   114
      snapshot.cumulate_markup[Int](range, 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
   115
        Some(Set(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
   116
        {
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
   117
          case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body))) =>
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
   118
            body match {
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
   119
              case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => pri max legacy_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
   120
              case _ => 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
   121
            }
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
   122
          case (pri, Text.Info(_, XML.Elem(Markup(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
   123
            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
   124
        })
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
   125
    val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
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
   126
    gutter_icons.get(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
   127
  }
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
   128
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
   129
  private val squiggly_colors = Map(
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
   130
    writeln_pri -> writeln_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
   131
    warning_pri -> 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
   132
    error_pri -> error_color)
39181
2257eded8323 Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents: 39179
diff changeset
   133
46224
9cb98d34f593 tuned signature;
wenzelm
parents: 46208
diff changeset
   134
  def squiggly_underline(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[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
   135
  {
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
   136
    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
   137
      snapshot.cumulate_markup[Int](range, 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
   138
        Some(Set(Isabelle_Markup.WRITELN, 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
   139
        {
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
   140
          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) =>
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
   141
            name match {
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
   142
              case Isabelle_Markup.WRITELN => pri max writeln_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
   143
              case Isabelle_Markup.WARNING => 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
   144
              case Isabelle_Markup.ERROR => 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
   145
              case _ => 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
   146
            }
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
   147
        })
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
   148
    for {
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
   149
      Text.Info(r, pri) <- 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
   150
      color <- squiggly_colors.get(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
   151
    } yield Text.Info(r, 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
   152
  }
46224
9cb98d34f593 tuned signature;
wenzelm
parents: 46208
diff changeset
   153
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   154
  def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   155
    for {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   156
      Text.Info(r, result) <-
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   157
        snapshot.cumulate_markup[(Option[Protocol.Status], Option[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
   158
          range, (Some(Protocol.Status.init), None),
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   159
          Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE),
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   160
          {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   161
            case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   162
            if (Protocol.command_status_markup(markup.name)) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   163
              (Some(Protocol.command_status(status, markup)), color)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   164
            case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   165
              (None, Some(bad_color))
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   166
            case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   167
              (None, Some(hilite_color))
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   168
          })
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   169
      color <-
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   170
        (result match {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   171
          case (Some(status), _) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   172
            if (status.is_running) Some(running1_color)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   173
            else if (status.is_unprocessed) Some(unprocessed1_color)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   174
            else None
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   175
          case (_, opt_color) => opt_color
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   176
        })
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   177
    } yield Text.Info(r, color)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   178
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   179
  def background2(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
46198
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   180
    snapshot.select_markup(range,
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   181
      Some(Set(Isabelle_Markup.TOKEN_RANGE)),
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   182
      {
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   183
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   184
      })
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   185
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   186
  def foreground(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
46198
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   187
    snapshot.select_markup(range,
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   188
      Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)),
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   189
      {
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   190
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   191
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   192
        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   193
      })
44545
3c40007aa031 transparent foreground color for quoted entities;
wenzelm
parents: 44181
diff changeset
   194
43434
2fd41645813d tuned signature;
wenzelm
parents: 43432
diff changeset
   195
  private val text_colors: Map[String, Color] =
43386
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   196
    Map(
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   197
      Isabelle_Markup.STRING -> get_color("black"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   198
      Isabelle_Markup.ALTSTRING -> get_color("black"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   199
      Isabelle_Markup.VERBATIM -> get_color("black"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   200
      Isabelle_Markup.LITERAL -> keyword1_color,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   201
      Isabelle_Markup.DELIMITER -> get_color("black"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   202
      Isabelle_Markup.TFREE -> get_color("#A020F0"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   203
      Isabelle_Markup.TVAR -> get_color("#A020F0"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   204
      Isabelle_Markup.FREE -> get_color("blue"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   205
      Isabelle_Markup.SKOLEM -> get_color("#D2691E"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   206
      Isabelle_Markup.BOUND -> get_color("green"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   207
      Isabelle_Markup.VAR -> get_color("#00009B"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   208
      Isabelle_Markup.INNER_STRING -> get_color("#D2691E"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   209
      Isabelle_Markup.INNER_COMMENT -> get_color("#8B0000"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   210
      Isabelle_Markup.DYNAMIC_FACT -> get_color("#7BA428"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   211
      Isabelle_Markup.ML_KEYWORD -> keyword1_color,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   212
      Isabelle_Markup.ML_DELIMITER -> get_color("black"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   213
      Isabelle_Markup.ML_NUMERAL -> get_color("red"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   214
      Isabelle_Markup.ML_CHAR -> get_color("#D2691E"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   215
      Isabelle_Markup.ML_STRING -> get_color("#D2691E"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   216
      Isabelle_Markup.ML_COMMENT -> get_color("#8B0000"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   217
      Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"),
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   218
      Isabelle_Markup.ANTIQ -> get_color("blue"))
43386
4e78dd88c64f more foreground markup, using actual CSS color names;
wenzelm
parents: 43377
diff changeset
   219
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   220
  private val text_color_elements = Set.empty[String] ++ text_colors.keys
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   221
46197
e4da482283ef tuned text_color: cumulate with explicit default color;
wenzelm
parents: 46196
diff changeset
   222
  def text_color(snapshot: Document.Snapshot, range: Text.Range, color: Color)
e4da482283ef tuned text_color: cumulate with explicit default color;
wenzelm
parents: 46196
diff changeset
   223
      : Stream[Text.Info[Color]] =
e4da482283ef tuned text_color: cumulate with explicit default color;
wenzelm
parents: 46196
diff changeset
   224
    snapshot.cumulate_markup(range, color, Some(text_color_elements),
45468
33e946d3f449 tuned signature;
wenzelm
parents: 45467
diff changeset
   225
      {
46197
e4da482283ef tuned text_color: cumulate with explicit default color;
wenzelm
parents: 46196
diff changeset
   226
        case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
45474
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45468
diff changeset
   227
        if text_colors.isDefinedAt(m) => text_colors(m)
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   228
      })
43376
0f6880c1c759 some direct text foreground painting, instead of token marking;
wenzelm
parents: 43282
diff changeset
   229
43431
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   230
  private val tooltips: Map[String, String] =
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   231
    Map(
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   232
      Isabelle_Markup.SORT -> "sort",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   233
      Isabelle_Markup.TYP -> "type",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   234
      Isabelle_Markup.TERM -> "term",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   235
      Isabelle_Markup.PROP -> "proposition",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   236
      Isabelle_Markup.TOKEN_RANGE -> "inner syntax token",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   237
      Isabelle_Markup.FREE -> "free variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   238
      Isabelle_Markup.SKOLEM -> "skolem variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   239
      Isabelle_Markup.BOUND -> "bound variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   240
      Isabelle_Markup.VAR -> "schematic variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   241
      Isabelle_Markup.TFREE -> "free type variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   242
      Isabelle_Markup.TVAR -> "schematic type variable",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   243
      Isabelle_Markup.ML_SOURCE -> "ML source",
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   244
      Isabelle_Markup.DOC_SOURCE -> "document source")
43431
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   245
45445
41e641a870de pass term positions into check phase, where resulting types are reported accordingly, and eventually shown as tooltips;
wenzelm
parents: 44866
diff changeset
   246
  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
   247
    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
   248
      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
   249
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   250
  def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   251
  {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   252
    val tip1 =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   253
      snapshot.select_markup(range,
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   254
        Some(Set(Isabelle_Markup.ENTITY, Isabelle_Markup.ML_TYPING) ++ tooltips.keys),
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   255
        {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   256
          case Text.Info(_, XML.Elem(Isabelle_Markup.Entity(kind, name), _)) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   257
            kind + " " + quote(name)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   258
          case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body)) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   259
            string_of_typing("ML:", body)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   260
          case Text.Info(_, XML.Elem(Markup(name, _), _))
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   261
          if tooltips.isDefinedAt(name) => tooltips(name)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   262
        })
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   263
    val tip2 =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   264
      snapshot.select_markup(range, Some(Set(Isabelle_Markup.TYPING)),
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   265
        {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   266
          case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body)) =>
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   267
            string_of_typing("::", body)
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   268
        })
42302
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   269
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   270
    val tips =
46198
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   271
      (tip1 match { case Text.Info(_, text) #:: _ => List(text) case _ => Nil }) :::
cd040c5772de improved select_markup: include filtering of defined results;
wenzelm
parents: 46197
diff changeset
   272
      (tip2 match { case Text.Info(_, text) #:: _ => List(text) case _ => Nil })
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   273
46196
805de058722b added cat_lines convenience;
wenzelm
parents: 46178
diff changeset
   274
    if (tips.isEmpty) None else Some(cat_lines(tips))
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   275
  }
45460
dcd02d1a25d7 more tooltip content;
wenzelm
parents: 45454
diff changeset
   276
42302
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   277
  private val subexp_include =
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   278
    Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   279
      Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   280
      Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   281
      Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE,
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45665
diff changeset
   282
      Isabelle_Markup.DOC_SOURCE)
42302
d08aab6663b8 present type variables;
wenzelm
parents: 42283
diff changeset
   283
46205
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46199
diff changeset
   284
  def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Color]] =
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   285
  {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   286
    snapshot.select_markup(range, Some(subexp_include),
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   287
        {
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   288
          case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
46205
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46199
diff changeset
   289
            Text.Info(snapshot.convert(range), subexp_color)
07e334ad2e2a ignore empty gfx_range;
wenzelm
parents: 46199
diff changeset
   290
        }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46166
diff changeset
   291
  }
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   292
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   293
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   294
  /* token markup -- text styles */
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   295
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   296
  private val command_style: Map[String, Byte] =
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   297
  {
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   298
    import JEditToken._
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   299
    Map[String, Byte](
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   300
      Keyword.THY_END -> KEYWORD2,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   301
      Keyword.THY_SCRIPT -> LABEL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   302
      Keyword.PRF_SCRIPT -> LABEL,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   303
      Keyword.PRF_ASM -> KEYWORD3,
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   304
      Keyword.PRF_ASM_GOAL -> KEYWORD3
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   305
    ).withDefaultValue(KEYWORD1)
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   306
  }
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   307
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   308
  private val token_style: Map[Token.Kind.Value, Byte] =
39179
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._
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   311
    Map[Token.Kind.Value, Byte](
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   312
      Token.Kind.KEYWORD -> KEYWORD2,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   313
      Token.Kind.IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   314
      Token.Kind.LONG_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   315
      Token.Kind.SYM_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   316
      Token.Kind.VAR -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   317
      Token.Kind.TYPE_IDENT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   318
      Token.Kind.TYPE_VAR -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   319
      Token.Kind.NAT -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   320
      Token.Kind.FLOAT -> NULL,
43431
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   321
      Token.Kind.STRING -> LITERAL1,
f3d5cecfecdc tuned markup;
wenzelm
parents: 43430
diff changeset
   322
      Token.Kind.ALT_STRING -> LITERAL2,
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   323
      Token.Kind.VERBATIM -> COMMENT3,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   324
      Token.Kind.SPACE -> NULL,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   325
      Token.Kind.COMMENT -> COMMENT1,
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   326
      Token.Kind.UNPARSED -> INVALID
39179
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   327
    ).withDefaultValue(NULL)
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   328
  }
591bbab9ef59 moved token markup tables to isabelle_markup.scala;
wenzelm
parents: 39178
diff changeset
   329
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   330
  def token_markup(syntax: Outer_Syntax, token: Token): Byte =
43430
1ed88ddf1268 more uniform treatment of "keyword" vs. "operator";
wenzelm
parents: 43418
diff changeset
   331
    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
   332
    else if (token.is_operator) JEditToken.OPERATOR
43414
f0770743b7ec static token markup, based on outer syntax only;
wenzelm
parents: 43394
diff changeset
   333
    else token_style(token.kind)
39178
83e9f3ccea9f concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff changeset
   334
}