src/Tools/jEdit/src/rendering.scala
author wenzelm
Sun Nov 25 19:55:42 2012 +0100 (2012-11-25 ago)
changeset 50202 ec0f2f8dbeb9
parent 50201 src/Tools/jEdit/src/isabelle_rendering.scala@c26369c9eda6
child 50205 788c8263e634
permissions -rw-r--r--
tuned file name;
     1 /*  Title:      Tools/jEdit/src/rendering.scala
     2     Author:     Makarius
     3 
     4 Isabelle-specific implementation of quasi-abstract rendering and
     5 markup interpretation.
     6 */
     7 
     8 package isabelle.jedit
     9 
    10 
    11 import isabelle._
    12 
    13 import java.awt.Color
    14 import javax.swing.Icon
    15 
    16 import org.gjt.sp.jedit.syntax.{Token => JEditToken}
    17 import org.gjt.sp.jedit.GUIUtilities
    18 
    19 import scala.collection.immutable.SortedMap
    20 
    21 
    22 object Rendering
    23 {
    24   def apply(snapshot: Document.Snapshot, options: Options): Rendering =
    25     new Rendering(snapshot, options)
    26 
    27 
    28   /* message priorities */
    29 
    30   private val writeln_pri = 1
    31   private val tracing_pri = 2
    32   private val warning_pri = 3
    33   private val legacy_pri = 4
    34   private val error_pri = 5
    35 
    36   private val message_pri = Map(
    37     Markup.WRITELN -> writeln_pri, Markup.WRITELN_MESSAGE -> writeln_pri,
    38     Markup.TRACING -> tracing_pri, Markup.TRACING_MESSAGE -> tracing_pri,
    39     Markup.WARNING -> warning_pri, Markup.WARNING_MESSAGE -> warning_pri,
    40     Markup.ERROR -> error_pri, Markup.ERROR_MESSAGE -> error_pri)
    41 
    42 
    43   /* icons */
    44 
    45   private def load_icon(name: String): Icon =
    46   {
    47     val icon = GUIUtilities.loadIcon(name)
    48     if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
    49     else icon
    50   }
    51 
    52   private val gutter_icons = Map(
    53     warning_pri -> load_icon("16x16/status/dialog-information.png"),
    54     legacy_pri -> load_icon("16x16/status/dialog-warning.png"),
    55     error_pri -> load_icon("16x16/status/dialog-error.png"))
    56 
    57   val tooltip_close_icon = load_icon("16x16/actions/document-close.png")
    58   val tooltip_detach_icon = load_icon("16x16/actions/window-new.png")
    59 
    60 
    61   /* token markup -- text styles */
    62 
    63   private val command_style: Map[String, Byte] =
    64   {
    65     import JEditToken._
    66     Map[String, Byte](
    67       Keyword.THY_END -> KEYWORD2,
    68       Keyword.THY_SCRIPT -> LABEL,
    69       Keyword.PRF_SCRIPT -> LABEL,
    70       Keyword.PRF_ASM -> KEYWORD3,
    71       Keyword.PRF_ASM_GOAL -> KEYWORD3
    72     ).withDefaultValue(KEYWORD1)
    73   }
    74 
    75   private val token_style: Map[Token.Kind.Value, Byte] =
    76   {
    77     import JEditToken._
    78     Map[Token.Kind.Value, Byte](
    79       Token.Kind.KEYWORD -> KEYWORD2,
    80       Token.Kind.IDENT -> NULL,
    81       Token.Kind.LONG_IDENT -> NULL,
    82       Token.Kind.SYM_IDENT -> NULL,
    83       Token.Kind.VAR -> NULL,
    84       Token.Kind.TYPE_IDENT -> NULL,
    85       Token.Kind.TYPE_VAR -> NULL,
    86       Token.Kind.NAT -> NULL,
    87       Token.Kind.FLOAT -> NULL,
    88       Token.Kind.STRING -> LITERAL1,
    89       Token.Kind.ALT_STRING -> LITERAL2,
    90       Token.Kind.VERBATIM -> COMMENT3,
    91       Token.Kind.SPACE -> NULL,
    92       Token.Kind.COMMENT -> COMMENT1,
    93       Token.Kind.ERROR -> INVALID
    94     ).withDefaultValue(NULL)
    95   }
    96 
    97   def token_markup(syntax: Outer_Syntax, token: Token): Byte =
    98     if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
    99     else if (token.is_operator) JEditToken.OPERATOR
   100     else token_style(token.kind)
   101 }
   102 
   103 
   104 class Rendering private(val snapshot: Document.Snapshot, val options: Options)
   105 {
   106   /* colors */
   107 
   108   def color_value(s: String): Color = Color_Value(options.string(s))
   109 
   110   val outdated_color = color_value("outdated_color")
   111   val unprocessed_color = color_value("unprocessed_color")
   112   val unprocessed1_color = color_value("unprocessed1_color")
   113   val running_color = color_value("running_color")
   114   val running1_color = color_value("running1_color")
   115   val light_color = color_value("light_color")
   116   val tooltip_color = color_value("tooltip_color")
   117   val writeln_color = color_value("writeln_color")
   118   val warning_color = color_value("warning_color")
   119   val error_color = color_value("error_color")
   120   val error1_color = color_value("error1_color")
   121   val writeln_message_color = color_value("writeln_message_color")
   122   val tracing_message_color = color_value("tracing_message_color")
   123   val warning_message_color = color_value("warning_message_color")
   124   val error_message_color = color_value("error_message_color")
   125   val bad_color = color_value("bad_color")
   126   val intensify_color = color_value("intensify_color")
   127   val quoted_color = color_value("quoted_color")
   128   val highlight_color = color_value("highlight_color")
   129   val hyperlink_color = color_value("hyperlink_color")
   130   val sendback_color = color_value("sendback_color")
   131   val sendback_active_color = color_value("sendback_active_color")
   132   val keyword1_color = color_value("keyword1_color")
   133   val keyword2_color = color_value("keyword2_color")
   134 
   135   val tfree_color = color_value("tfree_color")
   136   val tvar_color = color_value("tvar_color")
   137   val free_color = color_value("free_color")
   138   val skolem_color = color_value("skolem_color")
   139   val bound_color = color_value("bound_color")
   140   val var_color = color_value("var_color")
   141   val inner_numeral_color = color_value("inner_numeral_color")
   142   val inner_quoted_color = color_value("inner_quoted_color")
   143   val inner_comment_color = color_value("inner_comment_color")
   144   val antiquotation_color = color_value("antiquotation_color")
   145   val dynamic_color = color_value("dynamic_color")
   146 
   147 
   148   /* command overview */
   149 
   150   val overview_limit = options.int("jedit_text_overview_limit")
   151 
   152   def overview_color(range: Text.Range): Option[Color] =
   153   {
   154     if (snapshot.is_outdated) None
   155     else {
   156       val results =
   157         snapshot.cumulate_markup[(Protocol.Status, Int)](
   158           range, (Protocol.Status.init, 0),
   159           Some(Protocol.command_status_markup + Markup.WARNING + Markup.ERROR),
   160           {
   161             case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
   162               if (markup.name == Markup.WARNING || markup.name == Markup.ERROR)
   163                 (status, pri max Rendering.message_pri(markup.name))
   164               else (Protocol.command_status(status, markup), pri)
   165           })
   166       if (results.isEmpty) None
   167       else {
   168         val (status, pri) =
   169           ((Protocol.Status.init, 0) /: results) {
   170             case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) }
   171 
   172         if (pri == Rendering.warning_pri) Some(warning_color)
   173         else if (pri == Rendering.error_pri) Some(error_color)
   174         else if (status.is_unprocessed) Some(unprocessed_color)
   175         else if (status.is_running) Some(running_color)
   176         else if (status.is_failed) Some(error_color)
   177         else None
   178       }
   179     }
   180   }
   181 
   182 
   183   /* markup selectors */
   184 
   185   private val highlight_include =
   186     Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
   187       Markup.ENTITY, Markup.PATH, Markup.SORTING, Markup.TYPING, Markup.FREE, Markup.SKOLEM,
   188       Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOCUMENT_SOURCE)
   189 
   190   def highlight(range: Text.Range): Option[Text.Info[Color]] =
   191   {
   192     snapshot.select_markup(range, Some(highlight_include),
   193         {
   194           case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if highlight_include(name) =>
   195             Text.Info(snapshot.convert(info_range), highlight_color)
   196         }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   197   }
   198 
   199 
   200   private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH)
   201 
   202   def hyperlink(range: Text.Range): Option[Text.Info[Hyperlink]] =
   203   {
   204     snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include),
   205         {
   206           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
   207           if Path.is_ok(name) =>
   208             val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
   209             Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
   210 
   211           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
   212           if !props.exists(
   213             { case (Markup.KIND, Markup.ML_OPEN) => true
   214               case (Markup.KIND, Markup.ML_STRUCT) => true
   215               case _ => false }) =>
   216 
   217             props match {
   218               case Position.Def_Line_File(line, name) if Path.is_ok(name) =>
   219                 Isabelle_System.source_file(Path.explode(name)) match {
   220                   case Some(path) =>
   221                     val jedit_file = Isabelle_System.platform_path(path)
   222                     Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0)) :: links
   223                   case None => links
   224                 }
   225 
   226               case Position.Def_Id_Offset(id, offset) =>
   227                 snapshot.state.find_command(snapshot.version, id) match {
   228                   case Some((node, command)) =>
   229                     val sources =
   230                       node.commands.iterator.takeWhile(_ != command).map(_.source) ++
   231                         Iterator.single(command.source(Text.Range(0, command.decode(offset))))
   232                     val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
   233                     Text.Info(snapshot.convert(info_range),
   234                       Hyperlink(command.node_name.node, line, column)) :: links
   235                   case None => links
   236                 }
   237 
   238               case _ => links
   239             }
   240         }) match { case Text.Info(_, info :: _) #:: _ => Some(info) case _ => None }
   241   }
   242 
   243 
   244   def sendback(range: Text.Range): Option[Text.Info[Option[Document.Exec_ID]]] =
   245     snapshot.select_markup(range, Some(Set(Markup.SENDBACK)),
   246         {
   247           case Text.Info(info_range, XML.Elem(Markup(Markup.SENDBACK, props), _)) =>
   248             Text.Info(snapshot.convert(info_range), Position.Id.unapply(props))
   249         }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   250 
   251 
   252   def tooltip_message(range: Text.Range): XML.Body =
   253   {
   254     val msgs =
   255       snapshot.cumulate_markup[SortedMap[Long, XML.Tree]](range, SortedMap.empty,
   256         Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)),
   257         {
   258           case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
   259           if name == Markup.WRITELN ||
   260               name == Markup.WARNING ||
   261               name == Markup.ERROR =>
   262             msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
   263           case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
   264           if !body.isEmpty => msgs + (Document.new_id() -> msg)
   265         }).toList.flatMap(_.info)
   266     Pretty.separate(msgs.iterator.map(_._2).toList)
   267   }
   268 
   269 
   270   private val tooltips: Map[String, String] =
   271     Map(
   272       Markup.SORT -> "sort",
   273       Markup.TYP -> "type",
   274       Markup.TERM -> "term",
   275       Markup.PROP -> "proposition",
   276       Markup.TOKEN_RANGE -> "inner syntax token",
   277       Markup.FREE -> "free variable",
   278       Markup.SKOLEM -> "skolem variable",
   279       Markup.BOUND -> "bound variable",
   280       Markup.VAR -> "schematic variable",
   281       Markup.TFREE -> "free type variable",
   282       Markup.TVAR -> "schematic type variable",
   283       Markup.ML_SOURCE -> "ML source",
   284       Markup.DOCUMENT_SOURCE -> "document source")
   285 
   286   private val tooltip_elements =
   287     Set(Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.ML_TYPING, Markup.PATH) ++
   288       tooltips.keys
   289 
   290   private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
   291     Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
   292 
   293   def tooltip(range: Text.Range): XML.Body =
   294   {
   295     def add(prev: Text.Info[List[(Boolean, XML.Tree)]], r: Text.Range, p: (Boolean, XML.Tree)) =
   296       if (prev.range == r) Text.Info(r, p :: prev.info) else Text.Info(r, List(p))
   297 
   298     val tips =
   299       snapshot.cumulate_markup[Text.Info[(List[(Boolean, XML.Tree)])]](
   300         range, Text.Info(range, Nil), Some(tooltip_elements),
   301         {
   302           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
   303             val kind1 = space_explode('_', kind).mkString(" ")
   304             add(prev, r, (true, XML.Text(kind1 + " " + quote(name))))
   305           case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
   306           if Path.is_ok(name) =>
   307             val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
   308             add(prev, r, (true, XML.Text("file " + quote(jedit_file))))
   309           case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
   310           if name == Markup.SORTING || name == Markup.TYPING =>
   311             add(prev, r, (true, pretty_typing("::", body)))
   312           case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   313             add(prev, r, (false, pretty_typing("ML:", body)))
   314           case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
   315           if tooltips.isDefinedAt(name) => add(prev, r, (true, XML.Text(tooltips(name))))
   316         }).toList.flatMap(_.info.info)
   317 
   318     val all_tips =
   319       (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
   320     Library.separate(Pretty.FBreak, all_tips.toList)
   321   }
   322 
   323 
   324   def gutter_message(range: Text.Range): Option[Icon] =
   325   {
   326     val results =
   327       snapshot.cumulate_markup[Int](range, 0, Some(Set(Markup.WARNING, Markup.ERROR)),
   328         {
   329           case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
   330             body match {
   331               case List(XML.Elem(Markup(Markup.LEGACY, _), _)) =>
   332                 pri max Rendering.legacy_pri
   333               case _ => pri max Rendering.warning_pri
   334             }
   335           case (pri, Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _))) =>
   336             pri max Rendering.error_pri
   337         })
   338     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
   339     Rendering.gutter_icons.get(pri)
   340   }
   341 
   342 
   343   private val squiggly_colors = Map(
   344     Rendering.writeln_pri -> writeln_color,
   345     Rendering.warning_pri -> warning_color,
   346     Rendering.error_pri -> error_color)
   347 
   348   def squiggly_underline(range: Text.Range): Stream[Text.Info[Color]] =
   349   {
   350     val results =
   351       snapshot.cumulate_markup[Int](range, 0,
   352         Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)),
   353         {
   354           case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
   355           if name == Markup.WRITELN ||
   356             name == Markup.WARNING ||
   357             name == Markup.ERROR => pri max Rendering.message_pri(name)
   358         })
   359     for {
   360       Text.Info(r, pri) <- results
   361       color <- squiggly_colors.get(pri)
   362     } yield Text.Info(r, color)
   363   }
   364 
   365 
   366   private val messages_include =
   367     Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE)
   368 
   369   private val message_colors = Map(
   370     Rendering.writeln_pri -> writeln_message_color,
   371     Rendering.tracing_pri -> tracing_message_color,
   372     Rendering.warning_pri -> warning_message_color,
   373     Rendering.error_pri -> error_message_color)
   374 
   375   def line_background(range: Text.Range): Option[(Color, Boolean)] =
   376   {
   377     val results =
   378       snapshot.cumulate_markup[Int](range, 0, Some(messages_include),
   379         {
   380           case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
   381           if name == Markup.WRITELN_MESSAGE ||
   382             name == Markup.TRACING_MESSAGE ||
   383             name == Markup.WARNING_MESSAGE ||
   384             name == Markup.ERROR_MESSAGE => pri max Rendering.message_pri(name)
   385         })
   386     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
   387 
   388     val is_separator = pri > 0 &&
   389       snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)),
   390         {
   391           case (_, Text.Info(_, XML.Elem(Markup(Markup.SEPARATOR, _), _))) => true
   392         }).exists(_.info)
   393 
   394     message_colors.get(pri).map((_, is_separator))
   395   }
   396 
   397 
   398   private val background1_include =
   399     Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
   400       Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY +
   401       Markup.SENDBACK
   402 
   403   def background1(range: Text.Range): Stream[Text.Info[Color]] =
   404   {
   405     if (snapshot.is_outdated) Stream(Text.Info(range, outdated_color))
   406     else
   407       for {
   408         Text.Info(r, result) <-
   409           snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
   410             range, (Some(Protocol.Status.init), None), Some(background1_include),
   411             {
   412               case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
   413               if (Protocol.command_status_markup(markup.name)) =>
   414                 (Some(Protocol.command_status(status, markup)), color)
   415               case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
   416                 (None, Some(bad_color))
   417               case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   418                 (None, Some(intensify_color))
   419               case (_, Text.Info(_, XML.Elem(Markup(Markup.SENDBACK, _), _))) =>
   420                 (None, Some(sendback_color))
   421             })
   422         color <-
   423           (result match {
   424             case (Some(status), opt_color) =>
   425               if (status.is_unprocessed) Some(unprocessed1_color)
   426               else if (status.is_running) Some(running1_color)
   427               else opt_color
   428             case (_, opt_color) => opt_color
   429           })
   430       } yield Text.Info(r, color)
   431   }
   432 
   433 
   434   def background2(range: Text.Range): Stream[Text.Info[Color]] =
   435     snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)),
   436       {
   437         case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
   438       })
   439 
   440 
   441   def foreground(range: Text.Range): Stream[Text.Info[Color]] =
   442     snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)),
   443       {
   444         case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
   445         case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
   446         case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
   447       })
   448 
   449 
   450   private val text_colors: Map[String, Color] = Map(
   451       Markup.KEYWORD1 -> keyword1_color,
   452       Markup.KEYWORD2 -> keyword2_color,
   453       Markup.STRING -> Color.BLACK,
   454       Markup.ALTSTRING -> Color.BLACK,
   455       Markup.VERBATIM -> Color.BLACK,
   456       Markup.LITERAL -> keyword1_color,
   457       Markup.DELIMITER -> Color.BLACK,
   458       Markup.TFREE -> tfree_color,
   459       Markup.TVAR -> tvar_color,
   460       Markup.FREE -> free_color,
   461       Markup.SKOLEM -> skolem_color,
   462       Markup.BOUND -> bound_color,
   463       Markup.VAR -> var_color,
   464       Markup.INNER_STRING -> inner_quoted_color,
   465       Markup.INNER_COMMENT -> inner_comment_color,
   466       Markup.DYNAMIC_FACT -> dynamic_color,
   467       Markup.ML_KEYWORD -> keyword1_color,
   468       Markup.ML_DELIMITER -> Color.BLACK,
   469       Markup.ML_NUMERAL -> inner_numeral_color,
   470       Markup.ML_CHAR -> inner_quoted_color,
   471       Markup.ML_STRING -> inner_quoted_color,
   472       Markup.ML_COMMENT -> inner_comment_color,
   473       Markup.ANTIQ -> antiquotation_color)
   474 
   475   private val text_color_elements = Set.empty[String] ++ text_colors.keys
   476 
   477   def text_color(range: Text.Range, color: Color)
   478       : Stream[Text.Info[Color]] =
   479   {
   480     if (color == Token_Markup.hidden_color) Stream(Text.Info(range, color))
   481     else
   482       snapshot.cumulate_markup(range, color, Some(text_color_elements),
   483         {
   484           case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
   485           if text_colors.isDefinedAt(m) => text_colors(m)
   486         })
   487   }
   488 }