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