src/Tools/jEdit/src/jedit/isabelle_markup.scala
author wenzelm
Tue Sep 07 23:59:14 2010 +0200 (2010-09-07)
changeset 39181 2257eded8323
parent 39179 591bbab9ef59
child 39241 e9a442606db3
permissions -rw-r--r--
Document_View: select gutter message icons from markup over line range, not full range results;
tuned;
     1 /*  Title:      Tools/jEdit/src/jedit/isabelle_markup.scala
     2     Author:     Makarius
     3 
     4 Isabelle specific physical rendering and markup selection.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.awt.Color
    13 
    14 import org.gjt.sp.jedit.GUIUtilities
    15 import org.gjt.sp.jedit.syntax.Token
    16 
    17 
    18 object Isabelle_Markup
    19 {
    20   /* physical rendering */
    21 
    22   val outdated_color = new Color(240, 240, 240)
    23   val unfinished_color = new Color(255, 228, 225)
    24 
    25   val regular_color = new Color(192, 192, 192)
    26   val warning_color = new Color(255, 168, 0)
    27   val error_color = new Color(255, 80, 80)
    28   val bad_color = new Color(255, 204, 153, 100)
    29 
    30   class Icon(val priority: Int, val icon: javax.swing.Icon)
    31   {
    32     def >= (that: Icon): Boolean = this.priority >= that.priority
    33   }
    34   val warning_icon = new Icon(1, GUIUtilities.loadIcon("16x16/status/dialog-warning.png"))
    35   val error_icon = new Icon(2, GUIUtilities.loadIcon("16x16/status/dialog-error.png"))
    36 
    37 
    38   /* command status */
    39 
    40   def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
    41   {
    42     val state = snapshot.state(command)
    43     if (snapshot.is_outdated) Some(outdated_color)
    44     else
    45       Isar_Document.command_status(state.status) match {
    46         case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
    47         case Isar_Document.Unprocessed => Some(unfinished_color)
    48         case _ => None
    49       }
    50   }
    51 
    52   def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
    53   {
    54     val state = snapshot.state(command)
    55     if (snapshot.is_outdated) None
    56     else
    57       Isar_Document.command_status(state.status) match {
    58         case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
    59         case Isar_Document.Unprocessed => Some(unfinished_color)
    60         case Isar_Document.Failed => Some(error_color)
    61         case _ => None
    62       }
    63   }
    64 
    65 
    66   /* markup selectors */
    67 
    68   private val subexp_include =
    69     Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING)
    70 
    71   val subexp: Markup_Tree.Select[(Text.Range, Color)] =
    72   {
    73     case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
    74       (range, Color.black)
    75   }
    76 
    77   val message: Markup_Tree.Select[Color] =
    78   {
    79     case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
    80     case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
    81     case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
    82   }
    83 
    84   val gutter_message: Markup_Tree.Select[Icon] =
    85   {
    86     case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
    87     case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
    88   }
    89 
    90   val background: Markup_Tree.Select[Color] =
    91   {
    92     case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
    93   }
    94 
    95   val box: Markup_Tree.Select[Color] =
    96   {
    97     case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => regular_color
    98   }
    99 
   100   val tooltip: Markup_Tree.Select[String] =
   101   {
   102     case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
   103       Pretty.string_of(List(Pretty.block(body)), margin = 40)
   104     case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
   105     case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
   106     case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
   107     case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
   108   }
   109 
   110 
   111   /* token markup -- text styles */
   112 
   113   private val command_style: Map[String, Byte] =
   114   {
   115     import Token._
   116     Map[String, Byte](
   117       Keyword.THY_END -> KEYWORD2,
   118       Keyword.THY_SCRIPT -> LABEL,
   119       Keyword.PRF_SCRIPT -> LABEL,
   120       Keyword.PRF_ASM -> KEYWORD3,
   121       Keyword.PRF_ASM_GOAL -> KEYWORD3
   122     ).withDefaultValue(KEYWORD1)
   123   }
   124 
   125   private val token_style: Map[String, Byte] =
   126   {
   127     import Token._
   128     Map[String, Byte](
   129       // logical entities
   130       Markup.TCLASS -> NULL,
   131       Markup.TYCON -> NULL,
   132       Markup.FIXED_DECL -> FUNCTION,
   133       Markup.FIXED -> NULL,
   134       Markup.CONST_DECL -> FUNCTION,
   135       Markup.CONST -> NULL,
   136       Markup.FACT_DECL -> FUNCTION,
   137       Markup.FACT -> NULL,
   138       Markup.DYNAMIC_FACT -> LABEL,
   139       Markup.LOCAL_FACT_DECL -> FUNCTION,
   140       Markup.LOCAL_FACT -> NULL,
   141       // inner syntax
   142       Markup.TFREE -> NULL,
   143       Markup.FREE -> NULL,
   144       Markup.TVAR -> NULL,
   145       Markup.SKOLEM -> NULL,
   146       Markup.BOUND -> NULL,
   147       Markup.VAR -> NULL,
   148       Markup.NUM -> DIGIT,
   149       Markup.FLOAT -> DIGIT,
   150       Markup.XNUM -> DIGIT,
   151       Markup.XSTR -> LITERAL4,
   152       Markup.LITERAL -> OPERATOR,
   153       Markup.INNER_COMMENT -> COMMENT1,
   154       Markup.SORT -> NULL,
   155       Markup.TYP -> NULL,
   156       Markup.TERM -> NULL,
   157       Markup.PROP -> NULL,
   158       Markup.ATTRIBUTE -> NULL,
   159       Markup.METHOD -> NULL,
   160       // ML syntax
   161       Markup.ML_KEYWORD -> KEYWORD1,
   162       Markup.ML_DELIMITER -> OPERATOR,
   163       Markup.ML_IDENT -> NULL,
   164       Markup.ML_TVAR -> NULL,
   165       Markup.ML_NUMERAL -> DIGIT,
   166       Markup.ML_CHAR -> LITERAL1,
   167       Markup.ML_STRING -> LITERAL1,
   168       Markup.ML_COMMENT -> COMMENT1,
   169       Markup.ML_MALFORMED -> INVALID,
   170       // embedded source text
   171       Markup.ML_SOURCE -> COMMENT3,
   172       Markup.DOC_SOURCE -> COMMENT3,
   173       Markup.ANTIQ -> COMMENT4,
   174       Markup.ML_ANTIQ -> COMMENT4,
   175       Markup.DOC_ANTIQ -> COMMENT4,
   176       // outer syntax
   177       Markup.KEYWORD -> KEYWORD2,
   178       Markup.OPERATOR -> OPERATOR,
   179       Markup.COMMAND -> KEYWORD1,
   180       Markup.IDENT -> NULL,
   181       Markup.VERBATIM -> COMMENT3,
   182       Markup.COMMENT -> COMMENT1,
   183       Markup.CONTROL -> COMMENT3,
   184       Markup.MALFORMED -> INVALID,
   185       Markup.STRING -> LITERAL3,
   186       Markup.ALTSTRING -> LITERAL1
   187     ).withDefaultValue(NULL)
   188   }
   189 
   190   def tokens(syntax: Outer_Syntax): Markup_Tree.Select[Byte] =
   191   {
   192     case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
   193     if syntax.keyword_kind(name).isDefined => command_style(syntax.keyword_kind(name).get)
   194 
   195     case Text.Info(_, XML.Elem(Markup(name, _), _))
   196     if token_style(name) != Token.NULL => token_style(name)
   197   }
   198 }