src/Pure/PIDE/rendering.scala
author wenzelm
Sun, 13 Dec 2020 22:30:30 +0100
changeset 72903 8f586c241071
parent 72902 3c09adb4b042
child 72904 b44b2d2380f0
permissions -rw-r--r--
tuned signature;
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
72900
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   173
  /* entity focus */
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   174
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   175
  object Focus
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   176
  {
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   177
    def apply(ids: Set[Long]): Focus = new Focus(ids)
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   178
    val empty: Focus = apply(Set.empty)
72901
16fd39c9e31f tuned signature;
wenzelm
parents: 72900
diff changeset
   179
    def merge(args: TraversableOnce[Focus]): Focus = (empty /: args)(_ ++ _)
72900
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   180
  }
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   181
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   182
  sealed class Focus private[Rendering](protected val rep: Set[Long])
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   183
  {
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   184
    def defined: Boolean = rep.nonEmpty
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   185
    def apply(id: Long): Boolean = rep.contains(id)
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   186
    def + (id: Long): Focus = if (rep.contains(id)) this else new Focus(rep + id)
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   187
    def ++ (other: Focus): Focus =
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   188
      if (this eq other) this
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   189
      else if (rep.isEmpty) other
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   190
      else (this /: other.rep.iterator)(_ + _)
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   191
    override def toString: String = rep.mkString("Focus(", ",", ")")
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   192
  }
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   193
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   194
65149
wenzelm
parents: 65145
diff changeset
   195
  /* markup elements */
wenzelm
parents: 65145
diff changeset
   196
72692
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 71601
diff changeset
   197
  val position_elements =
22aeec526ffd support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents: 71601
diff changeset
   198
    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
   199
66053
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   200
  val semantic_completion_elements =
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   201
    Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   202
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   203
  val language_context_elements =
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   204
    Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   205
      Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   206
      Markup.ML_STRING, Markup.ML_COMMENT)
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   207
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   208
  val language_elements = Markup.Elements(Markup.LANGUAGE)
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   209
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   210
  val citation_elements = Markup.Elements(Markup.CITATION)
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   211
65149
wenzelm
parents: 65145
diff changeset
   212
  val active_elements =
69650
c95edf19133b clarified message;
wenzelm
parents: 69648
diff changeset
   213
    Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.THEORY_EXPORTS,
65149
wenzelm
parents: 65145
diff changeset
   214
      Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
wenzelm
parents: 65145
diff changeset
   215
wenzelm
parents: 65145
diff changeset
   216
  val background_elements =
68758
a110e7e24e55 clarified modules;
wenzelm
parents: 67933
diff changeset
   217
    Document_Status.Command_Status.proper_elements + Markup.WRITELN_MESSAGE +
65149
wenzelm
parents: 65145
diff changeset
   218
      Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
wenzelm
parents: 65145
diff changeset
   219
      Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
wenzelm
parents: 65145
diff changeset
   220
      Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
wenzelm
parents: 65145
diff changeset
   221
      Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
67322
734a4e44b159 clarified terminology of "markdown_bullet";
wenzelm
parents: 67132
diff changeset
   222
      Markup.Markdown_Bullet.name ++ active_elements
65149
wenzelm
parents: 65145
diff changeset
   223
66074
wenzelm
parents: 66055
diff changeset
   224
  val foreground_elements = Markup.Elements(foreground.keySet)
wenzelm
parents: 66055
diff changeset
   225
wenzelm
parents: 66055
diff changeset
   226
  val text_color_elements = Markup.Elements(text_color.keySet)
65149
wenzelm
parents: 65145
diff changeset
   227
65129
06a7c2d316cf more general tooltips, with uniform info range handling;
wenzelm
parents: 65126
diff changeset
   228
  val tooltip_elements =
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   229
    Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   230
      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
69650
c95edf19133b clarified message;
wenzelm
parents: 69648
diff changeset
   231
      Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL,
69648
97ddaec3e2ae support hyperlink to theory exports;
wenzelm
parents: 69366
diff changeset
   232
      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
   233
      Markup.Elements(tooltip_descriptions.keySet)
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   234
65129
06a7c2d316cf more general tooltips, with uniform info range handling;
wenzelm
parents: 65126
diff changeset
   235
  val tooltip_message_elements =
06a7c2d316cf more general tooltips, with uniform info range handling;
wenzelm
parents: 65126
diff changeset
   236
    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
   237
      Markup.BAD)
06a7c2d316cf more general tooltips, with uniform info range handling;
wenzelm
parents: 65126
diff changeset
   238
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72856
diff changeset
   239
  val message_elements = Markup.Elements(message_pri.keySet)
71499
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 70135
diff changeset
   240
  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
   241
  val error_elements = Markup.Elements(Markup.ERROR)
71499
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 70135
diff changeset
   242
72901
16fd39c9e31f tuned signature;
wenzelm
parents: 72900
diff changeset
   243
  val entity_elements = Markup.Elements(Markup.ENTITY)
67132
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   244
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   245
  val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED)
67336
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67323
diff changeset
   246
69900
18a61caf5e68 support for document meta data in PIDE and RDF;
wenzelm
parents: 69899
diff changeset
   247
  val meta_data_elements =
18a61caf5e68 support for document meta data in PIDE and RDF;
wenzelm
parents: 69899
diff changeset
   248
    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
   249
      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
   250
70135
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 69970
diff changeset
   251
  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
   252
    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
   253
67336
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67323
diff changeset
   254
  val markdown_elements =
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67323
diff changeset
   255
    Markup.Elements(Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name,
3ee6da378183 HTML output for Markdown elements;
wenzelm
parents: 67323
diff changeset
   256
      Markup.Markdown_Bullet.name)
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   257
}
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   258
72856
3a27e6f83ce1 clarified signature;
wenzelm
parents: 72842
diff changeset
   259
class Rendering(
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   260
  val snapshot: Document.Snapshot,
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   261
  val options: Options,
65213
51c0f094dc02 proper local debugger state, depending on session;
wenzelm
parents: 65190
diff changeset
   262
  val session: Session)
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   263
{
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   264
  override def toString: String = "Rendering(" + snapshot.toString + ")"
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   265
72856
3a27e6f83ce1 clarified signature;
wenzelm
parents: 72842
diff changeset
   266
  def get_text(range: Text.Range): Option[String] = None
66114
c137a9f038a6 clarified signature;
wenzelm
parents: 66074
diff changeset
   267
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   268
66117
e6f808d1307c tuned signature;
wenzelm
parents: 66114
diff changeset
   269
  /* caret */
e6f808d1307c tuned signature;
wenzelm
parents: 66114
diff changeset
   270
e6f808d1307c tuned signature;
wenzelm
parents: 66114
diff changeset
   271
  def before_caret_range(caret: Text.Offset): Text.Range =
e6f808d1307c tuned signature;
wenzelm
parents: 66114
diff changeset
   272
  {
e6f808d1307c tuned signature;
wenzelm
parents: 66114
diff changeset
   273
    val former_caret = snapshot.revert(caret)
e6f808d1307c tuned signature;
wenzelm
parents: 66114
diff changeset
   274
    snapshot.convert(Text.Range(former_caret - 1, former_caret))
e6f808d1307c tuned signature;
wenzelm
parents: 66114
diff changeset
   275
  }
e6f808d1307c tuned signature;
wenzelm
parents: 66114
diff changeset
   276
e6f808d1307c tuned signature;
wenzelm
parents: 66114
diff changeset
   277
64877
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64767
diff changeset
   278
  /* completion */
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64767
diff changeset
   279
66054
fb0eea226a4d more uniform syntax_completion + semantic_completion;
wenzelm
parents: 66053
diff changeset
   280
  def semantic_completion(completed_range: Option[Text.Range], caret_range: Text.Range)
64877
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64767
diff changeset
   281
      : Option[Text.Info[Completion.Semantic]] =
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64767
diff changeset
   282
    if (snapshot.is_outdated) None
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64767
diff changeset
   283
    else {
66054
fb0eea226a4d more uniform syntax_completion + semantic_completion;
wenzelm
parents: 66053
diff changeset
   284
      snapshot.select(caret_range, Rendering.semantic_completion_elements, _ =>
64877
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64767
diff changeset
   285
        {
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64767
diff changeset
   286
          case Completion.Semantic.Info(info) =>
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64767
diff changeset
   287
            completed_range match {
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64767
diff changeset
   288
              case Some(range0) if range0.contains(info.range) && range0 != info.range => None
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64767
diff changeset
   289
              case _ => Some(info)
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64767
diff changeset
   290
            }
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64767
diff changeset
   291
          case _ => None
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64767
diff changeset
   292
        }).headOption.map(_.info)
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64767
diff changeset
   293
    }
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64767
diff changeset
   294
66054
fb0eea226a4d more uniform syntax_completion + semantic_completion;
wenzelm
parents: 66053
diff changeset
   295
  def semantic_completion_result(
fb0eea226a4d more uniform syntax_completion + semantic_completion;
wenzelm
parents: 66053
diff changeset
   296
    history: Completion.History,
66055
wenzelm
parents: 66054
diff changeset
   297
    unicode: Boolean,
66054
fb0eea226a4d more uniform syntax_completion + semantic_completion;
wenzelm
parents: 66053
diff changeset
   298
    completed_range: Option[Text.Range],
66114
c137a9f038a6 clarified signature;
wenzelm
parents: 66074
diff changeset
   299
    caret_range: Text.Range): (Boolean, Option[Completion.Result]) =
66054
fb0eea226a4d more uniform syntax_completion + semantic_completion;
wenzelm
parents: 66053
diff changeset
   300
  {
fb0eea226a4d more uniform syntax_completion + semantic_completion;
wenzelm
parents: 66053
diff changeset
   301
    semantic_completion(completed_range, caret_range) match {
fb0eea226a4d more uniform syntax_completion + semantic_completion;
wenzelm
parents: 66053
diff changeset
   302
      case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
fb0eea226a4d more uniform syntax_completion + semantic_completion;
wenzelm
parents: 66053
diff changeset
   303
      case Some(Text.Info(range, names: Completion.Names)) =>
72856
3a27e6f83ce1 clarified signature;
wenzelm
parents: 72842
diff changeset
   304
        get_text(range) match {
66055
wenzelm
parents: 66054
diff changeset
   305
          case Some(original) => (false, names.complete(range, history, unicode, original))
66054
fb0eea226a4d more uniform syntax_completion + semantic_completion;
wenzelm
parents: 66053
diff changeset
   306
          case None => (false, None)
fb0eea226a4d more uniform syntax_completion + semantic_completion;
wenzelm
parents: 66053
diff changeset
   307
        }
fb0eea226a4d more uniform syntax_completion + semantic_completion;
wenzelm
parents: 66053
diff changeset
   308
      case None => (false, None)
fb0eea226a4d more uniform syntax_completion + semantic_completion;
wenzelm
parents: 66053
diff changeset
   309
    }
fb0eea226a4d more uniform syntax_completion + semantic_completion;
wenzelm
parents: 66053
diff changeset
   310
  }
fb0eea226a4d more uniform syntax_completion + semantic_completion;
wenzelm
parents: 66053
diff changeset
   311
66053
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   312
  def language_context(range: Text.Range): Option[Completion.Language_Context] =
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   313
    snapshot.select(range, Rendering.language_context_elements, _ =>
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   314
      {
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   315
        case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) =>
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   316
          if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes))
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   317
          else None
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   318
        case Text.Info(_, elem)
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   319
        if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   320
          Some(Completion.Language_Context.ML_inner)
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   321
        case Text.Info(_, _) =>
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   322
          Some(Completion.Language_Context.inner)
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   323
      }).headOption.map(_.info)
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   324
72729
83411077c37b clarified signature;
wenzelm
parents: 72727
diff changeset
   325
  def citations(range: Text.Range): List[Text.Info[String]] =
66158
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   326
    snapshot.select(range, Rendering.citation_elements, _ =>
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   327
      {
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   328
        case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) =>
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   329
          Some(Text.Info(snapshot.convert(info_range), name))
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   330
        case _ => None
72729
83411077c37b clarified signature;
wenzelm
parents: 72727
diff changeset
   331
      }).map(_.info)
66158
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   332
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   333
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   334
  /* file-system path completion */
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   335
72842
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72729
diff changeset
   336
  def language_path(range: Text.Range): Option[Text.Info[Boolean]] =
66053
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   337
    snapshot.select(range, Rendering.language_elements, _ =>
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   338
      {
72842
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72729
diff changeset
   339
        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
   340
          Some((delimited, snapshot.convert(info_range)))
66053
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   341
        case _ => None
72842
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72729
diff changeset
   342
      }).headOption.map({ case Text.Info(_, (delimited, range)) => Text.Info(range, delimited) })
66053
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   343
66158
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   344
  def path_completion(caret: Text.Offset): Option[Completion.Result] =
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   345
  {
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   346
    def complete(text: String): List[(String, List[String])] =
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   347
    {
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   348
      try {
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   349
        val path = Path.explode(text)
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   350
        val (dir, base_name) =
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   351
          if (text == "" || text.endsWith("/")) (path, "")
69366
b6dacf6eabe3 clarified signature;
wenzelm
parents: 69320
diff changeset
   352
          else (path.dir, path.file_name)
66158
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   353
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   354
        val directory = new JFile(session.resources.append(snapshot.node_name, dir))
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   355
        val files = directory.listFiles
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   356
        if (files == null) Nil
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   357
        else {
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   358
          val ignore =
66923
wenzelm
parents: 66158
diff changeset
   359
            space_explode(':', options.string("completion_path_ignore")).
66158
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   360
              map(s => FileSystems.getDefault.getPathMatcher("glob:" + s))
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   361
          (for {
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   362
            file <- files.iterator
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   363
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   364
            name = file.getName
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   365
            if name.startsWith(base_name)
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   366
            path_name = new JFile(name).toPath
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   367
            if !ignore.exists(matcher => matcher.matches(path_name))
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   368
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   369
            text1 = (dir + Path.basic(name)).implode_short
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   370
            if text != text1
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   371
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   372
            is_dir = new JFile(directory, name).isDirectory
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   373
            replacement = text1 + (if (is_dir) "/" else "")
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   374
            descr = List(text1, if (is_dir) "(directory)" else "(file)")
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   375
          } yield (replacement, descr)).take(options.int("completion_limit")).toList
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   376
        }
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   377
      }
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   378
      catch { case ERROR(_) => Nil }
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   379
    }
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   380
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   381
    def is_wrapped(s: String): Boolean =
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   382
      s.startsWith("\"") && s.endsWith("\"") ||
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   383
      s.startsWith(Symbol.open_decoded) && s.endsWith(Symbol.close_decoded)
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   384
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   385
    for {
72842
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72729
diff changeset
   386
      Text.Info(r1, delimited) <- language_path(before_caret_range(caret))
72856
3a27e6f83ce1 clarified signature;
wenzelm
parents: 72842
diff changeset
   387
      s1 <- get_text(r1)
72842
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72729
diff changeset
   388
      (r2, s2) <-
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72729
diff changeset
   389
        if (is_wrapped(s1)) {
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72729
diff changeset
   390
          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
   391
        }
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72729
diff changeset
   392
        else if (delimited) Some((r1, s1))
6aae62f55c2b clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents: 72729
diff changeset
   393
        else None
66158
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   394
      if Path.is_valid(s2)
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   395
      paths = complete(s2)
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   396
      if paths.nonEmpty
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   397
      items = paths.map(p => Completion.Item(r2, s2, "", p._2, p._1, 0, false))
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   398
    } yield Completion.Result(r2, s2, false, items)
ad83d4971dfe clarified modules;
wenzelm
parents: 66117
diff changeset
   399
  }
66053
cd8d0ad5ac19 clarified modules;
wenzelm
parents: 65913
diff changeset
   400
64877
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64767
diff changeset
   401
65139
0a2c0712e432 clarified modules: spell-checker in Pure;
wenzelm
parents: 65133
diff changeset
   402
  /* spell checker */
0a2c0712e432 clarified modules: spell-checker in Pure;
wenzelm
parents: 65133
diff changeset
   403
67395
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67336
diff changeset
   404
  private lazy val spell_checker_include =
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67336
diff changeset
   405
    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
   406
65139
0a2c0712e432 clarified modules: spell-checker in Pure;
wenzelm
parents: 65133
diff changeset
   407
  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
   408
    spell_checker_include ++
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67336
diff changeset
   409
      Markup.Elements(space_explode(',', options.string("spell_checker_exclude")): _*)
65139
0a2c0712e432 clarified modules: spell-checker in Pure;
wenzelm
parents: 65133
diff changeset
   410
67395
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67336
diff changeset
   411
  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
   412
  {
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67336
diff changeset
   413
    val result =
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67336
diff changeset
   414
      snapshot.select(range, spell_checker_elements, _ =>
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67336
diff changeset
   415
        {
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67336
diff changeset
   416
          case info =>
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67336
diff changeset
   417
            Some(
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67336
diff changeset
   418
              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
   419
                Some(snapshot.convert(info.range))
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67336
diff changeset
   420
              else None)
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67336
diff changeset
   421
        })
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67336
diff changeset
   422
    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
   423
      yield Text.Info(range, range1)
b39d596b77ce more accurate spell-checking for nested quotations / antiquotations, notably in formal comments;
wenzelm
parents: 67336
diff changeset
   424
  }
65139
0a2c0712e432 clarified modules: spell-checker in Pure;
wenzelm
parents: 65133
diff changeset
   425
0a2c0712e432 clarified modules: spell-checker in Pure;
wenzelm
parents: 65133
diff changeset
   426
  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
   427
    spell_checker(range).headOption.map(_.info)
65139
0a2c0712e432 clarified modules: spell-checker in Pure;
wenzelm
parents: 65133
diff changeset
   428
0a2c0712e432 clarified modules: spell-checker in Pure;
wenzelm
parents: 65133
diff changeset
   429
65101
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   430
  /* text background */
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   431
72900
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   432
  def background(elements: Markup.Elements, range: Text.Range, focus: Rendering.Focus)
65176
908d8be90533 suppress irrelevant markup for VSCode;
wenzelm
parents: 65150
diff changeset
   433
    : List[Text.Info[Rendering.Color.Value]] =
65101
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   434
  {
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   435
    for {
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   436
      Text.Info(r, result) <-
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   437
        snapshot.cumulate[(List[Markup], Option[Rendering.Color.Value])](
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   438
          range, (List(Markup.Empty), None), Rendering.background_elements,
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   439
          command_states =>
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   440
            {
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   441
              case (((markups, color), Text.Info(_, XML.Elem(markup, _))))
68758
a110e7e24e55 clarified modules;
wenzelm
parents: 67933
diff changeset
   442
              if markups.nonEmpty && Document_Status.Command_Status.proper_elements(markup.name) =>
65101
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   443
                Some((markup :: markups, color))
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   444
              case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   445
                Some((Nil, Some(Rendering.Color.bad)))
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   446
              case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   447
                Some((Nil, Some(Rendering.Color.intensify)))
72903
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   448
              case (_, Text.Info(_, XML.Elem(Markup.Entity.Id(i), _))) if focus(i) =>
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   449
                Some((Nil, Some(Rendering.Color.entity)))
67322
734a4e44b159 clarified terminology of "markdown_bullet";
wenzelm
parents: 67132
diff changeset
   450
              case (_, Text.Info(_, XML.Elem(Markup.Markdown_Bullet(depth), _))) =>
65101
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   451
                val color =
65150
fa299b4e50c3 clarified rendering;
wenzelm
parents: 65149
diff changeset
   452
                  depth % 4 match {
67322
734a4e44b159 clarified terminology of "markdown_bullet";
wenzelm
parents: 67132
diff changeset
   453
                    case 1 => Rendering.Color.markdown_bullet1
734a4e44b159 clarified terminology of "markdown_bullet";
wenzelm
parents: 67132
diff changeset
   454
                    case 2 => Rendering.Color.markdown_bullet2
734a4e44b159 clarified terminology of "markdown_bullet";
wenzelm
parents: 67132
diff changeset
   455
                    case 3 => Rendering.Color.markdown_bullet3
734a4e44b159 clarified terminology of "markdown_bullet";
wenzelm
parents: 67132
diff changeset
   456
                    case _ => Rendering.Color.markdown_bullet4
65101
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   457
                  }
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   458
                Some((Nil, Some(color)))
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   459
              case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   460
                command_states.collectFirst(
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   461
                  { case st if st.results.defined(serial) => st.results.get(serial).get }) match
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   462
                {
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   463
                  case Some(Protocol.Dialog_Result(res)) if res == result =>
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   464
                    Some((Nil, Some(Rendering.Color.active_result)))
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   465
                  case _ =>
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   466
                    Some((Nil, Some(Rendering.Color.active)))
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   467
                }
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   468
              case (_, Text.Info(_, elem)) =>
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   469
                if (Rendering.active_elements(elem.name))
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   470
                  Some((Nil, Some(Rendering.Color.active)))
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   471
                else None
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   472
            })
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   473
      color <-
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   474
        (result match {
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   475
          case (markups, opt_color) if markups.nonEmpty =>
68758
a110e7e24e55 clarified modules;
wenzelm
parents: 67933
diff changeset
   476
            val status = Document_Status.Command_Status.make(markups.iterator)
65101
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   477
            if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   478
            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
   479
            else if (status.is_canceled) Some(Rendering.Color.canceled)
65101
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   480
            else opt_color
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   481
          case (_, opt_color) => opt_color
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   482
        })
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   483
    } yield Text.Info(r, color)
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   484
  }
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   485
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   486
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   487
  /* text foreground */
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   488
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   489
  def foreground(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   490
    snapshot.select(range, Rendering.foreground_elements, _ =>
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   491
      {
66074
wenzelm
parents: 66055
diff changeset
   492
        case info => Some(Rendering.foreground(info.info.name))
65101
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   493
      })
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   494
4263b2a201b3 symbolic Rendering.Color;
wenzelm
parents: 64877
diff changeset
   495
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   496
  /* caret focus */
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   497
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   498
  private def entity_focus(range: Text.Range,
72900
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   499
      check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def)
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   500
    : Rendering.Focus =
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   501
  {
72901
16fd39c9e31f tuned signature;
wenzelm
parents: 72900
diff changeset
   502
    Rendering.Focus.merge(
16fd39c9e31f tuned signature;
wenzelm
parents: 72900
diff changeset
   503
      snapshot.cumulate[Rendering.Focus](range, Rendering.Focus.empty, Rendering.entity_elements,
16fd39c9e31f tuned signature;
wenzelm
parents: 72900
diff changeset
   504
        _ =>
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   505
          {
72900
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   506
            case (focus, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   507
              props match {
72902
3c09adb4b042 tuned signature;
wenzelm
parents: 72901
diff changeset
   508
                case Markup.Def(i) if check(true, i) => Some(focus + i)
3c09adb4b042 tuned signature;
wenzelm
parents: 72901
diff changeset
   509
                case Markup.Ref(i) if check(false, i) => Some(focus + i)
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   510
                case _ => None
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   511
              }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   512
            case _ => None
72901
16fd39c9e31f tuned signature;
wenzelm
parents: 72900
diff changeset
   513
          }).iterator.map(_.info))
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   514
  }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   515
72900
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   516
  def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Rendering.Focus =
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   517
  {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   518
    val focus_defs = entity_focus(caret_range)
72900
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   519
    if (focus_defs.defined) focus_defs
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   520
    else {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   521
      val visible_defs = entity_focus(visible_range)
72900
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   522
      entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs(i))
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   523
    }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   524
  }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   525
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   526
  def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   527
  {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   528
    val focus = caret_focus(caret_range, visible_range)
72900
c9813630cca4 clarified signature: more explicit types;
wenzelm
parents: 72872
diff changeset
   529
    if (focus.defined) {
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   530
      val results =
72901
16fd39c9e31f tuned signature;
wenzelm
parents: 72900
diff changeset
   531
        snapshot.cumulate[Boolean](visible_range, false, Rendering.entity_elements, _ =>
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   532
          {
72903
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   533
            case (_, Text.Info(_, XML.Elem(Markup.Entity.Id(i), _))) if focus(i) => Some(true)
8f586c241071 tuned signature;
wenzelm
parents: 72902
diff changeset
   534
            case _ => None
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   535
          })
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   536
      for (info <- results if info.info) yield info.range
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   537
    }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   538
    else Nil
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   539
  }
65121
12c6774a8f65 more generic rendering;
wenzelm
parents: 65107
diff changeset
   540
12c6774a8f65 more generic rendering;
wenzelm
parents: 65107
diff changeset
   541
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72856
diff changeset
   542
  /* messages */
65121
12c6774a8f65 more generic rendering;
wenzelm
parents: 65107
diff changeset
   543
65129
06a7c2d316cf more general tooltips, with uniform info range handling;
wenzelm
parents: 65126
diff changeset
   544
  def message_underline_color(elements: Markup.Elements, range: Text.Range)
06a7c2d316cf more general tooltips, with uniform info range handling;
wenzelm
parents: 65126
diff changeset
   545
    : List[Text.Info[Rendering.Color.Value]] =
65121
12c6774a8f65 more generic rendering;
wenzelm
parents: 65107
diff changeset
   546
  {
12c6774a8f65 more generic rendering;
wenzelm
parents: 65107
diff changeset
   547
    val results =
12c6774a8f65 more generic rendering;
wenzelm
parents: 65107
diff changeset
   548
      snapshot.cumulate[Int](range, 0, elements, _ =>
12c6774a8f65 more generic rendering;
wenzelm
parents: 65107
diff changeset
   549
        {
12c6774a8f65 more generic rendering;
wenzelm
parents: 65107
diff changeset
   550
          case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
12c6774a8f65 more generic rendering;
wenzelm
parents: 65107
diff changeset
   551
        })
12c6774a8f65 more generic rendering;
wenzelm
parents: 65107
diff changeset
   552
    for {
12c6774a8f65 more generic rendering;
wenzelm
parents: 65107
diff changeset
   553
      Text.Info(r, pri) <- results
12c6774a8f65 more generic rendering;
wenzelm
parents: 65107
diff changeset
   554
      color <- Rendering.message_underline_color.get(pri)
12c6774a8f65 more generic rendering;
wenzelm
parents: 65107
diff changeset
   555
    } yield Text.Info(r, color)
12c6774a8f65 more generic rendering;
wenzelm
parents: 65107
diff changeset
   556
  }
65149
wenzelm
parents: 65145
diff changeset
   557
72869
015a61936c13 clarified signature: more specific types;
wenzelm
parents: 72858
diff changeset
   558
  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
   559
  {
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72856
diff changeset
   560
    val results =
72872
530534f2f0fd clarified types;
wenzelm
parents: 72869
diff changeset
   561
      snapshot.cumulate[Vector[Command.Results.Entry]](
530534f2f0fd clarified types;
wenzelm
parents: 72869
diff changeset
   562
        range, Vector.empty, Rendering.message_elements, command_states =>
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72856
diff changeset
   563
          {
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72856
diff changeset
   564
            case (res, Text.Info(_, elem)) =>
72872
530534f2f0fd clarified types;
wenzelm
parents: 72869
diff changeset
   565
              Command.State.get_result_proper(command_states, elem.markup.properties)
530534f2f0fd clarified types;
wenzelm
parents: 72869
diff changeset
   566
                .map(res :+ _)
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72856
diff changeset
   567
            case _ => None
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72856
diff changeset
   568
          })
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72856
diff changeset
   569
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72856
diff changeset
   570
    var seen_serials = Set.empty[Long]
72872
530534f2f0fd clarified types;
wenzelm
parents: 72869
diff changeset
   571
    def seen(i: Long): Boolean =
530534f2f0fd clarified types;
wenzelm
parents: 72869
diff changeset
   572
    {
530534f2f0fd clarified types;
wenzelm
parents: 72869
diff changeset
   573
      val b = seen_serials(i)
530534f2f0fd clarified types;
wenzelm
parents: 72869
diff changeset
   574
      seen_serials += i
530534f2f0fd clarified types;
wenzelm
parents: 72869
diff changeset
   575
      b
530534f2f0fd clarified types;
wenzelm
parents: 72869
diff changeset
   576
    }
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72856
diff changeset
   577
    for {
72872
530534f2f0fd clarified types;
wenzelm
parents: 72869
diff changeset
   578
      Text.Info(range, entries) <- results
530534f2f0fd clarified types;
wenzelm
parents: 72869
diff changeset
   579
      (i, elem) <- entries if !seen(i)
72869
015a61936c13 clarified signature: more specific types;
wenzelm
parents: 72858
diff changeset
   580
    } yield Text.Info(range, elem)
72858
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72856
diff changeset
   581
  }
cb0c407fbc6e added "isabelle log": print messages from build database;
wenzelm
parents: 72856
diff changeset
   582
65149
wenzelm
parents: 65145
diff changeset
   583
wenzelm
parents: 65145
diff changeset
   584
  /* tooltips */
wenzelm
parents: 65145
diff changeset
   585
69899
27cf4287de43 tuned signature;
wenzelm
parents: 69650
diff changeset
   586
  def timing_threshold: Double = 0.0
65149
wenzelm
parents: 65145
diff changeset
   587
wenzelm
parents: 65145
diff changeset
   588
  private sealed case class Tooltip_Info(
wenzelm
parents: 65145
diff changeset
   589
    range: Text.Range,
wenzelm
parents: 65145
diff changeset
   590
    timing: Timing = Timing.zero,
72869
015a61936c13 clarified signature: more specific types;
wenzelm
parents: 72858
diff changeset
   591
    messages: List[(Long, XML.Tree)] = Nil,
65149
wenzelm
parents: 65145
diff changeset
   592
    rev_infos: List[(Boolean, XML.Tree)] = Nil)
wenzelm
parents: 65145
diff changeset
   593
  {
wenzelm
parents: 65145
diff changeset
   594
    def + (t: Timing): Tooltip_Info = copy(timing = timing + t)
wenzelm
parents: 65145
diff changeset
   595
    def + (r0: Text.Range, serial: Long, tree: XML.Tree): Tooltip_Info =
wenzelm
parents: 65145
diff changeset
   596
    {
wenzelm
parents: 65145
diff changeset
   597
      val r = snapshot.convert(r0)
wenzelm
parents: 65145
diff changeset
   598
      if (range == r) copy(messages = (serial -> tree) :: messages)
wenzelm
parents: 65145
diff changeset
   599
      else copy(range = r, messages = List(serial -> tree))
wenzelm
parents: 65145
diff changeset
   600
    }
wenzelm
parents: 65145
diff changeset
   601
    def + (r0: Text.Range, important: Boolean, tree: XML.Tree): Tooltip_Info =
wenzelm
parents: 65145
diff changeset
   602
    {
wenzelm
parents: 65145
diff changeset
   603
      val r = snapshot.convert(r0)
wenzelm
parents: 65145
diff changeset
   604
      if (range == r) copy(rev_infos = (important -> tree) :: rev_infos)
wenzelm
parents: 65145
diff changeset
   605
      else copy (range = r, rev_infos = List(important -> tree))
wenzelm
parents: 65145
diff changeset
   606
    }
67933
604da273e18d more robust timing info: do not rely on order of markup;
wenzelm
parents: 67824
diff changeset
   607
604da273e18d more robust timing info: do not rely on order of markup;
wenzelm
parents: 67824
diff changeset
   608
    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
   609
      tree match {
604da273e18d more robust timing info: do not rely on order of markup;
wenzelm
parents: 67824
diff changeset
   610
        case XML.Elem(Markup(Markup.TIMING, _), _) =>
604da273e18d more robust timing info: do not rely on order of markup;
wenzelm
parents: 67824
diff changeset
   611
          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
   612
        case _ => Some(tree)
604da273e18d more robust timing info: do not rely on order of markup;
wenzelm
parents: 67824
diff changeset
   613
      }
65149
wenzelm
parents: 65145
diff changeset
   614
    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
   615
      for {
604da273e18d more robust timing info: do not rely on order of markup;
wenzelm
parents: 67824
diff changeset
   616
        (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
   617
        tree1 <- timing_info(tree)
604da273e18d more robust timing info: do not rely on order of markup;
wenzelm
parents: 67824
diff changeset
   618
      } yield tree1
65149
wenzelm
parents: 65145
diff changeset
   619
  }
wenzelm
parents: 65145
diff changeset
   620
65488
331f09d9535e tuned signature;
wenzelm
parents: 65487
diff changeset
   621
  def perhaps_append_file(node_name: Document.Node.Name, name: String): String =
331f09d9535e tuned signature;
wenzelm
parents: 65487
diff changeset
   622
    if (Path.is_valid(name)) session.resources.append(node_name, Path.explode(name)) else name
65487
7847807b07ce tuned signature;
wenzelm
parents: 65222
diff changeset
   623
65149
wenzelm
parents: 65145
diff changeset
   624
  def tooltips(elements: Markup.Elements, range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
wenzelm
parents: 65145
diff changeset
   625
  {
wenzelm
parents: 65145
diff changeset
   626
    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
   627
      snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, command_states =>
65149
wenzelm
parents: 65145
diff changeset
   628
        {
wenzelm
parents: 65145
diff changeset
   629
          case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info + t)
wenzelm
parents: 65145
diff changeset
   630
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
   631
          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
   632
          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
   633
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
   634
          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
   635
          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
   636
            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
   637
            yield (info + (r0, i, tree))
65149
wenzelm
parents: 65145
diff changeset
   638
wenzelm
parents: 65145
diff changeset
   639
          case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _)))
wenzelm
parents: 65145
diff changeset
   640
          if kind != "" && kind != Markup.ML_DEF =>
wenzelm
parents: 65145
diff changeset
   641
            val kind1 = Word.implode(Word.explode('_', kind))
wenzelm
parents: 65145
diff changeset
   642
            val txt1 =
wenzelm
parents: 65145
diff changeset
   643
              if (name == "") kind1
wenzelm
parents: 65145
diff changeset
   644
              else if (kind1 == "") quote(name)
wenzelm
parents: 65145
diff changeset
   645
              else kind1 + " " + quote(name)
67933
604da273e18d more robust timing info: do not rely on order of markup;
wenzelm
parents: 67824
diff changeset
   646
            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
   647
            Some(if (kind == Markup.COMMAND) info1 + (r0, true, XML.elem(Markup.TIMING)) else info1)
65149
wenzelm
parents: 65145
diff changeset
   648
wenzelm
parents: 65145
diff changeset
   649
          case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
65488
331f09d9535e tuned signature;
wenzelm
parents: 65487
diff changeset
   650
            val file = perhaps_append_file(snapshot.node_name, name)
65149
wenzelm
parents: 65145
diff changeset
   651
            val text =
wenzelm
parents: 65145
diff changeset
   652
              if (name == file) "file " + quote(file)
wenzelm
parents: 65145
diff changeset
   653
              else "path " + quote(name) + "\nfile " + quote(file)
wenzelm
parents: 65145
diff changeset
   654
            Some(info + (r0, true, XML.Text(text)))
wenzelm
parents: 65145
diff changeset
   655
wenzelm
parents: 65145
diff changeset
   656
          case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) =>
wenzelm
parents: 65145
diff changeset
   657
            val text = "doc " + quote(name)
wenzelm
parents: 65145
diff changeset
   658
            Some(info + (r0, true, XML.Text(text)))
wenzelm
parents: 65145
diff changeset
   659
wenzelm
parents: 65145
diff changeset
   660
          case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) =>
wenzelm
parents: 65145
diff changeset
   661
            Some(info + (r0, true, XML.Text("URL " + quote(name))))
wenzelm
parents: 65145
diff changeset
   662
wenzelm
parents: 65145
diff changeset
   663
          case (info, Text.Info(r0, XML.Elem(Markup(name, _), body)))
wenzelm
parents: 65145
diff changeset
   664
          if name == Markup.SORTING || name == Markup.TYPING =>
wenzelm
parents: 65145
diff changeset
   665
            Some(info + (r0, true, Pretty.block(XML.Text("::") :: Pretty.brk(1) :: body)))
wenzelm
parents: 65145
diff changeset
   666
wenzelm
parents: 65145
diff changeset
   667
          case (info, Text.Info(r0, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
wenzelm
parents: 65145
diff changeset
   668
            Some(info + (r0, true, Pretty.block(0, body)))
wenzelm
parents: 65145
diff changeset
   669
wenzelm
parents: 65145
diff changeset
   670
          case (info, Text.Info(r0, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
wenzelm
parents: 65145
diff changeset
   671
            Some(info + (r0, false, Pretty.block(XML.Text("ML:") :: Pretty.brk(1) :: body)))
wenzelm
parents: 65145
diff changeset
   672
wenzelm
parents: 65145
diff changeset
   673
          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
   674
              val text =
fb8253564483 more robust debugger initialization, e.g. required for GUI components before actual session startup;
wenzelm
parents: 65213
diff changeset
   675
                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
   676
                else "breakpoint (disabled)"
fb8253564483 more robust debugger initialization, e.g. required for GUI components before actual session startup;
wenzelm
parents: 65213
diff changeset
   677
              Some(info + (r0, true, XML.Text(text)))
65149
wenzelm
parents: 65145
diff changeset
   678
          case (info, Text.Info(r0, XML.Elem(Markup.Language(language, _, _, _), _))) =>
wenzelm
parents: 65145
diff changeset
   679
            val lang = Word.implode(Word.explode('_', language))
wenzelm
parents: 65145
diff changeset
   680
            Some(info + (r0, true, XML.Text("language: " + lang)))
wenzelm
parents: 65145
diff changeset
   681
wenzelm
parents: 65145
diff changeset
   682
          case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) =>
wenzelm
parents: 65145
diff changeset
   683
            val descr = if (kind == "") "expression" else "expression: " + kind
wenzelm
parents: 65145
diff changeset
   684
            Some(info + (r0, true, XML.Text(descr)))
wenzelm
parents: 65145
diff changeset
   685
wenzelm
parents: 65145
diff changeset
   686
          case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
wenzelm
parents: 65145
diff changeset
   687
            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
   688
          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
   689
            Some(info + (r0, true, XML.Text("Markdown: item")))
65149
wenzelm
parents: 65145
diff changeset
   690
          case (info, Text.Info(r0, XML.Elem(Markup.Markdown_List(kind), _))) =>
wenzelm
parents: 65145
diff changeset
   691
            Some(info + (r0, true, XML.Text("Markdown: " + kind)))
wenzelm
parents: 65145
diff changeset
   692
wenzelm
parents: 65145
diff changeset
   693
          case (info, Text.Info(r0, XML.Elem(Markup(name, _), _))) =>
wenzelm
parents: 65145
diff changeset
   694
            Rendering.tooltip_descriptions.get(name).map(desc => info + (r0, true, XML.Text(desc)))
wenzelm
parents: 65145
diff changeset
   695
        }).map(_.info)
wenzelm
parents: 65145
diff changeset
   696
wenzelm
parents: 65145
diff changeset
   697
    if (results.isEmpty) None
wenzelm
parents: 65145
diff changeset
   698
    else {
wenzelm
parents: 65145
diff changeset
   699
      val r = Text.Range(results.head.range.start, results.last.range.stop)
wenzelm
parents: 65145
diff changeset
   700
      val all_tips =
72869
015a61936c13 clarified signature: more specific types;
wenzelm
parents: 72858
diff changeset
   701
        (SortedMap.empty[Long, XML.Tree] /: results.flatMap(_.messages))(_ + _)
015a61936c13 clarified signature: more specific types;
wenzelm
parents: 72858
diff changeset
   702
          .iterator.map(_._2).toList :::
65149
wenzelm
parents: 65145
diff changeset
   703
        results.flatMap(res => res.infos(true)) :::
wenzelm
parents: 65145
diff changeset
   704
        results.flatMap(res => res.infos(false)).lastOption.toList
wenzelm
parents: 65145
diff changeset
   705
      if (all_tips.isEmpty) None else Some(Text.Info(r, all_tips))
wenzelm
parents: 65145
diff changeset
   706
    }
wenzelm
parents: 65145
diff changeset
   707
  }
65911
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   708
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   709
71499
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 70135
diff changeset
   710
  /* messages */
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 70135
diff changeset
   711
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 70135
diff changeset
   712
  def warnings(range: Text.Range): List[Text.Markup] =
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 70135
diff changeset
   713
    snapshot.select(range, Rendering.warning_elements, _ => Some(_)).map(_.info)
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 70135
diff changeset
   714
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 70135
diff changeset
   715
  def errors(range: Text.Range): List[Text.Markup] =
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 70135
diff changeset
   716
    snapshot.select(range, Rendering.error_elements, _ => Some(_)).map(_.info)
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 70135
diff changeset
   717
29f37eb9bd0f more Isabelle/jEdit actions;
wenzelm
parents: 70135
diff changeset
   718
65911
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   719
  /* command status overview */
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   720
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   721
  def overview_color(range: Text.Range): Option[Rendering.Color.Value] =
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   722
  {
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   723
    if (snapshot.is_outdated) None
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   724
    else {
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   725
      val results =
68758
a110e7e24e55 clarified modules;
wenzelm
parents: 67933
diff changeset
   726
        snapshot.cumulate[List[Markup]](range, Nil, Document_Status.Command_Status.liberal_elements,
a110e7e24e55 clarified modules;
wenzelm
parents: 67933
diff changeset
   727
          _ =>
a110e7e24e55 clarified modules;
wenzelm
parents: 67933
diff changeset
   728
            {
a110e7e24e55 clarified modules;
wenzelm
parents: 67933
diff changeset
   729
              case (status, Text.Info(_, elem)) => Some(elem.markup :: status)
a110e7e24e55 clarified modules;
wenzelm
parents: 67933
diff changeset
   730
            }, status = true)
65911
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   731
      if (results.isEmpty) None
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   732
      else {
68758
a110e7e24e55 clarified modules;
wenzelm
parents: 67933
diff changeset
   733
        val status = Document_Status.Command_Status.make(results.iterator.flatMap(_.info))
65911
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   734
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   735
        if (status.is_running) Some(Rendering.Color.running)
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   736
        else if (status.is_failed) Some(Rendering.Color.error)
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   737
        else if (status.is_warned) Some(Rendering.Color.warning)
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   738
        else if (status.is_unprocessed) Some(Rendering.Color.unprocessed)
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   739
        else None
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   740
      }
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   741
    }
f97d163479b9 clarified modules;
wenzelm
parents: 65637
diff changeset
   742
  }
67132
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   743
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   744
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   745
  /* antiquoted text */
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   746
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   747
  def antiquoted(range: Text.Range): Option[Text.Range] =
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   748
    snapshot.cumulate[Option[Text.Range]](range, None, Rendering.antiquoted_elements, _ =>
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   749
      {
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   750
        case (res, info) => if (res.isEmpty) Some(Some(info.range)) else None
336831647779 added action to make antiquoted cartouche;
wenzelm
parents: 67014
diff changeset
   751
      }).headOption.flatMap(_.info)
69900
18a61caf5e68 support for document meta data in PIDE and RDF;
wenzelm
parents: 69899
diff changeset
   752
18a61caf5e68 support for document meta data in PIDE and RDF;
wenzelm
parents: 69899
diff changeset
   753
18a61caf5e68 support for document meta data in PIDE and RDF;
wenzelm
parents: 69899
diff changeset
   754
  /* meta data */
18a61caf5e68 support for document meta data in PIDE and RDF;
wenzelm
parents: 69899
diff changeset
   755
18a61caf5e68 support for document meta data in PIDE and RDF;
wenzelm
parents: 69899
diff changeset
   756
  def meta_data(range: Text.Range): Properties.T =
18a61caf5e68 support for document meta data in PIDE and RDF;
wenzelm
parents: 69899
diff changeset
   757
  {
18a61caf5e68 support for document meta data in PIDE and RDF;
wenzelm
parents: 69899
diff changeset
   758
    val results =
18a61caf5e68 support for document meta data in PIDE and RDF;
wenzelm
parents: 69899
diff changeset
   759
      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
   760
        {
18a61caf5e68 support for document meta data in PIDE and RDF;
wenzelm
parents: 69899
diff changeset
   761
          case (res, Text.Info(_, elem)) =>
18a61caf5e68 support for document meta data in PIDE and RDF;
wenzelm
parents: 69899
diff changeset
   762
            val plain_text = XML.content(elem)
18a61caf5e68 support for document meta data in PIDE and RDF;
wenzelm
parents: 69899
diff changeset
   763
            Some((elem.name -> plain_text) :: res)
18a61caf5e68 support for document meta data in PIDE and RDF;
wenzelm
parents: 69899
diff changeset
   764
        })
18a61caf5e68 support for document meta data in PIDE and RDF;
wenzelm
parents: 69899
diff changeset
   765
    Library.distinct(results.flatMap(_.info.reverse))
18a61caf5e68 support for document meta data in PIDE and RDF;
wenzelm
parents: 69899
diff changeset
   766
  }
70135
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 69970
diff changeset
   767
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 69970
diff changeset
   768
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 69970
diff changeset
   769
  /* 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
   770
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 69970
diff changeset
   771
  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
   772
  {
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 69970
diff changeset
   773
    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
   774
      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
   775
        {
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 69970
diff changeset
   776
          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
   777
          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
   778
        })
ad6d4a14adb5 report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents: 69970
diff changeset
   779
    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
   780
  }
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   781
}