tuned file name;
authorwenzelm
Sun Nov 25 19:55:42 2012 +0100 (2012-11-25 ago)
changeset 50202ec0f2f8dbeb9
parent 50201 c26369c9eda6
child 50203 00d8ad713e32
tuned file name;
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/isabelle_rendering.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sun Nov 25 19:49:24 2012 +0100
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Nov 25 19:55:42 2012 +0100
     1.3 @@ -19,12 +19,11 @@
     1.4    "src/isabelle_encoding.scala"
     1.5    "src/isabelle_logic.scala"
     1.6    "src/isabelle_options.scala"
     1.7 -  "src/isabelle_rendering.scala"
     1.8    "src/isabelle_sidekick.scala"
     1.9    "src/jedit_lib.scala"
    1.10    "src/jedit_main.scala"
    1.11 +  "src/jedit_options.scala"
    1.12    "src/jedit_thy_load.scala"
    1.13 -  "src/jedit_options.scala"
    1.14    "src/output_dockable.scala"
    1.15    "src/plugin.scala"
    1.16    "src/pretty_text_area.scala"
    1.17 @@ -32,6 +31,7 @@
    1.18    "src/protocol_dockable.scala"
    1.19    "src/raw_output_dockable.scala"
    1.20    "src/readme_dockable.scala"
    1.21 +  "src/rendering.scala"
    1.22    "src/rich_text_area.scala"
    1.23    "src/scala_console.scala"
    1.24    "src/sendback.scala"
     2.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Sun Nov 25 19:49:24 2012 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,488 +0,0 @@
     2.4 -/*  Title:      Tools/jEdit/src/isabelle_rendering.scala
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -Isabelle-specific implementation of quasi-abstract rendering and
     2.8 -markup interpretation.
     2.9 -*/
    2.10 -
    2.11 -package isabelle.jedit
    2.12 -
    2.13 -
    2.14 -import isabelle._
    2.15 -
    2.16 -import java.awt.Color
    2.17 -import javax.swing.Icon
    2.18 -
    2.19 -import org.gjt.sp.jedit.syntax.{Token => JEditToken}
    2.20 -import org.gjt.sp.jedit.GUIUtilities
    2.21 -
    2.22 -import scala.collection.immutable.SortedMap
    2.23 -
    2.24 -
    2.25 -object Rendering
    2.26 -{
    2.27 -  def apply(snapshot: Document.Snapshot, options: Options): Rendering =
    2.28 -    new Rendering(snapshot, options)
    2.29 -
    2.30 -
    2.31 -  /* message priorities */
    2.32 -
    2.33 -  private val writeln_pri = 1
    2.34 -  private val tracing_pri = 2
    2.35 -  private val warning_pri = 3
    2.36 -  private val legacy_pri = 4
    2.37 -  private val error_pri = 5
    2.38 -
    2.39 -  private val message_pri = Map(
    2.40 -    Markup.WRITELN -> writeln_pri, Markup.WRITELN_MESSAGE -> writeln_pri,
    2.41 -    Markup.TRACING -> tracing_pri, Markup.TRACING_MESSAGE -> tracing_pri,
    2.42 -    Markup.WARNING -> warning_pri, Markup.WARNING_MESSAGE -> warning_pri,
    2.43 -    Markup.ERROR -> error_pri, Markup.ERROR_MESSAGE -> error_pri)
    2.44 -
    2.45 -
    2.46 -  /* icons */
    2.47 -
    2.48 -  private def load_icon(name: String): Icon =
    2.49 -  {
    2.50 -    val icon = GUIUtilities.loadIcon(name)
    2.51 -    if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
    2.52 -    else icon
    2.53 -  }
    2.54 -
    2.55 -  private val gutter_icons = Map(
    2.56 -    warning_pri -> load_icon("16x16/status/dialog-information.png"),
    2.57 -    legacy_pri -> load_icon("16x16/status/dialog-warning.png"),
    2.58 -    error_pri -> load_icon("16x16/status/dialog-error.png"))
    2.59 -
    2.60 -  val tooltip_close_icon = load_icon("16x16/actions/document-close.png")
    2.61 -  val tooltip_detach_icon = load_icon("16x16/actions/window-new.png")
    2.62 -
    2.63 -
    2.64 -  /* token markup -- text styles */
    2.65 -
    2.66 -  private val command_style: Map[String, Byte] =
    2.67 -  {
    2.68 -    import JEditToken._
    2.69 -    Map[String, Byte](
    2.70 -      Keyword.THY_END -> KEYWORD2,
    2.71 -      Keyword.THY_SCRIPT -> LABEL,
    2.72 -      Keyword.PRF_SCRIPT -> LABEL,
    2.73 -      Keyword.PRF_ASM -> KEYWORD3,
    2.74 -      Keyword.PRF_ASM_GOAL -> KEYWORD3
    2.75 -    ).withDefaultValue(KEYWORD1)
    2.76 -  }
    2.77 -
    2.78 -  private val token_style: Map[Token.Kind.Value, Byte] =
    2.79 -  {
    2.80 -    import JEditToken._
    2.81 -    Map[Token.Kind.Value, Byte](
    2.82 -      Token.Kind.KEYWORD -> KEYWORD2,
    2.83 -      Token.Kind.IDENT -> NULL,
    2.84 -      Token.Kind.LONG_IDENT -> NULL,
    2.85 -      Token.Kind.SYM_IDENT -> NULL,
    2.86 -      Token.Kind.VAR -> NULL,
    2.87 -      Token.Kind.TYPE_IDENT -> NULL,
    2.88 -      Token.Kind.TYPE_VAR -> NULL,
    2.89 -      Token.Kind.NAT -> NULL,
    2.90 -      Token.Kind.FLOAT -> NULL,
    2.91 -      Token.Kind.STRING -> LITERAL1,
    2.92 -      Token.Kind.ALT_STRING -> LITERAL2,
    2.93 -      Token.Kind.VERBATIM -> COMMENT3,
    2.94 -      Token.Kind.SPACE -> NULL,
    2.95 -      Token.Kind.COMMENT -> COMMENT1,
    2.96 -      Token.Kind.ERROR -> INVALID
    2.97 -    ).withDefaultValue(NULL)
    2.98 -  }
    2.99 -
   2.100 -  def token_markup(syntax: Outer_Syntax, token: Token): Byte =
   2.101 -    if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
   2.102 -    else if (token.is_operator) JEditToken.OPERATOR
   2.103 -    else token_style(token.kind)
   2.104 -}
   2.105 -
   2.106 -
   2.107 -class Rendering private(val snapshot: Document.Snapshot, val options: Options)
   2.108 -{
   2.109 -  /* colors */
   2.110 -
   2.111 -  def color_value(s: String): Color = Color_Value(options.string(s))
   2.112 -
   2.113 -  val outdated_color = color_value("outdated_color")
   2.114 -  val unprocessed_color = color_value("unprocessed_color")
   2.115 -  val unprocessed1_color = color_value("unprocessed1_color")
   2.116 -  val running_color = color_value("running_color")
   2.117 -  val running1_color = color_value("running1_color")
   2.118 -  val light_color = color_value("light_color")
   2.119 -  val tooltip_color = color_value("tooltip_color")
   2.120 -  val writeln_color = color_value("writeln_color")
   2.121 -  val warning_color = color_value("warning_color")
   2.122 -  val error_color = color_value("error_color")
   2.123 -  val error1_color = color_value("error1_color")
   2.124 -  val writeln_message_color = color_value("writeln_message_color")
   2.125 -  val tracing_message_color = color_value("tracing_message_color")
   2.126 -  val warning_message_color = color_value("warning_message_color")
   2.127 -  val error_message_color = color_value("error_message_color")
   2.128 -  val bad_color = color_value("bad_color")
   2.129 -  val intensify_color = color_value("intensify_color")
   2.130 -  val quoted_color = color_value("quoted_color")
   2.131 -  val highlight_color = color_value("highlight_color")
   2.132 -  val hyperlink_color = color_value("hyperlink_color")
   2.133 -  val sendback_color = color_value("sendback_color")
   2.134 -  val sendback_active_color = color_value("sendback_active_color")
   2.135 -  val keyword1_color = color_value("keyword1_color")
   2.136 -  val keyword2_color = color_value("keyword2_color")
   2.137 -
   2.138 -  val tfree_color = color_value("tfree_color")
   2.139 -  val tvar_color = color_value("tvar_color")
   2.140 -  val free_color = color_value("free_color")
   2.141 -  val skolem_color = color_value("skolem_color")
   2.142 -  val bound_color = color_value("bound_color")
   2.143 -  val var_color = color_value("var_color")
   2.144 -  val inner_numeral_color = color_value("inner_numeral_color")
   2.145 -  val inner_quoted_color = color_value("inner_quoted_color")
   2.146 -  val inner_comment_color = color_value("inner_comment_color")
   2.147 -  val antiquotation_color = color_value("antiquotation_color")
   2.148 -  val dynamic_color = color_value("dynamic_color")
   2.149 -
   2.150 -
   2.151 -  /* command overview */
   2.152 -
   2.153 -  val overview_limit = options.int("jedit_text_overview_limit")
   2.154 -
   2.155 -  def overview_color(range: Text.Range): Option[Color] =
   2.156 -  {
   2.157 -    if (snapshot.is_outdated) None
   2.158 -    else {
   2.159 -      val results =
   2.160 -        snapshot.cumulate_markup[(Protocol.Status, Int)](
   2.161 -          range, (Protocol.Status.init, 0),
   2.162 -          Some(Protocol.command_status_markup + Markup.WARNING + Markup.ERROR),
   2.163 -          {
   2.164 -            case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
   2.165 -              if (markup.name == Markup.WARNING || markup.name == Markup.ERROR)
   2.166 -                (status, pri max Rendering.message_pri(markup.name))
   2.167 -              else (Protocol.command_status(status, markup), pri)
   2.168 -          })
   2.169 -      if (results.isEmpty) None
   2.170 -      else {
   2.171 -        val (status, pri) =
   2.172 -          ((Protocol.Status.init, 0) /: results) {
   2.173 -            case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) }
   2.174 -
   2.175 -        if (pri == Rendering.warning_pri) Some(warning_color)
   2.176 -        else if (pri == Rendering.error_pri) Some(error_color)
   2.177 -        else if (status.is_unprocessed) Some(unprocessed_color)
   2.178 -        else if (status.is_running) Some(running_color)
   2.179 -        else if (status.is_failed) Some(error_color)
   2.180 -        else None
   2.181 -      }
   2.182 -    }
   2.183 -  }
   2.184 -
   2.185 -
   2.186 -  /* markup selectors */
   2.187 -
   2.188 -  private val highlight_include =
   2.189 -    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
   2.190 -      Markup.ENTITY, Markup.PATH, Markup.SORTING, Markup.TYPING, Markup.FREE, Markup.SKOLEM,
   2.191 -      Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOCUMENT_SOURCE)
   2.192 -
   2.193 -  def highlight(range: Text.Range): Option[Text.Info[Color]] =
   2.194 -  {
   2.195 -    snapshot.select_markup(range, Some(highlight_include),
   2.196 -        {
   2.197 -          case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if highlight_include(name) =>
   2.198 -            Text.Info(snapshot.convert(info_range), highlight_color)
   2.199 -        }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   2.200 -  }
   2.201 -
   2.202 -
   2.203 -  private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH)
   2.204 -
   2.205 -  def hyperlink(range: Text.Range): Option[Text.Info[Hyperlink]] =
   2.206 -  {
   2.207 -    snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include),
   2.208 -        {
   2.209 -          case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
   2.210 -          if Path.is_ok(name) =>
   2.211 -            val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
   2.212 -            Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
   2.213 -
   2.214 -          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
   2.215 -          if !props.exists(
   2.216 -            { case (Markup.KIND, Markup.ML_OPEN) => true
   2.217 -              case (Markup.KIND, Markup.ML_STRUCT) => true
   2.218 -              case _ => false }) =>
   2.219 -
   2.220 -            props match {
   2.221 -              case Position.Def_Line_File(line, name) if Path.is_ok(name) =>
   2.222 -                Isabelle_System.source_file(Path.explode(name)) match {
   2.223 -                  case Some(path) =>
   2.224 -                    val jedit_file = Isabelle_System.platform_path(path)
   2.225 -                    Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0)) :: links
   2.226 -                  case None => links
   2.227 -                }
   2.228 -
   2.229 -              case Position.Def_Id_Offset(id, offset) =>
   2.230 -                snapshot.state.find_command(snapshot.version, id) match {
   2.231 -                  case Some((node, command)) =>
   2.232 -                    val sources =
   2.233 -                      node.commands.iterator.takeWhile(_ != command).map(_.source) ++
   2.234 -                        Iterator.single(command.source(Text.Range(0, command.decode(offset))))
   2.235 -                    val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
   2.236 -                    Text.Info(snapshot.convert(info_range),
   2.237 -                      Hyperlink(command.node_name.node, line, column)) :: links
   2.238 -                  case None => links
   2.239 -                }
   2.240 -
   2.241 -              case _ => links
   2.242 -            }
   2.243 -        }) match { case Text.Info(_, info :: _) #:: _ => Some(info) case _ => None }
   2.244 -  }
   2.245 -
   2.246 -
   2.247 -  def sendback(range: Text.Range): Option[Text.Info[Option[Document.Exec_ID]]] =
   2.248 -    snapshot.select_markup(range, Some(Set(Markup.SENDBACK)),
   2.249 -        {
   2.250 -          case Text.Info(info_range, XML.Elem(Markup(Markup.SENDBACK, props), _)) =>
   2.251 -            Text.Info(snapshot.convert(info_range), Position.Id.unapply(props))
   2.252 -        }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   2.253 -
   2.254 -
   2.255 -  def tooltip_message(range: Text.Range): XML.Body =
   2.256 -  {
   2.257 -    val msgs =
   2.258 -      snapshot.cumulate_markup[SortedMap[Long, XML.Tree]](range, SortedMap.empty,
   2.259 -        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)),
   2.260 -        {
   2.261 -          case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
   2.262 -          if name == Markup.WRITELN ||
   2.263 -              name == Markup.WARNING ||
   2.264 -              name == Markup.ERROR =>
   2.265 -            msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
   2.266 -          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
   2.267 -          if !body.isEmpty => msgs + (Document.new_id() -> msg)
   2.268 -        }).toList.flatMap(_.info)
   2.269 -    Pretty.separate(msgs.iterator.map(_._2).toList)
   2.270 -  }
   2.271 -
   2.272 -
   2.273 -  private val tooltips: Map[String, String] =
   2.274 -    Map(
   2.275 -      Markup.SORT -> "sort",
   2.276 -      Markup.TYP -> "type",
   2.277 -      Markup.TERM -> "term",
   2.278 -      Markup.PROP -> "proposition",
   2.279 -      Markup.TOKEN_RANGE -> "inner syntax token",
   2.280 -      Markup.FREE -> "free variable",
   2.281 -      Markup.SKOLEM -> "skolem variable",
   2.282 -      Markup.BOUND -> "bound variable",
   2.283 -      Markup.VAR -> "schematic variable",
   2.284 -      Markup.TFREE -> "free type variable",
   2.285 -      Markup.TVAR -> "schematic type variable",
   2.286 -      Markup.ML_SOURCE -> "ML source",
   2.287 -      Markup.DOCUMENT_SOURCE -> "document source")
   2.288 -
   2.289 -  private val tooltip_elements =
   2.290 -    Set(Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.ML_TYPING, Markup.PATH) ++
   2.291 -      tooltips.keys
   2.292 -
   2.293 -  private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
   2.294 -    Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
   2.295 -
   2.296 -  def tooltip(range: Text.Range): XML.Body =
   2.297 -  {
   2.298 -    def add(prev: Text.Info[List[(Boolean, XML.Tree)]], r: Text.Range, p: (Boolean, XML.Tree)) =
   2.299 -      if (prev.range == r) Text.Info(r, p :: prev.info) else Text.Info(r, List(p))
   2.300 -
   2.301 -    val tips =
   2.302 -      snapshot.cumulate_markup[Text.Info[(List[(Boolean, XML.Tree)])]](
   2.303 -        range, Text.Info(range, Nil), Some(tooltip_elements),
   2.304 -        {
   2.305 -          case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
   2.306 -            val kind1 = space_explode('_', kind).mkString(" ")
   2.307 -            add(prev, r, (true, XML.Text(kind1 + " " + quote(name))))
   2.308 -          case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
   2.309 -          if Path.is_ok(name) =>
   2.310 -            val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
   2.311 -            add(prev, r, (true, XML.Text("file " + quote(jedit_file))))
   2.312 -          case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
   2.313 -          if name == Markup.SORTING || name == Markup.TYPING =>
   2.314 -            add(prev, r, (true, pretty_typing("::", body)))
   2.315 -          case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   2.316 -            add(prev, r, (false, pretty_typing("ML:", body)))
   2.317 -          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
   2.318 -          if tooltips.isDefinedAt(name) => add(prev, r, (true, XML.Text(tooltips(name))))
   2.319 -        }).toList.flatMap(_.info.info)
   2.320 -
   2.321 -    val all_tips =
   2.322 -      (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
   2.323 -    Library.separate(Pretty.FBreak, all_tips.toList)
   2.324 -  }
   2.325 -
   2.326 -
   2.327 -  def gutter_message(range: Text.Range): Option[Icon] =
   2.328 -  {
   2.329 -    val results =
   2.330 -      snapshot.cumulate_markup[Int](range, 0, Some(Set(Markup.WARNING, Markup.ERROR)),
   2.331 -        {
   2.332 -          case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
   2.333 -            body match {
   2.334 -              case List(XML.Elem(Markup(Markup.LEGACY, _), _)) =>
   2.335 -                pri max Rendering.legacy_pri
   2.336 -              case _ => pri max Rendering.warning_pri
   2.337 -            }
   2.338 -          case (pri, Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _))) =>
   2.339 -            pri max Rendering.error_pri
   2.340 -        })
   2.341 -    val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
   2.342 -    Rendering.gutter_icons.get(pri)
   2.343 -  }
   2.344 -
   2.345 -
   2.346 -  private val squiggly_colors = Map(
   2.347 -    Rendering.writeln_pri -> writeln_color,
   2.348 -    Rendering.warning_pri -> warning_color,
   2.349 -    Rendering.error_pri -> error_color)
   2.350 -
   2.351 -  def squiggly_underline(range: Text.Range): Stream[Text.Info[Color]] =
   2.352 -  {
   2.353 -    val results =
   2.354 -      snapshot.cumulate_markup[Int](range, 0,
   2.355 -        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)),
   2.356 -        {
   2.357 -          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
   2.358 -          if name == Markup.WRITELN ||
   2.359 -            name == Markup.WARNING ||
   2.360 -            name == Markup.ERROR => pri max Rendering.message_pri(name)
   2.361 -        })
   2.362 -    for {
   2.363 -      Text.Info(r, pri) <- results
   2.364 -      color <- squiggly_colors.get(pri)
   2.365 -    } yield Text.Info(r, color)
   2.366 -  }
   2.367 -
   2.368 -
   2.369 -  private val messages_include =
   2.370 -    Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE)
   2.371 -
   2.372 -  private val message_colors = Map(
   2.373 -    Rendering.writeln_pri -> writeln_message_color,
   2.374 -    Rendering.tracing_pri -> tracing_message_color,
   2.375 -    Rendering.warning_pri -> warning_message_color,
   2.376 -    Rendering.error_pri -> error_message_color)
   2.377 -
   2.378 -  def line_background(range: Text.Range): Option[(Color, Boolean)] =
   2.379 -  {
   2.380 -    val results =
   2.381 -      snapshot.cumulate_markup[Int](range, 0, Some(messages_include),
   2.382 -        {
   2.383 -          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
   2.384 -          if name == Markup.WRITELN_MESSAGE ||
   2.385 -            name == Markup.TRACING_MESSAGE ||
   2.386 -            name == Markup.WARNING_MESSAGE ||
   2.387 -            name == Markup.ERROR_MESSAGE => pri max Rendering.message_pri(name)
   2.388 -        })
   2.389 -    val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
   2.390 -
   2.391 -    val is_separator = pri > 0 &&
   2.392 -      snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)),
   2.393 -        {
   2.394 -          case (_, Text.Info(_, XML.Elem(Markup(Markup.SEPARATOR, _), _))) => true
   2.395 -        }).exists(_.info)
   2.396 -
   2.397 -    message_colors.get(pri).map((_, is_separator))
   2.398 -  }
   2.399 -
   2.400 -
   2.401 -  private val background1_include =
   2.402 -    Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
   2.403 -      Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY +
   2.404 -      Markup.SENDBACK
   2.405 -
   2.406 -  def background1(range: Text.Range): Stream[Text.Info[Color]] =
   2.407 -  {
   2.408 -    if (snapshot.is_outdated) Stream(Text.Info(range, outdated_color))
   2.409 -    else
   2.410 -      for {
   2.411 -        Text.Info(r, result) <-
   2.412 -          snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
   2.413 -            range, (Some(Protocol.Status.init), None), Some(background1_include),
   2.414 -            {
   2.415 -              case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
   2.416 -              if (Protocol.command_status_markup(markup.name)) =>
   2.417 -                (Some(Protocol.command_status(status, markup)), color)
   2.418 -              case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
   2.419 -                (None, Some(bad_color))
   2.420 -              case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   2.421 -                (None, Some(intensify_color))
   2.422 -              case (_, Text.Info(_, XML.Elem(Markup(Markup.SENDBACK, _), _))) =>
   2.423 -                (None, Some(sendback_color))
   2.424 -            })
   2.425 -        color <-
   2.426 -          (result match {
   2.427 -            case (Some(status), opt_color) =>
   2.428 -              if (status.is_unprocessed) Some(unprocessed1_color)
   2.429 -              else if (status.is_running) Some(running1_color)
   2.430 -              else opt_color
   2.431 -            case (_, opt_color) => opt_color
   2.432 -          })
   2.433 -      } yield Text.Info(r, color)
   2.434 -  }
   2.435 -
   2.436 -
   2.437 -  def background2(range: Text.Range): Stream[Text.Info[Color]] =
   2.438 -    snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)),
   2.439 -      {
   2.440 -        case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
   2.441 -      })
   2.442 -
   2.443 -
   2.444 -  def foreground(range: Text.Range): Stream[Text.Info[Color]] =
   2.445 -    snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)),
   2.446 -      {
   2.447 -        case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
   2.448 -        case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
   2.449 -        case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
   2.450 -      })
   2.451 -
   2.452 -
   2.453 -  private val text_colors: Map[String, Color] = Map(
   2.454 -      Markup.KEYWORD1 -> keyword1_color,
   2.455 -      Markup.KEYWORD2 -> keyword2_color,
   2.456 -      Markup.STRING -> Color.BLACK,
   2.457 -      Markup.ALTSTRING -> Color.BLACK,
   2.458 -      Markup.VERBATIM -> Color.BLACK,
   2.459 -      Markup.LITERAL -> keyword1_color,
   2.460 -      Markup.DELIMITER -> Color.BLACK,
   2.461 -      Markup.TFREE -> tfree_color,
   2.462 -      Markup.TVAR -> tvar_color,
   2.463 -      Markup.FREE -> free_color,
   2.464 -      Markup.SKOLEM -> skolem_color,
   2.465 -      Markup.BOUND -> bound_color,
   2.466 -      Markup.VAR -> var_color,
   2.467 -      Markup.INNER_STRING -> inner_quoted_color,
   2.468 -      Markup.INNER_COMMENT -> inner_comment_color,
   2.469 -      Markup.DYNAMIC_FACT -> dynamic_color,
   2.470 -      Markup.ML_KEYWORD -> keyword1_color,
   2.471 -      Markup.ML_DELIMITER -> Color.BLACK,
   2.472 -      Markup.ML_NUMERAL -> inner_numeral_color,
   2.473 -      Markup.ML_CHAR -> inner_quoted_color,
   2.474 -      Markup.ML_STRING -> inner_quoted_color,
   2.475 -      Markup.ML_COMMENT -> inner_comment_color,
   2.476 -      Markup.ANTIQ -> antiquotation_color)
   2.477 -
   2.478 -  private val text_color_elements = Set.empty[String] ++ text_colors.keys
   2.479 -
   2.480 -  def text_color(range: Text.Range, color: Color)
   2.481 -      : Stream[Text.Info[Color]] =
   2.482 -  {
   2.483 -    if (color == Token_Markup.hidden_color) Stream(Text.Info(range, color))
   2.484 -    else
   2.485 -      snapshot.cumulate_markup(range, color, Some(text_color_elements),
   2.486 -        {
   2.487 -          case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
   2.488 -          if text_colors.isDefinedAt(m) => text_colors(m)
   2.489 -        })
   2.490 -  }
   2.491 -}
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sun Nov 25 19:55:42 2012 +0100
     3.3 @@ -0,0 +1,488 @@
     3.4 +/*  Title:      Tools/jEdit/src/rendering.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Isabelle-specific implementation of quasi-abstract rendering and
     3.8 +markup interpretation.
     3.9 +*/
    3.10 +
    3.11 +package isabelle.jedit
    3.12 +
    3.13 +
    3.14 +import isabelle._
    3.15 +
    3.16 +import java.awt.Color
    3.17 +import javax.swing.Icon
    3.18 +
    3.19 +import org.gjt.sp.jedit.syntax.{Token => JEditToken}
    3.20 +import org.gjt.sp.jedit.GUIUtilities
    3.21 +
    3.22 +import scala.collection.immutable.SortedMap
    3.23 +
    3.24 +
    3.25 +object Rendering
    3.26 +{
    3.27 +  def apply(snapshot: Document.Snapshot, options: Options): Rendering =
    3.28 +    new Rendering(snapshot, options)
    3.29 +
    3.30 +
    3.31 +  /* message priorities */
    3.32 +
    3.33 +  private val writeln_pri = 1
    3.34 +  private val tracing_pri = 2
    3.35 +  private val warning_pri = 3
    3.36 +  private val legacy_pri = 4
    3.37 +  private val error_pri = 5
    3.38 +
    3.39 +  private val message_pri = Map(
    3.40 +    Markup.WRITELN -> writeln_pri, Markup.WRITELN_MESSAGE -> writeln_pri,
    3.41 +    Markup.TRACING -> tracing_pri, Markup.TRACING_MESSAGE -> tracing_pri,
    3.42 +    Markup.WARNING -> warning_pri, Markup.WARNING_MESSAGE -> warning_pri,
    3.43 +    Markup.ERROR -> error_pri, Markup.ERROR_MESSAGE -> error_pri)
    3.44 +
    3.45 +
    3.46 +  /* icons */
    3.47 +
    3.48 +  private def load_icon(name: String): Icon =
    3.49 +  {
    3.50 +    val icon = GUIUtilities.loadIcon(name)
    3.51 +    if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
    3.52 +    else icon
    3.53 +  }
    3.54 +
    3.55 +  private val gutter_icons = Map(
    3.56 +    warning_pri -> load_icon("16x16/status/dialog-information.png"),
    3.57 +    legacy_pri -> load_icon("16x16/status/dialog-warning.png"),
    3.58 +    error_pri -> load_icon("16x16/status/dialog-error.png"))
    3.59 +
    3.60 +  val tooltip_close_icon = load_icon("16x16/actions/document-close.png")
    3.61 +  val tooltip_detach_icon = load_icon("16x16/actions/window-new.png")
    3.62 +
    3.63 +
    3.64 +  /* token markup -- text styles */
    3.65 +
    3.66 +  private val command_style: Map[String, Byte] =
    3.67 +  {
    3.68 +    import JEditToken._
    3.69 +    Map[String, Byte](
    3.70 +      Keyword.THY_END -> KEYWORD2,
    3.71 +      Keyword.THY_SCRIPT -> LABEL,
    3.72 +      Keyword.PRF_SCRIPT -> LABEL,
    3.73 +      Keyword.PRF_ASM -> KEYWORD3,
    3.74 +      Keyword.PRF_ASM_GOAL -> KEYWORD3
    3.75 +    ).withDefaultValue(KEYWORD1)
    3.76 +  }
    3.77 +
    3.78 +  private val token_style: Map[Token.Kind.Value, Byte] =
    3.79 +  {
    3.80 +    import JEditToken._
    3.81 +    Map[Token.Kind.Value, Byte](
    3.82 +      Token.Kind.KEYWORD -> KEYWORD2,
    3.83 +      Token.Kind.IDENT -> NULL,
    3.84 +      Token.Kind.LONG_IDENT -> NULL,
    3.85 +      Token.Kind.SYM_IDENT -> NULL,
    3.86 +      Token.Kind.VAR -> NULL,
    3.87 +      Token.Kind.TYPE_IDENT -> NULL,
    3.88 +      Token.Kind.TYPE_VAR -> NULL,
    3.89 +      Token.Kind.NAT -> NULL,
    3.90 +      Token.Kind.FLOAT -> NULL,
    3.91 +      Token.Kind.STRING -> LITERAL1,
    3.92 +      Token.Kind.ALT_STRING -> LITERAL2,
    3.93 +      Token.Kind.VERBATIM -> COMMENT3,
    3.94 +      Token.Kind.SPACE -> NULL,
    3.95 +      Token.Kind.COMMENT -> COMMENT1,
    3.96 +      Token.Kind.ERROR -> INVALID
    3.97 +    ).withDefaultValue(NULL)
    3.98 +  }
    3.99 +
   3.100 +  def token_markup(syntax: Outer_Syntax, token: Token): Byte =
   3.101 +    if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
   3.102 +    else if (token.is_operator) JEditToken.OPERATOR
   3.103 +    else token_style(token.kind)
   3.104 +}
   3.105 +
   3.106 +
   3.107 +class Rendering private(val snapshot: Document.Snapshot, val options: Options)
   3.108 +{
   3.109 +  /* colors */
   3.110 +
   3.111 +  def color_value(s: String): Color = Color_Value(options.string(s))
   3.112 +
   3.113 +  val outdated_color = color_value("outdated_color")
   3.114 +  val unprocessed_color = color_value("unprocessed_color")
   3.115 +  val unprocessed1_color = color_value("unprocessed1_color")
   3.116 +  val running_color = color_value("running_color")
   3.117 +  val running1_color = color_value("running1_color")
   3.118 +  val light_color = color_value("light_color")
   3.119 +  val tooltip_color = color_value("tooltip_color")
   3.120 +  val writeln_color = color_value("writeln_color")
   3.121 +  val warning_color = color_value("warning_color")
   3.122 +  val error_color = color_value("error_color")
   3.123 +  val error1_color = color_value("error1_color")
   3.124 +  val writeln_message_color = color_value("writeln_message_color")
   3.125 +  val tracing_message_color = color_value("tracing_message_color")
   3.126 +  val warning_message_color = color_value("warning_message_color")
   3.127 +  val error_message_color = color_value("error_message_color")
   3.128 +  val bad_color = color_value("bad_color")
   3.129 +  val intensify_color = color_value("intensify_color")
   3.130 +  val quoted_color = color_value("quoted_color")
   3.131 +  val highlight_color = color_value("highlight_color")
   3.132 +  val hyperlink_color = color_value("hyperlink_color")
   3.133 +  val sendback_color = color_value("sendback_color")
   3.134 +  val sendback_active_color = color_value("sendback_active_color")
   3.135 +  val keyword1_color = color_value("keyword1_color")
   3.136 +  val keyword2_color = color_value("keyword2_color")
   3.137 +
   3.138 +  val tfree_color = color_value("tfree_color")
   3.139 +  val tvar_color = color_value("tvar_color")
   3.140 +  val free_color = color_value("free_color")
   3.141 +  val skolem_color = color_value("skolem_color")
   3.142 +  val bound_color = color_value("bound_color")
   3.143 +  val var_color = color_value("var_color")
   3.144 +  val inner_numeral_color = color_value("inner_numeral_color")
   3.145 +  val inner_quoted_color = color_value("inner_quoted_color")
   3.146 +  val inner_comment_color = color_value("inner_comment_color")
   3.147 +  val antiquotation_color = color_value("antiquotation_color")
   3.148 +  val dynamic_color = color_value("dynamic_color")
   3.149 +
   3.150 +
   3.151 +  /* command overview */
   3.152 +
   3.153 +  val overview_limit = options.int("jedit_text_overview_limit")
   3.154 +
   3.155 +  def overview_color(range: Text.Range): Option[Color] =
   3.156 +  {
   3.157 +    if (snapshot.is_outdated) None
   3.158 +    else {
   3.159 +      val results =
   3.160 +        snapshot.cumulate_markup[(Protocol.Status, Int)](
   3.161 +          range, (Protocol.Status.init, 0),
   3.162 +          Some(Protocol.command_status_markup + Markup.WARNING + Markup.ERROR),
   3.163 +          {
   3.164 +            case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
   3.165 +              if (markup.name == Markup.WARNING || markup.name == Markup.ERROR)
   3.166 +                (status, pri max Rendering.message_pri(markup.name))
   3.167 +              else (Protocol.command_status(status, markup), pri)
   3.168 +          })
   3.169 +      if (results.isEmpty) None
   3.170 +      else {
   3.171 +        val (status, pri) =
   3.172 +          ((Protocol.Status.init, 0) /: results) {
   3.173 +            case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) }
   3.174 +
   3.175 +        if (pri == Rendering.warning_pri) Some(warning_color)
   3.176 +        else if (pri == Rendering.error_pri) Some(error_color)
   3.177 +        else if (status.is_unprocessed) Some(unprocessed_color)
   3.178 +        else if (status.is_running) Some(running_color)
   3.179 +        else if (status.is_failed) Some(error_color)
   3.180 +        else None
   3.181 +      }
   3.182 +    }
   3.183 +  }
   3.184 +
   3.185 +
   3.186 +  /* markup selectors */
   3.187 +
   3.188 +  private val highlight_include =
   3.189 +    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
   3.190 +      Markup.ENTITY, Markup.PATH, Markup.SORTING, Markup.TYPING, Markup.FREE, Markup.SKOLEM,
   3.191 +      Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOCUMENT_SOURCE)
   3.192 +
   3.193 +  def highlight(range: Text.Range): Option[Text.Info[Color]] =
   3.194 +  {
   3.195 +    snapshot.select_markup(range, Some(highlight_include),
   3.196 +        {
   3.197 +          case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if highlight_include(name) =>
   3.198 +            Text.Info(snapshot.convert(info_range), highlight_color)
   3.199 +        }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   3.200 +  }
   3.201 +
   3.202 +
   3.203 +  private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH)
   3.204 +
   3.205 +  def hyperlink(range: Text.Range): Option[Text.Info[Hyperlink]] =
   3.206 +  {
   3.207 +    snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include),
   3.208 +        {
   3.209 +          case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
   3.210 +          if Path.is_ok(name) =>
   3.211 +            val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
   3.212 +            Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
   3.213 +
   3.214 +          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
   3.215 +          if !props.exists(
   3.216 +            { case (Markup.KIND, Markup.ML_OPEN) => true
   3.217 +              case (Markup.KIND, Markup.ML_STRUCT) => true
   3.218 +              case _ => false }) =>
   3.219 +
   3.220 +            props match {
   3.221 +              case Position.Def_Line_File(line, name) if Path.is_ok(name) =>
   3.222 +                Isabelle_System.source_file(Path.explode(name)) match {
   3.223 +                  case Some(path) =>
   3.224 +                    val jedit_file = Isabelle_System.platform_path(path)
   3.225 +                    Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0)) :: links
   3.226 +                  case None => links
   3.227 +                }
   3.228 +
   3.229 +              case Position.Def_Id_Offset(id, offset) =>
   3.230 +                snapshot.state.find_command(snapshot.version, id) match {
   3.231 +                  case Some((node, command)) =>
   3.232 +                    val sources =
   3.233 +                      node.commands.iterator.takeWhile(_ != command).map(_.source) ++
   3.234 +                        Iterator.single(command.source(Text.Range(0, command.decode(offset))))
   3.235 +                    val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
   3.236 +                    Text.Info(snapshot.convert(info_range),
   3.237 +                      Hyperlink(command.node_name.node, line, column)) :: links
   3.238 +                  case None => links
   3.239 +                }
   3.240 +
   3.241 +              case _ => links
   3.242 +            }
   3.243 +        }) match { case Text.Info(_, info :: _) #:: _ => Some(info) case _ => None }
   3.244 +  }
   3.245 +
   3.246 +
   3.247 +  def sendback(range: Text.Range): Option[Text.Info[Option[Document.Exec_ID]]] =
   3.248 +    snapshot.select_markup(range, Some(Set(Markup.SENDBACK)),
   3.249 +        {
   3.250 +          case Text.Info(info_range, XML.Elem(Markup(Markup.SENDBACK, props), _)) =>
   3.251 +            Text.Info(snapshot.convert(info_range), Position.Id.unapply(props))
   3.252 +        }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   3.253 +
   3.254 +
   3.255 +  def tooltip_message(range: Text.Range): XML.Body =
   3.256 +  {
   3.257 +    val msgs =
   3.258 +      snapshot.cumulate_markup[SortedMap[Long, XML.Tree]](range, SortedMap.empty,
   3.259 +        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)),
   3.260 +        {
   3.261 +          case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
   3.262 +          if name == Markup.WRITELN ||
   3.263 +              name == Markup.WARNING ||
   3.264 +              name == Markup.ERROR =>
   3.265 +            msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
   3.266 +          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
   3.267 +          if !body.isEmpty => msgs + (Document.new_id() -> msg)
   3.268 +        }).toList.flatMap(_.info)
   3.269 +    Pretty.separate(msgs.iterator.map(_._2).toList)
   3.270 +  }
   3.271 +
   3.272 +
   3.273 +  private val tooltips: Map[String, String] =
   3.274 +    Map(
   3.275 +      Markup.SORT -> "sort",
   3.276 +      Markup.TYP -> "type",
   3.277 +      Markup.TERM -> "term",
   3.278 +      Markup.PROP -> "proposition",
   3.279 +      Markup.TOKEN_RANGE -> "inner syntax token",
   3.280 +      Markup.FREE -> "free variable",
   3.281 +      Markup.SKOLEM -> "skolem variable",
   3.282 +      Markup.BOUND -> "bound variable",
   3.283 +      Markup.VAR -> "schematic variable",
   3.284 +      Markup.TFREE -> "free type variable",
   3.285 +      Markup.TVAR -> "schematic type variable",
   3.286 +      Markup.ML_SOURCE -> "ML source",
   3.287 +      Markup.DOCUMENT_SOURCE -> "document source")
   3.288 +
   3.289 +  private val tooltip_elements =
   3.290 +    Set(Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.ML_TYPING, Markup.PATH) ++
   3.291 +      tooltips.keys
   3.292 +
   3.293 +  private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
   3.294 +    Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
   3.295 +
   3.296 +  def tooltip(range: Text.Range): XML.Body =
   3.297 +  {
   3.298 +    def add(prev: Text.Info[List[(Boolean, XML.Tree)]], r: Text.Range, p: (Boolean, XML.Tree)) =
   3.299 +      if (prev.range == r) Text.Info(r, p :: prev.info) else Text.Info(r, List(p))
   3.300 +
   3.301 +    val tips =
   3.302 +      snapshot.cumulate_markup[Text.Info[(List[(Boolean, XML.Tree)])]](
   3.303 +        range, Text.Info(range, Nil), Some(tooltip_elements),
   3.304 +        {
   3.305 +          case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
   3.306 +            val kind1 = space_explode('_', kind).mkString(" ")
   3.307 +            add(prev, r, (true, XML.Text(kind1 + " " + quote(name))))
   3.308 +          case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
   3.309 +          if Path.is_ok(name) =>
   3.310 +            val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
   3.311 +            add(prev, r, (true, XML.Text("file " + quote(jedit_file))))
   3.312 +          case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
   3.313 +          if name == Markup.SORTING || name == Markup.TYPING =>
   3.314 +            add(prev, r, (true, pretty_typing("::", body)))
   3.315 +          case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
   3.316 +            add(prev, r, (false, pretty_typing("ML:", body)))
   3.317 +          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
   3.318 +          if tooltips.isDefinedAt(name) => add(prev, r, (true, XML.Text(tooltips(name))))
   3.319 +        }).toList.flatMap(_.info.info)
   3.320 +
   3.321 +    val all_tips =
   3.322 +      (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
   3.323 +    Library.separate(Pretty.FBreak, all_tips.toList)
   3.324 +  }
   3.325 +
   3.326 +
   3.327 +  def gutter_message(range: Text.Range): Option[Icon] =
   3.328 +  {
   3.329 +    val results =
   3.330 +      snapshot.cumulate_markup[Int](range, 0, Some(Set(Markup.WARNING, Markup.ERROR)),
   3.331 +        {
   3.332 +          case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
   3.333 +            body match {
   3.334 +              case List(XML.Elem(Markup(Markup.LEGACY, _), _)) =>
   3.335 +                pri max Rendering.legacy_pri
   3.336 +              case _ => pri max Rendering.warning_pri
   3.337 +            }
   3.338 +          case (pri, Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _))) =>
   3.339 +            pri max Rendering.error_pri
   3.340 +        })
   3.341 +    val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
   3.342 +    Rendering.gutter_icons.get(pri)
   3.343 +  }
   3.344 +
   3.345 +
   3.346 +  private val squiggly_colors = Map(
   3.347 +    Rendering.writeln_pri -> writeln_color,
   3.348 +    Rendering.warning_pri -> warning_color,
   3.349 +    Rendering.error_pri -> error_color)
   3.350 +
   3.351 +  def squiggly_underline(range: Text.Range): Stream[Text.Info[Color]] =
   3.352 +  {
   3.353 +    val results =
   3.354 +      snapshot.cumulate_markup[Int](range, 0,
   3.355 +        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)),
   3.356 +        {
   3.357 +          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
   3.358 +          if name == Markup.WRITELN ||
   3.359 +            name == Markup.WARNING ||
   3.360 +            name == Markup.ERROR => pri max Rendering.message_pri(name)
   3.361 +        })
   3.362 +    for {
   3.363 +      Text.Info(r, pri) <- results
   3.364 +      color <- squiggly_colors.get(pri)
   3.365 +    } yield Text.Info(r, color)
   3.366 +  }
   3.367 +
   3.368 +
   3.369 +  private val messages_include =
   3.370 +    Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE)
   3.371 +
   3.372 +  private val message_colors = Map(
   3.373 +    Rendering.writeln_pri -> writeln_message_color,
   3.374 +    Rendering.tracing_pri -> tracing_message_color,
   3.375 +    Rendering.warning_pri -> warning_message_color,
   3.376 +    Rendering.error_pri -> error_message_color)
   3.377 +
   3.378 +  def line_background(range: Text.Range): Option[(Color, Boolean)] =
   3.379 +  {
   3.380 +    val results =
   3.381 +      snapshot.cumulate_markup[Int](range, 0, Some(messages_include),
   3.382 +        {
   3.383 +          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
   3.384 +          if name == Markup.WRITELN_MESSAGE ||
   3.385 +            name == Markup.TRACING_MESSAGE ||
   3.386 +            name == Markup.WARNING_MESSAGE ||
   3.387 +            name == Markup.ERROR_MESSAGE => pri max Rendering.message_pri(name)
   3.388 +        })
   3.389 +    val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
   3.390 +
   3.391 +    val is_separator = pri > 0 &&
   3.392 +      snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)),
   3.393 +        {
   3.394 +          case (_, Text.Info(_, XML.Elem(Markup(Markup.SEPARATOR, _), _))) => true
   3.395 +        }).exists(_.info)
   3.396 +
   3.397 +    message_colors.get(pri).map((_, is_separator))
   3.398 +  }
   3.399 +
   3.400 +
   3.401 +  private val background1_include =
   3.402 +    Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
   3.403 +      Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY +
   3.404 +      Markup.SENDBACK
   3.405 +
   3.406 +  def background1(range: Text.Range): Stream[Text.Info[Color]] =
   3.407 +  {
   3.408 +    if (snapshot.is_outdated) Stream(Text.Info(range, outdated_color))
   3.409 +    else
   3.410 +      for {
   3.411 +        Text.Info(r, result) <-
   3.412 +          snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
   3.413 +            range, (Some(Protocol.Status.init), None), Some(background1_include),
   3.414 +            {
   3.415 +              case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
   3.416 +              if (Protocol.command_status_markup(markup.name)) =>
   3.417 +                (Some(Protocol.command_status(status, markup)), color)
   3.418 +              case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
   3.419 +                (None, Some(bad_color))
   3.420 +              case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   3.421 +                (None, Some(intensify_color))
   3.422 +              case (_, Text.Info(_, XML.Elem(Markup(Markup.SENDBACK, _), _))) =>
   3.423 +                (None, Some(sendback_color))
   3.424 +            })
   3.425 +        color <-
   3.426 +          (result match {
   3.427 +            case (Some(status), opt_color) =>
   3.428 +              if (status.is_unprocessed) Some(unprocessed1_color)
   3.429 +              else if (status.is_running) Some(running1_color)
   3.430 +              else opt_color
   3.431 +            case (_, opt_color) => opt_color
   3.432 +          })
   3.433 +      } yield Text.Info(r, color)
   3.434 +  }
   3.435 +
   3.436 +
   3.437 +  def background2(range: Text.Range): Stream[Text.Info[Color]] =
   3.438 +    snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)),
   3.439 +      {
   3.440 +        case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
   3.441 +      })
   3.442 +
   3.443 +
   3.444 +  def foreground(range: Text.Range): Stream[Text.Info[Color]] =
   3.445 +    snapshot.select_markup(range, Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)),
   3.446 +      {
   3.447 +        case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
   3.448 +        case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
   3.449 +        case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
   3.450 +      })
   3.451 +
   3.452 +
   3.453 +  private val text_colors: Map[String, Color] = Map(
   3.454 +      Markup.KEYWORD1 -> keyword1_color,
   3.455 +      Markup.KEYWORD2 -> keyword2_color,
   3.456 +      Markup.STRING -> Color.BLACK,
   3.457 +      Markup.ALTSTRING -> Color.BLACK,
   3.458 +      Markup.VERBATIM -> Color.BLACK,
   3.459 +      Markup.LITERAL -> keyword1_color,
   3.460 +      Markup.DELIMITER -> Color.BLACK,
   3.461 +      Markup.TFREE -> tfree_color,
   3.462 +      Markup.TVAR -> tvar_color,
   3.463 +      Markup.FREE -> free_color,
   3.464 +      Markup.SKOLEM -> skolem_color,
   3.465 +      Markup.BOUND -> bound_color,
   3.466 +      Markup.VAR -> var_color,
   3.467 +      Markup.INNER_STRING -> inner_quoted_color,
   3.468 +      Markup.INNER_COMMENT -> inner_comment_color,
   3.469 +      Markup.DYNAMIC_FACT -> dynamic_color,
   3.470 +      Markup.ML_KEYWORD -> keyword1_color,
   3.471 +      Markup.ML_DELIMITER -> Color.BLACK,
   3.472 +      Markup.ML_NUMERAL -> inner_numeral_color,
   3.473 +      Markup.ML_CHAR -> inner_quoted_color,
   3.474 +      Markup.ML_STRING -> inner_quoted_color,
   3.475 +      Markup.ML_COMMENT -> inner_comment_color,
   3.476 +      Markup.ANTIQ -> antiquotation_color)
   3.477 +
   3.478 +  private val text_color_elements = Set.empty[String] ++ text_colors.keys
   3.479 +
   3.480 +  def text_color(range: Text.Range, color: Color)
   3.481 +      : Stream[Text.Info[Color]] =
   3.482 +  {
   3.483 +    if (color == Token_Markup.hidden_color) Stream(Text.Info(range, color))
   3.484 +    else
   3.485 +      snapshot.cumulate_markup(range, color, Some(text_color_elements),
   3.486 +        {
   3.487 +          case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
   3.488 +          if text_colors.isDefinedAt(m) => text_colors(m)
   3.489 +        })
   3.490 +  }
   3.491 +}