src/Pure/PIDE/rendering.scala
author wenzelm
Tue Mar 07 17:21:41 2017 +0100 (2017-03-07)
changeset 65143 36cd85caf09a
parent 65139 0a2c0712e432
child 65144 b5782e996651
permissions -rw-r--r--
tuned;
wenzelm@64622
     1
/*  Title:      Pure/PIDE/rendering.scala
wenzelm@64622
     2
    Author:     Makarius
wenzelm@64622
     3
wenzelm@64622
     4
Isabelle-specific implementation of quasi-abstract rendering and
wenzelm@64622
     5
markup interpretation.
wenzelm@64622
     6
*/
wenzelm@64622
     7
wenzelm@64622
     8
package isabelle
wenzelm@64622
     9
wenzelm@64622
    10
wenzelm@64622
    11
object Rendering
wenzelm@64622
    12
{
wenzelm@65101
    13
  /* color */
wenzelm@65101
    14
wenzelm@65101
    15
  object Color extends Enumeration
wenzelm@65101
    16
  {
wenzelm@65104
    17
    // background
wenzelm@65101
    18
    val unprocessed1 = Value("unprocessed1")
wenzelm@65101
    19
    val running1 = Value("running1")
wenzelm@65101
    20
    val bad = Value("bad")
wenzelm@65101
    21
    val intensify = Value("intensify")
wenzelm@65101
    22
    val entity = Value("entity")
wenzelm@65101
    23
    val active = Value("active")
wenzelm@65101
    24
    val active_result = Value("active_result")
wenzelm@65101
    25
    val markdown_item1 = Value("markdown_item1")
wenzelm@65101
    26
    val markdown_item2 = Value("markdown_item2")
wenzelm@65101
    27
    val markdown_item3 = Value("markdown_item3")
wenzelm@65101
    28
    val markdown_item4 = Value("markdown_item4")
wenzelm@65143
    29
    val background_colors = values
wenzelm@65104
    30
wenzelm@65104
    31
    // foreground
wenzelm@65104
    32
    val quoted = Value("quoted")
wenzelm@65104
    33
    val antiquoted = Value("antiquoted")
wenzelm@65143
    34
    val foreground_colors = values -- background_colors
wenzelm@65121
    35
wenzelm@65124
    36
    // message underline
wenzelm@65121
    37
    val writeln = Value("writeln")
wenzelm@65121
    38
    val information = Value("information")
wenzelm@65121
    39
    val warning = Value("warning")
wenzelm@65121
    40
    val legacy = Value("legacy")
wenzelm@65121
    41
    val error = Value("error")
wenzelm@65143
    42
    val message_underline_colors = values -- background_colors -- foreground_colors
wenzelm@65124
    43
wenzelm@65124
    44
    // message background
wenzelm@65124
    45
    val writeln_message = Value("writeln_message")
wenzelm@65124
    46
    val information_message = Value("information_message")
wenzelm@65124
    47
    val tracing_message = Value("tracing_message")
wenzelm@65124
    48
    val warning_message = Value("warning_message")
wenzelm@65124
    49
    val legacy_message = Value("legacy_message")
wenzelm@65124
    50
    val error_message = Value("error_message")
wenzelm@65143
    51
    val message_background_colors =
wenzelm@65143
    52
      values -- background_colors -- foreground_colors -- message_underline_colors
wenzelm@65101
    53
  }
wenzelm@65101
    54
wenzelm@65101
    55
wenzelm@64676
    56
  /* message priorities */
wenzelm@64676
    57
wenzelm@64676
    58
  val state_pri = 1
wenzelm@64676
    59
  val writeln_pri = 2
wenzelm@64676
    60
  val information_pri = 3
wenzelm@64676
    61
  val tracing_pri = 4
wenzelm@64676
    62
  val warning_pri = 5
wenzelm@64676
    63
  val legacy_pri = 6
wenzelm@64676
    64
  val error_pri = 7
wenzelm@64676
    65
wenzelm@64676
    66
  val message_pri = Map(
wenzelm@64676
    67
    Markup.STATE -> state_pri,
wenzelm@64676
    68
    Markup.STATE_MESSAGE -> state_pri,
wenzelm@64676
    69
    Markup.WRITELN -> writeln_pri,
wenzelm@64676
    70
    Markup.WRITELN_MESSAGE -> writeln_pri,
wenzelm@64676
    71
    Markup.INFORMATION -> information_pri,
wenzelm@64676
    72
    Markup.INFORMATION_MESSAGE -> information_pri,
wenzelm@64676
    73
    Markup.TRACING -> tracing_pri,
wenzelm@64676
    74
    Markup.TRACING_MESSAGE -> tracing_pri,
wenzelm@64676
    75
    Markup.WARNING -> warning_pri,
wenzelm@64676
    76
    Markup.WARNING_MESSAGE -> warning_pri,
wenzelm@64676
    77
    Markup.LEGACY -> legacy_pri,
wenzelm@64676
    78
    Markup.LEGACY_MESSAGE -> legacy_pri,
wenzelm@64676
    79
    Markup.ERROR -> error_pri,
wenzelm@65133
    80
    Markup.ERROR_MESSAGE -> error_pri
wenzelm@65133
    81
  ).withDefaultValue(0)
wenzelm@64676
    82
wenzelm@65121
    83
  val message_underline_color = Map(
wenzelm@65121
    84
    writeln_pri -> Color.writeln,
wenzelm@65121
    85
    information_pri -> Color.information,
wenzelm@65121
    86
    warning_pri -> Color.warning,
wenzelm@65121
    87
    legacy_pri -> Color.legacy,
wenzelm@65121
    88
    error_pri -> Color.error)
wenzelm@65121
    89
wenzelm@65124
    90
  val message_background_color = Map(
wenzelm@65124
    91
    writeln_pri -> Color.writeln_message,
wenzelm@65124
    92
    information_pri -> Color.information_message,
wenzelm@65124
    93
    tracing_pri -> Color.tracing_message,
wenzelm@65124
    94
    warning_pri -> Color.warning_message,
wenzelm@65124
    95
    legacy_pri -> Color.legacy_message,
wenzelm@65124
    96
    error_pri -> Color.error_message)
wenzelm@65124
    97
wenzelm@64676
    98
wenzelm@64676
    99
  /* markup elements */
wenzelm@64676
   100
wenzelm@65101
   101
  val active_elements =
wenzelm@65101
   102
    Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
wenzelm@65101
   103
      Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
wenzelm@65101
   104
wenzelm@65101
   105
  private val background_elements =
wenzelm@65101
   106
    Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
wenzelm@65101
   107
      Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
wenzelm@65101
   108
      Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
wenzelm@65101
   109
      Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
wenzelm@65101
   110
      Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
wenzelm@65101
   111
      Markup.Markdown_Item.name ++ active_elements
wenzelm@65101
   112
wenzelm@65101
   113
  private val foreground_elements =
wenzelm@65101
   114
    Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
wenzelm@65101
   115
      Markup.CARTOUCHE, Markup.ANTIQUOTED)
wenzelm@65101
   116
wenzelm@64877
   117
  private val semantic_completion_elements =
wenzelm@64877
   118
    Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
wenzelm@64877
   119
wenzelm@64622
   120
  private val tooltip_descriptions =
wenzelm@64622
   121
    Map(
wenzelm@64622
   122
      Markup.CITATION -> "citation",
wenzelm@64622
   123
      Markup.TOKEN_RANGE -> "inner syntax token",
wenzelm@64622
   124
      Markup.FREE -> "free variable",
wenzelm@64622
   125
      Markup.SKOLEM -> "skolem variable",
wenzelm@64622
   126
      Markup.BOUND -> "bound variable",
wenzelm@64622
   127
      Markup.VAR -> "schematic variable",
wenzelm@64622
   128
      Markup.TFREE -> "free type variable",
wenzelm@64622
   129
      Markup.TVAR -> "schematic type variable")
wenzelm@64622
   130
wenzelm@65129
   131
  val tooltip_elements =
wenzelm@64622
   132
    Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
wenzelm@64622
   133
      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
wenzelm@64622
   134
      Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
wenzelm@64622
   135
      Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
wenzelm@64622
   136
wenzelm@65129
   137
  val tooltip_message_elements =
wenzelm@65129
   138
    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
wenzelm@65129
   139
      Markup.BAD)
wenzelm@65129
   140
wenzelm@64622
   141
  private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
wenzelm@64622
   142
    Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
wenzelm@64767
   143
wenzelm@64767
   144
  val caret_focus_elements = Markup.Elements(Markup.ENTITY)
wenzelm@64622
   145
}
wenzelm@64622
   146
wenzelm@64622
   147
abstract class Rendering(
wenzelm@64622
   148
  val snapshot: Document.Snapshot,
wenzelm@64622
   149
  val options: Options,
wenzelm@64622
   150
  val resources: Resources)
wenzelm@64622
   151
{
wenzelm@64622
   152
  override def toString: String = "Rendering(" + snapshot.toString + ")"
wenzelm@64622
   153
wenzelm@64622
   154
wenzelm@64877
   155
  /* completion */
wenzelm@64877
   156
wenzelm@64877
   157
  def semantic_completion(completed_range: Option[Text.Range], range: Text.Range)
wenzelm@64877
   158
      : Option[Text.Info[Completion.Semantic]] =
wenzelm@64877
   159
    if (snapshot.is_outdated) None
wenzelm@64877
   160
    else {
wenzelm@64877
   161
      snapshot.select(range, Rendering.semantic_completion_elements, _ =>
wenzelm@64877
   162
        {
wenzelm@64877
   163
          case Completion.Semantic.Info(info) =>
wenzelm@64877
   164
            completed_range match {
wenzelm@64877
   165
              case Some(range0) if range0.contains(info.range) && range0 != info.range => None
wenzelm@64877
   166
              case _ => Some(info)
wenzelm@64877
   167
            }
wenzelm@64877
   168
          case _ => None
wenzelm@64877
   169
        }).headOption.map(_.info)
wenzelm@64877
   170
    }
wenzelm@64877
   171
wenzelm@64877
   172
wenzelm@65139
   173
  /* spell checker */
wenzelm@65139
   174
wenzelm@65139
   175
  private lazy val spell_checker_elements =
wenzelm@65139
   176
    Markup.Elements(space_explode(',', options.string("spell_checker_elements")): _*)
wenzelm@65139
   177
wenzelm@65139
   178
  def spell_checker_ranges(range: Text.Range): List[Text.Range] =
wenzelm@65139
   179
    snapshot.select(range, spell_checker_elements, _ => _ => Some(())).map(_.range)
wenzelm@65139
   180
wenzelm@65139
   181
  def spell_checker_point(range: Text.Range): Option[Text.Range] =
wenzelm@65139
   182
    snapshot.select(range, spell_checker_elements, _ =>
wenzelm@65139
   183
      {
wenzelm@65139
   184
        case info => Some(snapshot.convert(info.range))
wenzelm@65139
   185
      }).headOption.map(_.info)
wenzelm@65139
   186
wenzelm@65139
   187
wenzelm@64622
   188
  /* tooltips */
wenzelm@64622
   189
wenzelm@64622
   190
  def timing_threshold: Double
wenzelm@64622
   191
wenzelm@65129
   192
  private sealed case class Tooltip_Info(
wenzelm@65129
   193
    range: Text.Range,
wenzelm@65129
   194
    timing: Timing = Timing.zero,
wenzelm@65129
   195
    messages: List[Command.Results.Entry] = Nil,
wenzelm@65129
   196
    rev_infos: List[(Boolean, XML.Tree)] = Nil)
wenzelm@64622
   197
  {
wenzelm@65129
   198
    def + (t: Timing): Tooltip_Info = copy(timing = timing + t)
wenzelm@65129
   199
    def + (r0: Text.Range, serial: Long, tree: XML.Tree): Tooltip_Info =
wenzelm@65129
   200
    {
wenzelm@65129
   201
      val r = snapshot.convert(r0)
wenzelm@65129
   202
      if (range == r) copy(messages = (serial -> tree) :: messages)
wenzelm@65129
   203
      else copy(range = r, messages = List(serial -> tree))
wenzelm@65129
   204
    }
wenzelm@65129
   205
    def + (r0: Text.Range, important: Boolean, tree: XML.Tree): Tooltip_Info =
wenzelm@64622
   206
    {
wenzelm@64622
   207
      val r = snapshot.convert(r0)
wenzelm@65129
   208
      if (range == r) copy(rev_infos = (important -> tree) :: rev_infos)
wenzelm@65129
   209
      else copy (range = r, rev_infos = List(important -> tree))
wenzelm@64622
   210
    }
wenzelm@65129
   211
    def infos(important: Boolean): List[XML.Tree] =
wenzelm@65129
   212
      rev_infos.filter(p => p._1 == important).reverse.map(_._2)
wenzelm@65129
   213
  }
wenzelm@64622
   214
wenzelm@65129
   215
  def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
wenzelm@65129
   216
  {
wenzelm@64622
   217
    val results =
wenzelm@65129
   218
      snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, _ =>
wenzelm@64622
   219
        {
wenzelm@65129
   220
          case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info + t)
wenzelm@64622
   221
wenzelm@65129
   222
          case (info, Text.Info(r0, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
wenzelm@65129
   223
          if Rendering.tooltip_message_elements(name) && body.nonEmpty =>
wenzelm@65129
   224
            Some(info + (r0, serial, XML.Elem(Markup(Markup.message(name), props), body)))
wenzelm@65129
   225
wenzelm@65129
   226
          case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _)))
wenzelm@64660
   227
          if kind != "" && kind != Markup.ML_DEF =>
wenzelm@64622
   228
            val kind1 = Word.implode(Word.explode('_', kind))
wenzelm@64622
   229
            val txt1 =
wenzelm@64622
   230
              if (name == "") kind1
wenzelm@64622
   231
              else if (kind1 == "") quote(name)
wenzelm@64622
   232
              else kind1 + " " + quote(name)
wenzelm@64622
   233
            val txt2 =
wenzelm@65129
   234
              if (kind == Markup.COMMAND && info.timing.elapsed.seconds >= timing_threshold)
wenzelm@65129
   235
                "\n" + info.timing.message
wenzelm@64622
   236
              else ""
wenzelm@65129
   237
            Some(info + (r0, true, XML.Text(txt1 + txt2)))
wenzelm@64622
   238
wenzelm@65129
   239
          case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
wenzelm@64654
   240
            val file = resources.append_file(snapshot.node_name.master_dir, name)
wenzelm@64622
   241
            val text =
wenzelm@64622
   242
              if (name == file) "file " + quote(file)
wenzelm@64622
   243
              else "path " + quote(name) + "\nfile " + quote(file)
wenzelm@65129
   244
            Some(info + (r0, true, XML.Text(text)))
wenzelm@64622
   245
wenzelm@65129
   246
          case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) =>
wenzelm@64622
   247
            val text = "doc " + quote(name)
wenzelm@65129
   248
            Some(info + (r0, true, XML.Text(text)))
wenzelm@64622
   249
wenzelm@65129
   250
          case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) =>
wenzelm@65129
   251
            Some(info + (r0, true, XML.Text("URL " + quote(name))))
wenzelm@64622
   252
wenzelm@65129
   253
          case (info, Text.Info(r0, XML.Elem(Markup(name, _), body)))
wenzelm@64622
   254
          if name == Markup.SORTING || name == Markup.TYPING =>
wenzelm@65129
   255
            Some(info + (r0, true, Rendering.pretty_typing("::", body)))
wenzelm@64622
   256
wenzelm@65129
   257
          case (info, Text.Info(r0, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
wenzelm@65129
   258
            Some(info + (r0, true, Pretty.block(0, body)))
wenzelm@64622
   259
wenzelm@65129
   260
          case (info, Text.Info(r0, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
wenzelm@65129
   261
            Some(info + (r0, false, Rendering.pretty_typing("ML:", body)))
wenzelm@64622
   262
wenzelm@65129
   263
          case (info, Text.Info(r0, Protocol.ML_Breakpoint(breakpoint))) =>
wenzelm@64622
   264
            val text =
wenzelm@64622
   265
              if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
wenzelm@64622
   266
              else "breakpoint (disabled)"
wenzelm@65129
   267
            Some(info + (r0, true, XML.Text(text)))
wenzelm@64622
   268
wenzelm@65129
   269
          case (info, Text.Info(r0, XML.Elem(Markup.Language(language, _, _, _), _))) =>
wenzelm@64622
   270
            val lang = Word.implode(Word.explode('_', language))
wenzelm@65129
   271
            Some(info + (r0, true, XML.Text("language: " + lang)))
wenzelm@64622
   272
wenzelm@65129
   273
          case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) =>
wenzelm@64622
   274
            val descr = if (kind == "") "expression" else "expression: " + kind
wenzelm@65129
   275
            Some(info + (r0, true, XML.Text(descr)))
wenzelm@64622
   276
wenzelm@65129
   277
          case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
wenzelm@65129
   278
            Some(info + (r0, true, XML.Text("Markdown: paragraph")))
wenzelm@65129
   279
          case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) =>
wenzelm@65129
   280
            Some(info + (r0, true, XML.Text("Markdown: " + kind)))
wenzelm@64622
   281
wenzelm@65129
   282
          case (info, Text.Info(r0, XML.Elem(Markup(name, _), _))) =>
wenzelm@65129
   283
            Rendering.tooltip_descriptions.get(name).map(desc => info + (r0, true, XML.Text(desc)))
wenzelm@64622
   284
        }).map(_.info)
wenzelm@64622
   285
wenzelm@65129
   286
    if (results.isEmpty) None
wenzelm@65129
   287
    else {
wenzelm@65129
   288
      val r = Text.Range(results.head.range.start, results.last.range.stop)
wenzelm@65129
   289
      val all_tips =
wenzelm@65129
   290
        Command.Results.make(results.flatMap(_.messages)).iterator.map(_._2).toList :::
wenzelm@65129
   291
        results.flatMap(res => res.infos(true)) :::
wenzelm@65129
   292
        results.flatMap(res => res.infos(false)).lastOption.toList
wenzelm@65129
   293
      if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips))
wenzelm@64622
   294
    }
wenzelm@64622
   295
  }
wenzelm@64767
   296
wenzelm@64767
   297
wenzelm@65101
   298
  /* text background */
wenzelm@65101
   299
wenzelm@65101
   300
  def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Rendering.Color.Value]] =
wenzelm@65101
   301
  {
wenzelm@65101
   302
    for {
wenzelm@65101
   303
      Text.Info(r, result) <-
wenzelm@65101
   304
        snapshot.cumulate[(List[Markup], Option[Rendering.Color.Value])](
wenzelm@65101
   305
          range, (List(Markup.Empty), None), Rendering.background_elements,
wenzelm@65101
   306
          command_states =>
wenzelm@65101
   307
            {
wenzelm@65101
   308
              case (((markups, color), Text.Info(_, XML.Elem(markup, _))))
wenzelm@65101
   309
              if markups.nonEmpty && Protocol.proper_status_elements(markup.name) =>
wenzelm@65101
   310
                Some((markup :: markups, color))
wenzelm@65101
   311
              case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
wenzelm@65101
   312
                Some((Nil, Some(Rendering.Color.bad)))
wenzelm@65101
   313
              case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
wenzelm@65101
   314
                Some((Nil, Some(Rendering.Color.intensify)))
wenzelm@65101
   315
              case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
wenzelm@65101
   316
                props match {
wenzelm@65101
   317
                  case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
wenzelm@65101
   318
                  case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
wenzelm@65101
   319
                  case _ => None
wenzelm@65101
   320
                }
wenzelm@65101
   321
              case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) =>
wenzelm@65101
   322
                val color =
wenzelm@65101
   323
                  depth match {
wenzelm@65101
   324
                    case 1 => Rendering.Color.markdown_item1
wenzelm@65101
   325
                    case 2 => Rendering.Color.markdown_item2
wenzelm@65101
   326
                    case 3 => Rendering.Color.markdown_item3
wenzelm@65101
   327
                    case _ => Rendering.Color.markdown_item4
wenzelm@65101
   328
                  }
wenzelm@65101
   329
                Some((Nil, Some(color)))
wenzelm@65101
   330
              case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
wenzelm@65101
   331
                command_states.collectFirst(
wenzelm@65101
   332
                  { case st if st.results.defined(serial) => st.results.get(serial).get }) match
wenzelm@65101
   333
                {
wenzelm@65101
   334
                  case Some(Protocol.Dialog_Result(res)) if res == result =>
wenzelm@65101
   335
                    Some((Nil, Some(Rendering.Color.active_result)))
wenzelm@65101
   336
                  case _ =>
wenzelm@65101
   337
                    Some((Nil, Some(Rendering.Color.active)))
wenzelm@65101
   338
                }
wenzelm@65101
   339
              case (_, Text.Info(_, elem)) =>
wenzelm@65101
   340
                if (Rendering.active_elements(elem.name))
wenzelm@65101
   341
                  Some((Nil, Some(Rendering.Color.active)))
wenzelm@65101
   342
                else None
wenzelm@65101
   343
            })
wenzelm@65101
   344
      color <-
wenzelm@65101
   345
        (result match {
wenzelm@65101
   346
          case (markups, opt_color) if markups.nonEmpty =>
wenzelm@65101
   347
            val status = Protocol.Status.make(markups.iterator)
wenzelm@65101
   348
            if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
wenzelm@65101
   349
            else if (status.is_running) Some(Rendering.Color.running1)
wenzelm@65101
   350
            else opt_color
wenzelm@65101
   351
          case (_, opt_color) => opt_color
wenzelm@65101
   352
        })
wenzelm@65101
   353
    } yield Text.Info(r, color)
wenzelm@65101
   354
  }
wenzelm@65101
   355
wenzelm@65101
   356
wenzelm@65101
   357
  /* text foreground */
wenzelm@65101
   358
wenzelm@65101
   359
  def foreground(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
wenzelm@65101
   360
    snapshot.select(range, Rendering.foreground_elements, _ =>
wenzelm@65101
   361
      {
wenzelm@65101
   362
        case Text.Info(_, elem) =>
wenzelm@65101
   363
          if (elem.name == Markup.ANTIQUOTED) Some(Rendering.Color.antiquoted)
wenzelm@65101
   364
          else Some(Rendering.Color.quoted)
wenzelm@65101
   365
      })
wenzelm@65101
   366
wenzelm@65101
   367
wenzelm@64767
   368
  /* caret focus */
wenzelm@64767
   369
wenzelm@64767
   370
  private def entity_focus(range: Text.Range,
wenzelm@64767
   371
    check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] =
wenzelm@64767
   372
  {
wenzelm@64767
   373
    val results =
wenzelm@64767
   374
      snapshot.cumulate[Set[Long]](range, Set.empty, Rendering.caret_focus_elements, _ =>
wenzelm@64767
   375
          {
wenzelm@64767
   376
            case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
wenzelm@64767
   377
              props match {
wenzelm@64767
   378
                case Markup.Entity.Def(i) if check(true, i) => Some(serials + i)
wenzelm@64767
   379
                case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
wenzelm@64767
   380
                case _ => None
wenzelm@64767
   381
              }
wenzelm@64767
   382
            case _ => None
wenzelm@64767
   383
          })
wenzelm@64767
   384
    (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
wenzelm@64767
   385
  }
wenzelm@64767
   386
wenzelm@64767
   387
  def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
wenzelm@64767
   388
  {
wenzelm@64767
   389
    val focus_defs = entity_focus(caret_range)
wenzelm@64767
   390
    if (focus_defs.nonEmpty) focus_defs
wenzelm@64767
   391
    else {
wenzelm@64767
   392
      val visible_defs = entity_focus(visible_range)
wenzelm@64767
   393
      entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i))
wenzelm@64767
   394
    }
wenzelm@64767
   395
  }
wenzelm@64767
   396
wenzelm@64767
   397
  def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
wenzelm@64767
   398
  {
wenzelm@64767
   399
    val focus = caret_focus(caret_range, visible_range)
wenzelm@64767
   400
    if (focus.nonEmpty) {
wenzelm@64767
   401
      val results =
wenzelm@64767
   402
        snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ =>
wenzelm@64767
   403
          {
wenzelm@64767
   404
            case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
wenzelm@64767
   405
              props match {
wenzelm@64767
   406
                case Markup.Entity.Def(i) if focus(i) => Some(true)
wenzelm@64767
   407
                case Markup.Entity.Ref(i) if focus(i) => Some(true)
wenzelm@64767
   408
                case _ => None
wenzelm@64767
   409
              }
wenzelm@64767
   410
          })
wenzelm@64767
   411
      for (info <- results if info.info) yield info.range
wenzelm@64767
   412
    }
wenzelm@64767
   413
    else Nil
wenzelm@64767
   414
  }
wenzelm@65121
   415
wenzelm@65121
   416
wenzelm@65121
   417
  /* message underline color */
wenzelm@65121
   418
wenzelm@65129
   419
  def message_underline_color(elements: Markup.Elements, range: Text.Range)
wenzelm@65129
   420
    : List[Text.Info[Rendering.Color.Value]] =
wenzelm@65121
   421
  {
wenzelm@65121
   422
    val results =
wenzelm@65121
   423
      snapshot.cumulate[Int](range, 0, elements, _ =>
wenzelm@65121
   424
        {
wenzelm@65121
   425
          case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
wenzelm@65121
   426
        })
wenzelm@65121
   427
    for {
wenzelm@65121
   428
      Text.Info(r, pri) <- results
wenzelm@65121
   429
      color <- Rendering.message_underline_color.get(pri)
wenzelm@65121
   430
    } yield Text.Info(r, color)
wenzelm@65121
   431
  }
wenzelm@64622
   432
}