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