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