src/Pure/PIDE/rendering.scala
author wenzelm
Sat Sep 01 20:20:50 2018 +0200 (10 months ago)
changeset 68871 f5c76072db55
parent 68822 253f04c1e814
child 69320 fc221fa79741
permissions -rw-r--r--
more explicit status for "canceled" command within theory node;
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@66158
    11
import java.io.{File => JFile}
wenzelm@66158
    12
import java.nio.file.FileSystems
wenzelm@66158
    13
wenzelm@66158
    14
wenzelm@64622
    15
object Rendering
wenzelm@64622
    16
{
wenzelm@65101
    17
  /* color */
wenzelm@65101
    18
wenzelm@65101
    19
  object Color extends Enumeration
wenzelm@65101
    20
  {
wenzelm@65104
    21
    // background
wenzelm@68871
    22
    val unprocessed1, running1, canceled, bad, intensify, entity, active, active_result,
wenzelm@67322
    23
      markdown_bullet1, markdown_bullet2, markdown_bullet3, markdown_bullet4 = Value
wenzelm@65143
    24
    val background_colors = values
wenzelm@65104
    25
wenzelm@65104
    26
    // foreground
wenzelm@65637
    27
    val quoted, antiquoted = Value
wenzelm@65143
    28
    val foreground_colors = values -- background_colors
wenzelm@65121
    29
wenzelm@65124
    30
    // message underline
wenzelm@65637
    31
    val writeln, information, warning, legacy, error = Value
wenzelm@65143
    32
    val message_underline_colors = values -- background_colors -- foreground_colors
wenzelm@65124
    33
wenzelm@65124
    34
    // message background
wenzelm@65637
    35
    val writeln_message, information_message, tracing_message,
wenzelm@65637
    36
      warning_message, legacy_message, error_message = Value
wenzelm@65143
    37
    val message_background_colors =
wenzelm@65143
    38
      values -- background_colors -- foreground_colors -- message_underline_colors
wenzelm@65144
    39
wenzelm@65144
    40
    // text
wenzelm@65637
    41
    val main, keyword1, keyword2, keyword3, quasi_keyword, improper, operator,
wenzelm@65637
    42
      tfree, tvar, free, skolem, bound, `var`, inner_numeral, inner_quoted,
wenzelm@65637
    43
      inner_cartouche, inner_comment, dynamic, class_parameter, antiquote = Value
wenzelm@65144
    44
    val text_colors =
wenzelm@65144
    45
      values -- background_colors -- foreground_colors -- message_underline_colors --
wenzelm@65144
    46
      message_background_colors
wenzelm@65911
    47
wenzelm@65913
    48
    // text overview
wenzelm@65911
    49
    val unprocessed, running = Value
wenzelm@65913
    50
    val text_overview_colors = Set(unprocessed, running, error, warning)
wenzelm@65101
    51
  }
wenzelm@65101
    52
wenzelm@65101
    53
wenzelm@65190
    54
  /* output messages */
wenzelm@64676
    55
wenzelm@64676
    56
  val state_pri = 1
wenzelm@64676
    57
  val writeln_pri = 2
wenzelm@64676
    58
  val information_pri = 3
wenzelm@64676
    59
  val tracing_pri = 4
wenzelm@64676
    60
  val warning_pri = 5
wenzelm@64676
    61
  val legacy_pri = 6
wenzelm@64676
    62
  val error_pri = 7
wenzelm@64676
    63
wenzelm@64676
    64
  val message_pri = Map(
wenzelm@64676
    65
    Markup.STATE -> state_pri,
wenzelm@64676
    66
    Markup.STATE_MESSAGE -> state_pri,
wenzelm@64676
    67
    Markup.WRITELN -> writeln_pri,
wenzelm@64676
    68
    Markup.WRITELN_MESSAGE -> writeln_pri,
wenzelm@64676
    69
    Markup.INFORMATION -> information_pri,
wenzelm@64676
    70
    Markup.INFORMATION_MESSAGE -> information_pri,
wenzelm@64676
    71
    Markup.TRACING -> tracing_pri,
wenzelm@64676
    72
    Markup.TRACING_MESSAGE -> tracing_pri,
wenzelm@64676
    73
    Markup.WARNING -> warning_pri,
wenzelm@64676
    74
    Markup.WARNING_MESSAGE -> warning_pri,
wenzelm@64676
    75
    Markup.LEGACY -> legacy_pri,
wenzelm@64676
    76
    Markup.LEGACY_MESSAGE -> legacy_pri,
wenzelm@64676
    77
    Markup.ERROR -> error_pri,
wenzelm@65133
    78
    Markup.ERROR_MESSAGE -> error_pri
wenzelm@65133
    79
  ).withDefaultValue(0)
wenzelm@64676
    80
wenzelm@65121
    81
  val message_underline_color = Map(
wenzelm@65121
    82
    writeln_pri -> Color.writeln,
wenzelm@65121
    83
    information_pri -> Color.information,
wenzelm@65121
    84
    warning_pri -> Color.warning,
wenzelm@65121
    85
    legacy_pri -> Color.legacy,
wenzelm@65121
    86
    error_pri -> Color.error)
wenzelm@65121
    87
wenzelm@65124
    88
  val message_background_color = Map(
wenzelm@65124
    89
    writeln_pri -> Color.writeln_message,
wenzelm@65124
    90
    information_pri -> Color.information_message,
wenzelm@65124
    91
    tracing_pri -> Color.tracing_message,
wenzelm@65124
    92
    warning_pri -> Color.warning_message,
wenzelm@65124
    93
    legacy_pri -> Color.legacy_message,
wenzelm@65124
    94
    error_pri -> Color.error_message)
wenzelm@65124
    95
wenzelm@65190
    96
  def output_messages(results: Command.Results): List[XML.Tree] =
wenzelm@65190
    97
  {
wenzelm@65190
    98
    val (states, other) =
wenzelm@65190
    99
      results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList
wenzelm@65190
   100
        .partition(Protocol.is_state(_))
wenzelm@65190
   101
    states ::: other
wenzelm@65190
   102
  }
wenzelm@65190
   103
wenzelm@64676
   104
wenzelm@65144
   105
  /* text color */
wenzelm@65144
   106
wenzelm@65144
   107
  val text_color = Map(
wenzelm@65144
   108
    Markup.KEYWORD1 -> Color.keyword1,
wenzelm@65144
   109
    Markup.KEYWORD2 -> Color.keyword2,
wenzelm@65144
   110
    Markup.KEYWORD3 -> Color.keyword3,
wenzelm@65144
   111
    Markup.QUASI_KEYWORD -> Color.quasi_keyword,
wenzelm@65144
   112
    Markup.IMPROPER -> Color.improper,
wenzelm@65144
   113
    Markup.OPERATOR -> Color.operator,
wenzelm@65145
   114
    Markup.STRING -> Color.main,
wenzelm@65145
   115
    Markup.ALT_STRING -> Color.main,
wenzelm@65145
   116
    Markup.VERBATIM -> Color.main,
wenzelm@65145
   117
    Markup.CARTOUCHE -> Color.main,
wenzelm@65144
   118
    Markup.LITERAL -> Color.keyword1,
wenzelm@65145
   119
    Markup.DELIMITER -> Color.main,
wenzelm@65144
   120
    Markup.TFREE -> Color.tfree,
wenzelm@65144
   121
    Markup.TVAR -> Color.tvar,
wenzelm@65144
   122
    Markup.FREE -> Color.free,
wenzelm@65144
   123
    Markup.SKOLEM -> Color.skolem,
wenzelm@65144
   124
    Markup.BOUND -> Color.bound,
wenzelm@65637
   125
    Markup.VAR -> Color.`var`,
wenzelm@65144
   126
    Markup.INNER_STRING -> Color.inner_quoted,
wenzelm@65144
   127
    Markup.INNER_CARTOUCHE -> Color.inner_cartouche,
wenzelm@65144
   128
    Markup.INNER_COMMENT -> Color.inner_comment,
wenzelm@65144
   129
    Markup.DYNAMIC_FACT -> Color.dynamic,
wenzelm@65144
   130
    Markup.CLASS_PARAMETER -> Color.class_parameter,
wenzelm@65144
   131
    Markup.ANTIQUOTE -> Color.antiquote,
wenzelm@65144
   132
    Markup.ML_KEYWORD1 -> Color.keyword1,
wenzelm@65144
   133
    Markup.ML_KEYWORD2 -> Color.keyword2,
wenzelm@65144
   134
    Markup.ML_KEYWORD3 -> Color.keyword3,
wenzelm@65145
   135
    Markup.ML_DELIMITER -> Color.main,
wenzelm@65144
   136
    Markup.ML_NUMERAL -> Color.inner_numeral,
wenzelm@65144
   137
    Markup.ML_CHAR -> Color.inner_quoted,
wenzelm@65144
   138
    Markup.ML_STRING -> Color.inner_quoted,
wenzelm@68822
   139
    Markup.ML_COMMENT -> Color.inner_comment)
wenzelm@65144
   140
wenzelm@66074
   141
  val foreground =
wenzelm@66074
   142
    Map(
wenzelm@66074
   143
      Markup.STRING -> Color.quoted,
wenzelm@66074
   144
      Markup.ALT_STRING -> Color.quoted,
wenzelm@66074
   145
      Markup.VERBATIM -> Color.quoted,
wenzelm@66074
   146
      Markup.CARTOUCHE -> Color.quoted,
wenzelm@66074
   147
      Markup.ANTIQUOTED -> Color.antiquoted)
wenzelm@66074
   148
wenzelm@65144
   149
wenzelm@65149
   150
  /* tooltips */
wenzelm@65101
   151
wenzelm@65149
   152
  val tooltip_descriptions =
wenzelm@64622
   153
    Map(
wenzelm@64622
   154
      Markup.CITATION -> "citation",
wenzelm@64622
   155
      Markup.TOKEN_RANGE -> "inner syntax token",
wenzelm@64622
   156
      Markup.FREE -> "free variable",
wenzelm@64622
   157
      Markup.SKOLEM -> "skolem variable",
wenzelm@64622
   158
      Markup.BOUND -> "bound variable",
wenzelm@64622
   159
      Markup.VAR -> "schematic variable",
wenzelm@64622
   160
      Markup.TFREE -> "free type variable",
wenzelm@64622
   161
      Markup.TVAR -> "schematic type variable")
wenzelm@64622
   162
wenzelm@65149
   163
wenzelm@65149
   164
  /* markup elements */
wenzelm@65149
   165
wenzelm@66053
   166
  val semantic_completion_elements =
wenzelm@66053
   167
    Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
wenzelm@66053
   168
wenzelm@66053
   169
  val language_context_elements =
wenzelm@66053
   170
    Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
wenzelm@66053
   171
      Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
wenzelm@66053
   172
      Markup.ML_STRING, Markup.ML_COMMENT)
wenzelm@66053
   173
wenzelm@66053
   174
  val language_elements = Markup.Elements(Markup.LANGUAGE)
wenzelm@66053
   175
wenzelm@66053
   176
  val citation_elements = Markup.Elements(Markup.CITATION)
wenzelm@66053
   177
wenzelm@65149
   178
  val active_elements =
wenzelm@65149
   179
    Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
wenzelm@65149
   180
      Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
wenzelm@65149
   181
wenzelm@65149
   182
  val background_elements =
wenzelm@68758
   183
    Document_Status.Command_Status.proper_elements + Markup.WRITELN_MESSAGE +
wenzelm@65149
   184
      Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
wenzelm@65149
   185
      Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
wenzelm@65149
   186
      Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
wenzelm@65149
   187
      Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
wenzelm@67322
   188
      Markup.Markdown_Bullet.name ++ active_elements
wenzelm@65149
   189
wenzelm@66074
   190
  val foreground_elements = Markup.Elements(foreground.keySet)
wenzelm@66074
   191
wenzelm@66074
   192
  val text_color_elements = Markup.Elements(text_color.keySet)
wenzelm@65149
   193
wenzelm@65129
   194
  val tooltip_elements =
wenzelm@64622
   195
    Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
wenzelm@64622
   196
      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
wenzelm@64622
   197
      Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
wenzelm@67323
   198
      Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) ++
wenzelm@67323
   199
      Markup.Elements(tooltip_descriptions.keySet)
wenzelm@64622
   200
wenzelm@65129
   201
  val tooltip_message_elements =
wenzelm@65129
   202
    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
wenzelm@65129
   203
      Markup.BAD)
wenzelm@65129
   204
wenzelm@64767
   205
  val caret_focus_elements = Markup.Elements(Markup.ENTITY)
wenzelm@67132
   206
wenzelm@67132
   207
  val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED)
wenzelm@67336
   208
wenzelm@67336
   209
  val markdown_elements =
wenzelm@67336
   210
    Markup.Elements(Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name,
wenzelm@67336
   211
      Markup.Markdown_Bullet.name)
wenzelm@64622
   212
}
wenzelm@64622
   213
wenzelm@64622
   214
abstract class Rendering(
wenzelm@64622
   215
  val snapshot: Document.Snapshot,
wenzelm@64622
   216
  val options: Options,
wenzelm@65213
   217
  val session: Session)
wenzelm@64622
   218
{
wenzelm@64622
   219
  override def toString: String = "Rendering(" + snapshot.toString + ")"
wenzelm@64622
   220
wenzelm@66114
   221
  def model: Document.Model
wenzelm@66114
   222
wenzelm@64622
   223
wenzelm@66117
   224
  /* caret */
wenzelm@66117
   225
wenzelm@66117
   226
  def before_caret_range(caret: Text.Offset): Text.Range =
wenzelm@66117
   227
  {
wenzelm@66117
   228
    val former_caret = snapshot.revert(caret)
wenzelm@66117
   229
    snapshot.convert(Text.Range(former_caret - 1, former_caret))
wenzelm@66117
   230
  }
wenzelm@66117
   231
wenzelm@66117
   232
wenzelm@64877
   233
  /* completion */
wenzelm@64877
   234
wenzelm@66054
   235
  def semantic_completion(completed_range: Option[Text.Range], caret_range: Text.Range)
wenzelm@64877
   236
      : Option[Text.Info[Completion.Semantic]] =
wenzelm@64877
   237
    if (snapshot.is_outdated) None
wenzelm@64877
   238
    else {
wenzelm@66054
   239
      snapshot.select(caret_range, Rendering.semantic_completion_elements, _ =>
wenzelm@64877
   240
        {
wenzelm@64877
   241
          case Completion.Semantic.Info(info) =>
wenzelm@64877
   242
            completed_range match {
wenzelm@64877
   243
              case Some(range0) if range0.contains(info.range) && range0 != info.range => None
wenzelm@64877
   244
              case _ => Some(info)
wenzelm@64877
   245
            }
wenzelm@64877
   246
          case _ => None
wenzelm@64877
   247
        }).headOption.map(_.info)
wenzelm@64877
   248
    }
wenzelm@64877
   249
wenzelm@66054
   250
  def semantic_completion_result(
wenzelm@66054
   251
    history: Completion.History,
wenzelm@66055
   252
    unicode: Boolean,
wenzelm@66054
   253
    completed_range: Option[Text.Range],
wenzelm@66114
   254
    caret_range: Text.Range): (Boolean, Option[Completion.Result]) =
wenzelm@66054
   255
  {
wenzelm@66054
   256
    semantic_completion(completed_range, caret_range) match {
wenzelm@66054
   257
      case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
wenzelm@66054
   258
      case Some(Text.Info(range, names: Completion.Names)) =>
wenzelm@67014
   259
        model.get_text(range) match {
wenzelm@66055
   260
          case Some(original) => (false, names.complete(range, history, unicode, original))
wenzelm@66054
   261
          case None => (false, None)
wenzelm@66054
   262
        }
wenzelm@66054
   263
      case None => (false, None)
wenzelm@66054
   264
    }
wenzelm@66054
   265
  }
wenzelm@66054
   266
wenzelm@66053
   267
  def language_context(range: Text.Range): Option[Completion.Language_Context] =
wenzelm@66053
   268
    snapshot.select(range, Rendering.language_context_elements, _ =>
wenzelm@66053
   269
      {
wenzelm@66053
   270
        case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) =>
wenzelm@66053
   271
          if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes))
wenzelm@66053
   272
          else None
wenzelm@66053
   273
        case Text.Info(_, elem)
wenzelm@66053
   274
        if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
wenzelm@66053
   275
          Some(Completion.Language_Context.ML_inner)
wenzelm@66053
   276
        case Text.Info(_, _) =>
wenzelm@66053
   277
          Some(Completion.Language_Context.inner)
wenzelm@66053
   278
      }).headOption.map(_.info)
wenzelm@66053
   279
wenzelm@66158
   280
  def citation(range: Text.Range): Option[Text.Info[String]] =
wenzelm@66158
   281
    snapshot.select(range, Rendering.citation_elements, _ =>
wenzelm@66158
   282
      {
wenzelm@66158
   283
        case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) =>
wenzelm@66158
   284
          Some(Text.Info(snapshot.convert(info_range), name))
wenzelm@66158
   285
        case _ => None
wenzelm@66158
   286
      }).headOption.map(_.info)
wenzelm@66158
   287
wenzelm@66158
   288
wenzelm@66158
   289
  /* file-system path completion */
wenzelm@66158
   290
wenzelm@66053
   291
  def language_path(range: Text.Range): Option[Text.Range] =
wenzelm@66053
   292
    snapshot.select(range, Rendering.language_elements, _ =>
wenzelm@66053
   293
      {
wenzelm@66053
   294
        case Text.Info(info_range, XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), _)) =>
wenzelm@66053
   295
          Some(snapshot.convert(info_range))
wenzelm@66053
   296
        case _ => None
wenzelm@66053
   297
      }).headOption.map(_.info)
wenzelm@66053
   298
wenzelm@66158
   299
  def path_completion(caret: Text.Offset): Option[Completion.Result] =
wenzelm@66158
   300
  {
wenzelm@66158
   301
    def complete(text: String): List[(String, List[String])] =
wenzelm@66158
   302
    {
wenzelm@66158
   303
      try {
wenzelm@66158
   304
        val path = Path.explode(text)
wenzelm@66158
   305
        val (dir, base_name) =
wenzelm@66158
   306
          if (text == "" || text.endsWith("/")) (path, "")
wenzelm@66158
   307
          else (path.dir, path.base_name)
wenzelm@66158
   308
wenzelm@66158
   309
        val directory = new JFile(session.resources.append(snapshot.node_name, dir))
wenzelm@66158
   310
        val files = directory.listFiles
wenzelm@66158
   311
        if (files == null) Nil
wenzelm@66158
   312
        else {
wenzelm@66158
   313
          val ignore =
wenzelm@66923
   314
            space_explode(':', options.string("completion_path_ignore")).
wenzelm@66158
   315
              map(s => FileSystems.getDefault.getPathMatcher("glob:" + s))
wenzelm@66158
   316
          (for {
wenzelm@66158
   317
            file <- files.iterator
wenzelm@66158
   318
wenzelm@66158
   319
            name = file.getName
wenzelm@66158
   320
            if name.startsWith(base_name)
wenzelm@66158
   321
            path_name = new JFile(name).toPath
wenzelm@66158
   322
            if !ignore.exists(matcher => matcher.matches(path_name))
wenzelm@66158
   323
wenzelm@66158
   324
            text1 = (dir + Path.basic(name)).implode_short
wenzelm@66158
   325
            if text != text1
wenzelm@66158
   326
wenzelm@66158
   327
            is_dir = new JFile(directory, name).isDirectory
wenzelm@66158
   328
            replacement = text1 + (if (is_dir) "/" else "")
wenzelm@66158
   329
            descr = List(text1, if (is_dir) "(directory)" else "(file)")
wenzelm@66158
   330
          } yield (replacement, descr)).take(options.int("completion_limit")).toList
wenzelm@66158
   331
        }
wenzelm@66158
   332
      }
wenzelm@66158
   333
      catch { case ERROR(_) => Nil }
wenzelm@66158
   334
    }
wenzelm@66158
   335
wenzelm@66158
   336
    def is_wrapped(s: String): Boolean =
wenzelm@66158
   337
      s.startsWith("\"") && s.endsWith("\"") ||
wenzelm@66158
   338
      s.startsWith(Symbol.open_decoded) && s.endsWith(Symbol.close_decoded)
wenzelm@66158
   339
wenzelm@66158
   340
    for {
wenzelm@66158
   341
      r1 <- language_path(before_caret_range(caret))
wenzelm@67014
   342
      s1 <- model.get_text(r1)
wenzelm@66158
   343
      if is_wrapped(s1)
wenzelm@66158
   344
      r2 = Text.Range(r1.start + 1, r1.stop - 1)
wenzelm@66158
   345
      s2 = s1.substring(1, s1.length - 1)
wenzelm@66158
   346
      if Path.is_valid(s2)
wenzelm@66158
   347
      paths = complete(s2)
wenzelm@66158
   348
      if paths.nonEmpty
wenzelm@66158
   349
      items = paths.map(p => Completion.Item(r2, s2, "", p._2, p._1, 0, false))
wenzelm@66158
   350
    } yield Completion.Result(r2, s2, false, items)
wenzelm@66158
   351
  }
wenzelm@66053
   352
wenzelm@64877
   353
wenzelm@65139
   354
  /* spell checker */
wenzelm@65139
   355
wenzelm@67395
   356
  private lazy val spell_checker_include =
wenzelm@67395
   357
    Markup.Elements(space_explode(',', options.string("spell_checker_include")): _*)
wenzelm@67395
   358
wenzelm@65139
   359
  private lazy val spell_checker_elements =
wenzelm@67395
   360
    spell_checker_include ++
wenzelm@67395
   361
      Markup.Elements(space_explode(',', options.string("spell_checker_exclude")): _*)
wenzelm@65139
   362
wenzelm@67395
   363
  def spell_checker(range: Text.Range): List[Text.Info[Text.Range]] =
wenzelm@67395
   364
  {
wenzelm@67395
   365
    val result =
wenzelm@67395
   366
      snapshot.select(range, spell_checker_elements, _ =>
wenzelm@67395
   367
        {
wenzelm@67395
   368
          case info =>
wenzelm@67395
   369
            Some(
wenzelm@67395
   370
              if (spell_checker_include(info.info.name))
wenzelm@67395
   371
                Some(snapshot.convert(info.range))
wenzelm@67395
   372
              else None)
wenzelm@67395
   373
        })
wenzelm@67395
   374
    for (Text.Info(range, Some(range1)) <- result)
wenzelm@67395
   375
      yield Text.Info(range, range1)
wenzelm@67395
   376
  }
wenzelm@65139
   377
wenzelm@65139
   378
  def spell_checker_point(range: Text.Range): Option[Text.Range] =
wenzelm@67395
   379
    spell_checker(range).headOption.map(_.info)
wenzelm@65139
   380
wenzelm@65139
   381
wenzelm@65101
   382
  /* text background */
wenzelm@65101
   383
wenzelm@65176
   384
  def background(elements: Markup.Elements, range: Text.Range, focus: Set[Long])
wenzelm@65176
   385
    : List[Text.Info[Rendering.Color.Value]] =
wenzelm@65101
   386
  {
wenzelm@65101
   387
    for {
wenzelm@65101
   388
      Text.Info(r, result) <-
wenzelm@65101
   389
        snapshot.cumulate[(List[Markup], Option[Rendering.Color.Value])](
wenzelm@65101
   390
          range, (List(Markup.Empty), None), Rendering.background_elements,
wenzelm@65101
   391
          command_states =>
wenzelm@65101
   392
            {
wenzelm@65101
   393
              case (((markups, color), Text.Info(_, XML.Elem(markup, _))))
wenzelm@68758
   394
              if markups.nonEmpty && Document_Status.Command_Status.proper_elements(markup.name) =>
wenzelm@65101
   395
                Some((markup :: markups, color))
wenzelm@65101
   396
              case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
wenzelm@65101
   397
                Some((Nil, Some(Rendering.Color.bad)))
wenzelm@65101
   398
              case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
wenzelm@65101
   399
                Some((Nil, Some(Rendering.Color.intensify)))
wenzelm@65101
   400
              case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
wenzelm@65101
   401
                props match {
wenzelm@65101
   402
                  case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
wenzelm@65101
   403
                  case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
wenzelm@65101
   404
                  case _ => None
wenzelm@65101
   405
                }
wenzelm@67322
   406
              case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) =>
wenzelm@65101
   407
                val color =
wenzelm@65150
   408
                  depth % 4 match {
wenzelm@67322
   409
                    case 1 => Rendering.Color.markdown_bullet1
wenzelm@67322
   410
                    case 2 => Rendering.Color.markdown_bullet2
wenzelm@67322
   411
                    case 3 => Rendering.Color.markdown_bullet3
wenzelm@67322
   412
                    case _ => Rendering.Color.markdown_bullet4
wenzelm@65101
   413
                  }
wenzelm@65101
   414
                Some((Nil, Some(color)))
wenzelm@65101
   415
              case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
wenzelm@65101
   416
                command_states.collectFirst(
wenzelm@65101
   417
                  { case st if st.results.defined(serial) => st.results.get(serial).get }) match
wenzelm@65101
   418
                {
wenzelm@65101
   419
                  case Some(Protocol.Dialog_Result(res)) if res == result =>
wenzelm@65101
   420
                    Some((Nil, Some(Rendering.Color.active_result)))
wenzelm@65101
   421
                  case _ =>
wenzelm@65101
   422
                    Some((Nil, Some(Rendering.Color.active)))
wenzelm@65101
   423
                }
wenzelm@65101
   424
              case (_, Text.Info(_, elem)) =>
wenzelm@65101
   425
                if (Rendering.active_elements(elem.name))
wenzelm@65101
   426
                  Some((Nil, Some(Rendering.Color.active)))
wenzelm@65101
   427
                else None
wenzelm@65101
   428
            })
wenzelm@65101
   429
      color <-
wenzelm@65101
   430
        (result match {
wenzelm@65101
   431
          case (markups, opt_color) if markups.nonEmpty =>
wenzelm@68758
   432
            val status = Document_Status.Command_Status.make(markups.iterator)
wenzelm@65101
   433
            if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
wenzelm@65101
   434
            else if (status.is_running) Some(Rendering.Color.running1)
wenzelm@68871
   435
            else if (status.is_canceled) Some(Rendering.Color.canceled)
wenzelm@65101
   436
            else opt_color
wenzelm@65101
   437
          case (_, opt_color) => opt_color
wenzelm@65101
   438
        })
wenzelm@65101
   439
    } yield Text.Info(r, color)
wenzelm@65101
   440
  }
wenzelm@65101
   441
wenzelm@65101
   442
wenzelm@65101
   443
  /* text foreground */
wenzelm@65101
   444
wenzelm@65101
   445
  def foreground(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
wenzelm@65101
   446
    snapshot.select(range, Rendering.foreground_elements, _ =>
wenzelm@65101
   447
      {
wenzelm@66074
   448
        case info => Some(Rendering.foreground(info.info.name))
wenzelm@65101
   449
      })
wenzelm@65101
   450
wenzelm@65101
   451
wenzelm@64767
   452
  /* caret focus */
wenzelm@64767
   453
wenzelm@64767
   454
  private def entity_focus(range: Text.Range,
wenzelm@64767
   455
    check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] =
wenzelm@64767
   456
  {
wenzelm@64767
   457
    val results =
wenzelm@64767
   458
      snapshot.cumulate[Set[Long]](range, Set.empty, Rendering.caret_focus_elements, _ =>
wenzelm@64767
   459
          {
wenzelm@64767
   460
            case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
wenzelm@64767
   461
              props match {
wenzelm@64767
   462
                case Markup.Entity.Def(i) if check(true, i) => Some(serials + i)
wenzelm@64767
   463
                case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
wenzelm@64767
   464
                case _ => None
wenzelm@64767
   465
              }
wenzelm@64767
   466
            case _ => None
wenzelm@64767
   467
          })
wenzelm@64767
   468
    (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
wenzelm@64767
   469
  }
wenzelm@64767
   470
wenzelm@64767
   471
  def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
wenzelm@64767
   472
  {
wenzelm@64767
   473
    val focus_defs = entity_focus(caret_range)
wenzelm@64767
   474
    if (focus_defs.nonEmpty) focus_defs
wenzelm@64767
   475
    else {
wenzelm@64767
   476
      val visible_defs = entity_focus(visible_range)
wenzelm@64767
   477
      entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i))
wenzelm@64767
   478
    }
wenzelm@64767
   479
  }
wenzelm@64767
   480
wenzelm@64767
   481
  def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
wenzelm@64767
   482
  {
wenzelm@64767
   483
    val focus = caret_focus(caret_range, visible_range)
wenzelm@64767
   484
    if (focus.nonEmpty) {
wenzelm@64767
   485
      val results =
wenzelm@64767
   486
        snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ =>
wenzelm@64767
   487
          {
wenzelm@64767
   488
            case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
wenzelm@64767
   489
              props match {
wenzelm@64767
   490
                case Markup.Entity.Def(i) if focus(i) => Some(true)
wenzelm@64767
   491
                case Markup.Entity.Ref(i) if focus(i) => Some(true)
wenzelm@64767
   492
                case _ => None
wenzelm@64767
   493
              }
wenzelm@64767
   494
          })
wenzelm@64767
   495
      for (info <- results if info.info) yield info.range
wenzelm@64767
   496
    }
wenzelm@64767
   497
    else Nil
wenzelm@64767
   498
  }
wenzelm@65121
   499
wenzelm@65121
   500
wenzelm@65121
   501
  /* message underline color */
wenzelm@65121
   502
wenzelm@65129
   503
  def message_underline_color(elements: Markup.Elements, range: Text.Range)
wenzelm@65129
   504
    : List[Text.Info[Rendering.Color.Value]] =
wenzelm@65121
   505
  {
wenzelm@65121
   506
    val results =
wenzelm@65121
   507
      snapshot.cumulate[Int](range, 0, elements, _ =>
wenzelm@65121
   508
        {
wenzelm@65121
   509
          case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
wenzelm@65121
   510
        })
wenzelm@65121
   511
    for {
wenzelm@65121
   512
      Text.Info(r, pri) <- results
wenzelm@65121
   513
      color <- Rendering.message_underline_color.get(pri)
wenzelm@65121
   514
    } yield Text.Info(r, color)
wenzelm@65121
   515
  }
wenzelm@65149
   516
wenzelm@65149
   517
wenzelm@65149
   518
  /* tooltips */
wenzelm@65149
   519
wenzelm@65149
   520
  def timing_threshold: Double
wenzelm@65149
   521
wenzelm@65149
   522
  private sealed case class Tooltip_Info(
wenzelm@65149
   523
    range: Text.Range,
wenzelm@65149
   524
    timing: Timing = Timing.zero,
wenzelm@65149
   525
    messages: List[Command.Results.Entry] = Nil,
wenzelm@65149
   526
    rev_infos: List[(Boolean, XML.Tree)] = Nil)
wenzelm@65149
   527
  {
wenzelm@65149
   528
    def + (t: Timing): Tooltip_Info = copy(timing = timing + t)
wenzelm@65149
   529
    def + (r0: Text.Range, serial: Long, tree: XML.Tree): Tooltip_Info =
wenzelm@65149
   530
    {
wenzelm@65149
   531
      val r = snapshot.convert(r0)
wenzelm@65149
   532
      if (range == r) copy(messages = (serial -> tree) :: messages)
wenzelm@65149
   533
      else copy(range = r, messages = List(serial -> tree))
wenzelm@65149
   534
    }
wenzelm@65149
   535
    def + (r0: Text.Range, important: Boolean, tree: XML.Tree): Tooltip_Info =
wenzelm@65149
   536
    {
wenzelm@65149
   537
      val r = snapshot.convert(r0)
wenzelm@65149
   538
      if (range == r) copy(rev_infos = (important -> tree) :: rev_infos)
wenzelm@65149
   539
      else copy (range = r, rev_infos = List(important -> tree))
wenzelm@65149
   540
    }
wenzelm@67933
   541
wenzelm@67933
   542
    def timing_info(tree: XML.Tree): Option[XML.Tree] =
wenzelm@67933
   543
      tree match {
wenzelm@67933
   544
        case XML.Elem(Markup(Markup.TIMING, _), _) =>
wenzelm@67933
   545
          if (timing.elapsed.seconds >= timing_threshold) Some(XML.Text(timing.message)) else None
wenzelm@67933
   546
        case _ => Some(tree)
wenzelm@67933
   547
      }
wenzelm@65149
   548
    def infos(important: Boolean): List[XML.Tree] =
wenzelm@67933
   549
      for {
wenzelm@67933
   550
        (is_important, tree) <- rev_infos.reverse if is_important == important
wenzelm@67933
   551
        tree1 <- timing_info(tree)
wenzelm@67933
   552
      } yield tree1
wenzelm@65149
   553
  }
wenzelm@65149
   554
wenzelm@65488
   555
  def perhaps_append_file(node_name: Document.Node.Name, name: String): String =
wenzelm@65488
   556
    if (Path.is_valid(name)) session.resources.append(node_name, Path.explode(name)) else name
wenzelm@65487
   557
wenzelm@65149
   558
  def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
wenzelm@65149
   559
  {
wenzelm@65149
   560
    val results =
wenzelm@67824
   561
      snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, command_states =>
wenzelm@65149
   562
        {
wenzelm@65149
   563
          case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info + t)
wenzelm@65149
   564
wenzelm@67824
   565
          case (info, Text.Info(r0, msg @ XML.Elem(Markup(Markup.BAD, Markup.Serial(i)), body)))
wenzelm@67824
   566
          if body.nonEmpty => Some(info + (r0, i, msg))
wenzelm@67824
   567
wenzelm@67824
   568
          case (info, Text.Info(r0, XML.Elem(Markup(name, props), _)))
wenzelm@67824
   569
          if Rendering.tooltip_message_elements(name) =>
wenzelm@67824
   570
            for ((i, tree) <- Command.State.get_result_proper(command_states, props))
wenzelm@67824
   571
            yield (info + (r0, i, tree))
wenzelm@65149
   572
wenzelm@65149
   573
          case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _)))
wenzelm@65149
   574
          if kind != "" && kind != Markup.ML_DEF =>
wenzelm@65149
   575
            val kind1 = Word.implode(Word.explode('_', kind))
wenzelm@65149
   576
            val txt1 =
wenzelm@65149
   577
              if (name == "") kind1
wenzelm@65149
   578
              else if (kind1 == "") quote(name)
wenzelm@65149
   579
              else kind1 + " " + quote(name)
wenzelm@67933
   580
            val info1 = info + (r0, true, XML.Text(txt1))
wenzelm@67933
   581
            Some(if (kind == Markup.COMMAND) info1 + (r0, true, XML.elem(Markup.TIMING)) else info1)
wenzelm@65149
   582
wenzelm@65149
   583
          case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
wenzelm@65488
   584
            val file = perhaps_append_file(snapshot.node_name, name)
wenzelm@65149
   585
            val text =
wenzelm@65149
   586
              if (name == file) "file " + quote(file)
wenzelm@65149
   587
              else "path " + quote(name) + "\nfile " + quote(file)
wenzelm@65149
   588
            Some(info + (r0, true, XML.Text(text)))
wenzelm@65149
   589
wenzelm@65149
   590
          case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) =>
wenzelm@65149
   591
            val text = "doc " + quote(name)
wenzelm@65149
   592
            Some(info + (r0, true, XML.Text(text)))
wenzelm@65149
   593
wenzelm@65149
   594
          case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) =>
wenzelm@65149
   595
            Some(info + (r0, true, XML.Text("URL " + quote(name))))
wenzelm@65149
   596
wenzelm@65149
   597
          case (info, Text.Info(r0, XML.Elem(Markup(name, _), body)))
wenzelm@65149
   598
          if name == Markup.SORTING || name == Markup.TYPING =>
wenzelm@65149
   599
            Some(info + (r0, true, Pretty.block(XML.Text("::") :: Pretty.brk(1) :: body)))
wenzelm@65149
   600
wenzelm@65149
   601
          case (info, Text.Info(r0, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
wenzelm@65149
   602
            Some(info + (r0, true, Pretty.block(0, body)))
wenzelm@65149
   603
wenzelm@65149
   604
          case (info, Text.Info(r0, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
wenzelm@65149
   605
            Some(info + (r0, false, Pretty.block(XML.Text("ML:") :: Pretty.brk(1) :: body)))
wenzelm@65149
   606
wenzelm@65149
   607
          case (info, Text.Info(r0, Protocol.ML_Breakpoint(breakpoint))) =>
wenzelm@65222
   608
              val text =
wenzelm@65222
   609
                if (session.debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
wenzelm@65222
   610
                else "breakpoint (disabled)"
wenzelm@65222
   611
              Some(info + (r0, true, XML.Text(text)))
wenzelm@65149
   612
          case (info, Text.Info(r0, XML.Elem(Markup.Language(language, _, _, _), _))) =>
wenzelm@65149
   613
            val lang = Word.implode(Word.explode('_', language))
wenzelm@65149
   614
            Some(info + (r0, true, XML.Text("language: " + lang)))
wenzelm@65149
   615
wenzelm@65149
   616
          case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) =>
wenzelm@65149
   617
            val descr = if (kind == "") "expression" else "expression: " + kind
wenzelm@65149
   618
            Some(info + (r0, true, XML.Text(descr)))
wenzelm@65149
   619
wenzelm@65149
   620
          case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
wenzelm@65149
   621
            Some(info + (r0, true, XML.Text("Markdown: paragraph")))
wenzelm@67323
   622
          case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), _))) =>
wenzelm@67323
   623
            Some(info + (r0, true, XML.Text("Markdown: item")))
wenzelm@65149
   624
          case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) =>
wenzelm@65149
   625
            Some(info + (r0, true, XML.Text("Markdown: " + kind)))
wenzelm@65149
   626
wenzelm@65149
   627
          case (info, Text.Info(r0, XML.Elem(Markup(name, _), _))) =>
wenzelm@65149
   628
            Rendering.tooltip_descriptions.get(name).map(desc => info + (r0, true, XML.Text(desc)))
wenzelm@65149
   629
        }).map(_.info)
wenzelm@65149
   630
wenzelm@65149
   631
    if (results.isEmpty) None
wenzelm@65149
   632
    else {
wenzelm@65149
   633
      val r = Text.Range(results.head.range.start, results.last.range.stop)
wenzelm@65149
   634
      val all_tips =
wenzelm@65149
   635
        Command.Results.make(results.flatMap(_.messages)).iterator.map(_._2).toList :::
wenzelm@65149
   636
        results.flatMap(res => res.infos(true)) :::
wenzelm@65149
   637
        results.flatMap(res => res.infos(false)).lastOption.toList
wenzelm@65149
   638
      if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips))
wenzelm@65149
   639
    }
wenzelm@65149
   640
  }
wenzelm@65911
   641
wenzelm@65911
   642
wenzelm@65911
   643
  /* command status overview */
wenzelm@65911
   644
wenzelm@65911
   645
  def overview_color(range: Text.Range): Option[Rendering.Color.Value] =
wenzelm@65911
   646
  {
wenzelm@65911
   647
    if (snapshot.is_outdated) None
wenzelm@65911
   648
    else {
wenzelm@65911
   649
      val results =
wenzelm@68758
   650
        snapshot.cumulate[List[Markup]](range, Nil, Document_Status.Command_Status.liberal_elements,
wenzelm@68758
   651
          _ =>
wenzelm@68758
   652
            {
wenzelm@68758
   653
              case (status, Text.Info(_, elem)) => Some(elem.markup :: status)
wenzelm@68758
   654
            }, status = true)
wenzelm@65911
   655
      if (results.isEmpty) None
wenzelm@65911
   656
      else {
wenzelm@68758
   657
        val status = Document_Status.Command_Status.make(results.iterator.flatMap(_.info))
wenzelm@65911
   658
wenzelm@65911
   659
        if (status.is_running) Some(Rendering.Color.running)
wenzelm@65911
   660
        else if (status.is_failed) Some(Rendering.Color.error)
wenzelm@65911
   661
        else if (status.is_warned) Some(Rendering.Color.warning)
wenzelm@65911
   662
        else if (status.is_unprocessed) Some(Rendering.Color.unprocessed)
wenzelm@65911
   663
        else None
wenzelm@65911
   664
      }
wenzelm@65911
   665
    }
wenzelm@65911
   666
  }
wenzelm@67132
   667
wenzelm@67132
   668
wenzelm@67132
   669
  /* antiquoted text */
wenzelm@67132
   670
wenzelm@67132
   671
  def antiquoted(range: Text.Range): Option[Text.Range] =
wenzelm@67132
   672
    snapshot.cumulate[Option[Text.Range]](range, None, Rendering.antiquoted_elements, _ =>
wenzelm@67132
   673
      {
wenzelm@67132
   674
        case (res, info) => if (res.isEmpty) Some(Some(info.range)) else None
wenzelm@67132
   675
      }).headOption.flatMap(_.info)
wenzelm@64622
   676
}