src/Tools/jEdit/src/jedit/isabelle_markup.scala
author wenzelm
Tue Sep 07 23:06:52 2010 +0200 (2010-09-07)
changeset 39178 83e9f3ccea9f
child 39179 591bbab9ef59
permissions -rw-r--r--
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm@39178
     1
/*  Title:      Tools/jEdit/src/jedit/isabelle_markup.scala
wenzelm@39178
     2
    Author:     Makarius
wenzelm@39178
     3
wenzelm@39178
     4
Isabelle specific physical rendering and markup selection.
wenzelm@39178
     5
*/
wenzelm@39178
     6
wenzelm@39178
     7
package isabelle.jedit
wenzelm@39178
     8
wenzelm@39178
     9
wenzelm@39178
    10
import isabelle._
wenzelm@39178
    11
wenzelm@39178
    12
import java.awt.Color
wenzelm@39178
    13
wenzelm@39178
    14
import org.gjt.sp.jedit.GUIUtilities
wenzelm@39178
    15
wenzelm@39178
    16
wenzelm@39178
    17
object Isabelle_Markup
wenzelm@39178
    18
{
wenzelm@39178
    19
  /* physical rendering */
wenzelm@39178
    20
wenzelm@39178
    21
  val outdated_color = new Color(240, 240, 240)
wenzelm@39178
    22
  val unfinished_color = new Color(255, 228, 225)
wenzelm@39178
    23
wenzelm@39178
    24
  val regular_color = new Color(192, 192, 192)
wenzelm@39178
    25
  val warning_color = new Color(255, 168, 0)
wenzelm@39178
    26
  val error_color = new Color(255, 80, 80)
wenzelm@39178
    27
  val bad_color = new Color(255, 204, 153, 100)
wenzelm@39178
    28
wenzelm@39178
    29
  val warning_icon = GUIUtilities.loadIcon("16x16/status/dialog-warning.png")
wenzelm@39178
    30
  val error_icon = GUIUtilities.loadIcon("16x16/status/dialog-error.png")
wenzelm@39178
    31
wenzelm@39178
    32
wenzelm@39178
    33
  /* command status */
wenzelm@39178
    34
wenzelm@39178
    35
  def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
wenzelm@39178
    36
  {
wenzelm@39178
    37
    val state = snapshot.state(command)
wenzelm@39178
    38
    if (snapshot.is_outdated) Some(outdated_color)
wenzelm@39178
    39
    else
wenzelm@39178
    40
      Isar_Document.command_status(state.status) match {
wenzelm@39178
    41
        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
wenzelm@39178
    42
        case Isar_Document.Unprocessed => Some(unfinished_color)
wenzelm@39178
    43
        case _ => None
wenzelm@39178
    44
      }
wenzelm@39178
    45
  }
wenzelm@39178
    46
wenzelm@39178
    47
  def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
wenzelm@39178
    48
  {
wenzelm@39178
    49
    val state = snapshot.state(command)
wenzelm@39178
    50
    if (snapshot.is_outdated) None
wenzelm@39178
    51
    else
wenzelm@39178
    52
      Isar_Document.command_status(state.status) match {
wenzelm@39178
    53
        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
wenzelm@39178
    54
        case Isar_Document.Unprocessed => Some(unfinished_color)
wenzelm@39178
    55
        case Isar_Document.Failed => Some(error_color)
wenzelm@39178
    56
        case _ => None
wenzelm@39178
    57
      }
wenzelm@39178
    58
  }
wenzelm@39178
    59
wenzelm@39178
    60
wenzelm@39178
    61
  /* markup selectors */
wenzelm@39178
    62
wenzelm@39178
    63
  private val subexp_include =
wenzelm@39178
    64
    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING)
wenzelm@39178
    65
wenzelm@39178
    66
  val subexp: Markup_Tree.Select[(Text.Range, Color)] =
wenzelm@39178
    67
  {
wenzelm@39178
    68
    case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
wenzelm@39178
    69
      (range, Color.black)
wenzelm@39178
    70
  }
wenzelm@39178
    71
wenzelm@39178
    72
  val message: Markup_Tree.Select[Color] =
wenzelm@39178
    73
  {
wenzelm@39178
    74
    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
wenzelm@39178
    75
    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
wenzelm@39178
    76
    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
wenzelm@39178
    77
  }
wenzelm@39178
    78
wenzelm@39178
    79
  val background: Markup_Tree.Select[Color] =
wenzelm@39178
    80
  {
wenzelm@39178
    81
    case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
wenzelm@39178
    82
  }
wenzelm@39178
    83
wenzelm@39178
    84
  val box: Markup_Tree.Select[Color] =
wenzelm@39178
    85
  {
wenzelm@39178
    86
    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => regular_color
wenzelm@39178
    87
  }
wenzelm@39178
    88
wenzelm@39178
    89
  val tooltip: Markup_Tree.Select[String] =
wenzelm@39178
    90
  {
wenzelm@39178
    91
    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
wenzelm@39178
    92
      Pretty.string_of(List(Pretty.block(body)), margin = 40)
wenzelm@39178
    93
    case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
wenzelm@39178
    94
    case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
wenzelm@39178
    95
    case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
wenzelm@39178
    96
    case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
wenzelm@39178
    97
  }
wenzelm@39178
    98
}