src/Tools/jEdit/src/isabelle_rendering.scala
author wenzelm
Wed Mar 14 15:37:51 2012 +0100 (2012-03-14)
changeset 46920 5f44c8bea84e
parent 46235 e4e0b5190f3d
child 47540 1de8a8b1ae79
permissions -rw-r--r--
more explicit indication of swing thread context;
     1 /*  Title:      Tools/jEdit/src/isabelle_rendering.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 import javax.swing.Icon
    14 
    15 import org.lobobrowser.util.gui.ColorFactory
    16 import org.gjt.sp.jedit.syntax.{Token => JEditToken}
    17 
    18 import scala.collection.immutable.SortedMap
    19 
    20 
    21 object Isabelle_Rendering
    22 {
    23   /* physical rendering */
    24 
    25   // see http://www.w3schools.com/css/css_colornames.asp
    26 
    27   def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
    28 
    29   val outdated_color = new Color(238, 227, 227)
    30   val unprocessed_color = new Color(255, 160, 160)
    31   val unprocessed1_color = new Color(255, 160, 160, 50)
    32   val running_color = new Color(97, 0, 97)
    33   val running1_color = new Color(97, 0, 97, 100)
    34 
    35   val light_color = new Color(240, 240, 240)
    36   val writeln_color = new Color(192, 192, 192)
    37   val warning_color = new Color(255, 140, 0)
    38   val error_color = new Color(178, 34, 34)
    39   val error1_color = new Color(178, 34, 34, 50)
    40   val bad_color = new Color(255, 106, 106, 100)
    41   val hilite_color = new Color(255, 204, 102, 100)
    42 
    43   val quoted_color = new Color(139, 139, 139, 25)
    44   val subexp_color = new Color(80, 80, 80, 50)
    45 
    46   val keyword1_color = get_color("#006699")
    47   val keyword2_color = get_color("#009966")
    48 
    49   private val writeln_pri = 1
    50   private val warning_pri = 2
    51   private val legacy_pri = 3
    52   private val error_pri = 4
    53 
    54 
    55   /* command overview */
    56 
    57   def overview_color(snapshot: Document.Snapshot, range: Text.Range): Option[Color] =
    58   {
    59     if (snapshot.is_outdated) None
    60     else {
    61       val results =
    62         snapshot.cumulate_markup[(Protocol.Status, Int)](
    63           range, (Protocol.Status.init, 0),
    64           Some(Protocol.command_status_markup + Isabelle_Markup.WARNING + Isabelle_Markup.ERROR),
    65           {
    66             case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
    67               if (markup.name == Isabelle_Markup.WARNING) (status, pri max warning_pri)
    68               else if (markup.name == Isabelle_Markup.ERROR) (status, pri max error_pri)
    69               else (Protocol.command_status(status, markup), pri)
    70           })
    71       if (results.isEmpty) None
    72       else {
    73         val (status, pri) =
    74           ((Protocol.Status.init, 0) /: results) {
    75             case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) }
    76 
    77         if (pri == warning_pri) Some(warning_color)
    78         else if (pri == error_pri) Some(error_color)
    79         else if (status.is_unprocessed) Some(unprocessed_color)
    80         else if (status.is_running) Some(running_color)
    81         else if (status.is_failed) Some(error_color)
    82         else None
    83       }
    84     }
    85   }
    86 
    87 
    88   /* markup selectors */
    89 
    90   private val subexp_include =
    91     Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
    92       Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
    93       Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM, Isabelle_Markup.BOUND,
    94       Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE,
    95       Isabelle_Markup.DOC_SOURCE)
    96 
    97   def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Color]] =
    98   {
    99     snapshot.select_markup(range, Some(subexp_include),
   100         {
   101           case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
   102             Text.Info(snapshot.convert(range), subexp_color)
   103         }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   104   }
   105 
   106 
   107   def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
   108   {
   109     val msgs =
   110       snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
   111         Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
   112         {
   113           case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
   114           if markup == Isabelle_Markup.WRITELN ||
   115               markup == Isabelle_Markup.WARNING ||
   116               markup == Isabelle_Markup.ERROR =>
   117             msgs + (serial ->
   118               Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
   119         }).toList.flatMap(_.info)
   120     if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2)))
   121   }
   122 
   123 
   124   private val tooltips: Map[String, String] =
   125     Map(
   126       Isabelle_Markup.SORT -> "sort",
   127       Isabelle_Markup.TYP -> "type",
   128       Isabelle_Markup.TERM -> "term",
   129       Isabelle_Markup.PROP -> "proposition",
   130       Isabelle_Markup.TOKEN_RANGE -> "inner syntax token",
   131       Isabelle_Markup.FREE -> "free variable",
   132       Isabelle_Markup.SKOLEM -> "skolem variable",
   133       Isabelle_Markup.BOUND -> "bound variable",
   134       Isabelle_Markup.VAR -> "schematic variable",
   135       Isabelle_Markup.TFREE -> "free type variable",
   136       Isabelle_Markup.TVAR -> "schematic type variable",
   137       Isabelle_Markup.ML_SOURCE -> "ML source",
   138       Isabelle_Markup.DOC_SOURCE -> "document source")
   139 
   140   private val tooltip_elements =
   141     Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING) ++
   142     tooltips.keys
   143 
   144   private def string_of_typing(kind: String, body: XML.Body): String =
   145     Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
   146       margin = Isabelle.Int_Property("tooltip-margin"))
   147 
   148   def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
   149   {
   150     def add(prev: Text.Info[List[String]], r: Text.Range, s: String) =
   151       if (prev.range == r) Text.Info(r, s :: prev.info) else Text.Info(r, List(s))
   152 
   153     val tips =
   154       snapshot.cumulate_markup[Text.Info[List[String]]](
   155         range, Text.Info(range, Nil), Some(tooltip_elements),
   156         {
   157           case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) =>
   158             add(prev, r, kind + " " + quote(name))
   159           case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body))) =>
   160             add(prev, r, string_of_typing("::", body))
   161           case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) =>
   162             add(prev, r, string_of_typing("ML:", body))
   163           case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
   164           if tooltips.isDefinedAt(name) => add (prev, r, tooltips(name))
   165         }).toList.flatMap(_.info.info)
   166 
   167     if (tips.isEmpty) None else Some(cat_lines(tips))
   168   }
   169 
   170 
   171   private val gutter_icons = Map(
   172     warning_pri -> Isabelle.load_icon("16x16/status/dialog-information.png"),
   173     legacy_pri -> Isabelle.load_icon("16x16/status/dialog-warning.png"),
   174     error_pri -> Isabelle.load_icon("16x16/status/dialog-error.png"))
   175 
   176   def gutter_message(snapshot: Document.Snapshot, range: Text.Range): Option[Icon] =
   177   {
   178     val results =
   179       snapshot.cumulate_markup[Int](range, 0,
   180         Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
   181         {
   182           case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body))) =>
   183             body match {
   184               case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => pri max legacy_pri
   185               case _ => pri max warning_pri
   186             }
   187           case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _))) =>
   188             pri max error_pri
   189         })
   190     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
   191     gutter_icons.get(pri)
   192   }
   193 
   194 
   195   private val squiggly_colors = Map(
   196     writeln_pri -> writeln_color,
   197     warning_pri -> warning_color,
   198     error_pri -> error_color)
   199 
   200   def squiggly_underline(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
   201   {
   202     val results =
   203       snapshot.cumulate_markup[Int](range, 0,
   204         Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
   205         {
   206           case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) =>
   207             name match {
   208               case Isabelle_Markup.WRITELN => pri max writeln_pri
   209               case Isabelle_Markup.WARNING => pri max warning_pri
   210               case Isabelle_Markup.ERROR => pri max error_pri
   211               case _ => pri
   212             }
   213         })
   214     for {
   215       Text.Info(r, pri) <- results
   216       color <- squiggly_colors.get(pri)
   217     } yield Text.Info(r, color)
   218   }
   219 
   220 
   221   def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
   222   {
   223     if (snapshot.is_outdated) Stream(Text.Info(range, outdated_color))
   224     else
   225       for {
   226         Text.Info(r, result) <-
   227           snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
   228             range, (Some(Protocol.Status.init), None),
   229             Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE),
   230             {
   231               case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
   232               if (Protocol.command_status_markup(markup.name)) =>
   233                 (Some(Protocol.command_status(status, markup)), color)
   234               case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
   235                 (None, Some(bad_color))
   236               case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
   237                 (None, Some(hilite_color))
   238             })
   239         color <-
   240           (result match {
   241             case (Some(status), _) =>
   242               if (status.is_running) Some(running1_color)
   243               else if (status.is_unprocessed) Some(unprocessed1_color)
   244               else None
   245             case (_, opt_color) => opt_color
   246           })
   247       } yield Text.Info(r, color)
   248   }
   249 
   250 
   251   def background2(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
   252     snapshot.select_markup(range,
   253       Some(Set(Isabelle_Markup.TOKEN_RANGE)),
   254       {
   255         case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
   256       })
   257 
   258 
   259   def foreground(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
   260     snapshot.select_markup(range,
   261       Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)),
   262       {
   263         case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
   264         case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
   265         case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
   266       })
   267 
   268 
   269   private val text_colors: Map[String, Color] =
   270     Map(
   271       Isabelle_Markup.STRING -> get_color("black"),
   272       Isabelle_Markup.ALTSTRING -> get_color("black"),
   273       Isabelle_Markup.VERBATIM -> get_color("black"),
   274       Isabelle_Markup.LITERAL -> keyword1_color,
   275       Isabelle_Markup.DELIMITER -> get_color("black"),
   276       Isabelle_Markup.TFREE -> get_color("#A020F0"),
   277       Isabelle_Markup.TVAR -> get_color("#A020F0"),
   278       Isabelle_Markup.FREE -> get_color("blue"),
   279       Isabelle_Markup.SKOLEM -> get_color("#D2691E"),
   280       Isabelle_Markup.BOUND -> get_color("green"),
   281       Isabelle_Markup.VAR -> get_color("#00009B"),
   282       Isabelle_Markup.INNER_STRING -> get_color("#D2691E"),
   283       Isabelle_Markup.INNER_COMMENT -> get_color("#8B0000"),
   284       Isabelle_Markup.DYNAMIC_FACT -> get_color("#7BA428"),
   285       Isabelle_Markup.ML_KEYWORD -> keyword1_color,
   286       Isabelle_Markup.ML_DELIMITER -> get_color("black"),
   287       Isabelle_Markup.ML_NUMERAL -> get_color("red"),
   288       Isabelle_Markup.ML_CHAR -> get_color("#D2691E"),
   289       Isabelle_Markup.ML_STRING -> get_color("#D2691E"),
   290       Isabelle_Markup.ML_COMMENT -> get_color("#8B0000"),
   291       Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"),
   292       Isabelle_Markup.ANTIQ -> get_color("blue"))
   293 
   294   private val text_color_elements = Set.empty[String] ++ text_colors.keys
   295 
   296   def text_color(snapshot: Document.Snapshot, range: Text.Range, color: Color)
   297       : Stream[Text.Info[Color]] =
   298     snapshot.cumulate_markup(range, color, Some(text_color_elements),
   299       {
   300         case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
   301         if text_colors.isDefinedAt(m) => text_colors(m)
   302       })
   303 
   304 
   305   /* token markup -- text styles */
   306 
   307   private val command_style: Map[String, Byte] =
   308   {
   309     import JEditToken._
   310     Map[String, Byte](
   311       Keyword.THY_END -> KEYWORD2,
   312       Keyword.THY_SCRIPT -> LABEL,
   313       Keyword.PRF_SCRIPT -> LABEL,
   314       Keyword.PRF_ASM -> KEYWORD3,
   315       Keyword.PRF_ASM_GOAL -> KEYWORD3
   316     ).withDefaultValue(KEYWORD1)
   317   }
   318 
   319   private val token_style: Map[Token.Kind.Value, Byte] =
   320   {
   321     import JEditToken._
   322     Map[Token.Kind.Value, Byte](
   323       Token.Kind.KEYWORD -> KEYWORD2,
   324       Token.Kind.IDENT -> NULL,
   325       Token.Kind.LONG_IDENT -> NULL,
   326       Token.Kind.SYM_IDENT -> NULL,
   327       Token.Kind.VAR -> NULL,
   328       Token.Kind.TYPE_IDENT -> NULL,
   329       Token.Kind.TYPE_VAR -> NULL,
   330       Token.Kind.NAT -> NULL,
   331       Token.Kind.FLOAT -> NULL,
   332       Token.Kind.STRING -> LITERAL1,
   333       Token.Kind.ALT_STRING -> LITERAL2,
   334       Token.Kind.VERBATIM -> COMMENT3,
   335       Token.Kind.SPACE -> NULL,
   336       Token.Kind.COMMENT -> COMMENT1,
   337       Token.Kind.UNPARSED -> INVALID
   338     ).withDefaultValue(NULL)
   339   }
   340 
   341   def token_markup(syntax: Outer_Syntax, token: Token): Byte =
   342     if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
   343     else if (token.is_operator) JEditToken.OPERATOR
   344     else token_style(token.kind)
   345 }