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