src/Pure/PIDE/rendering.scala
author wenzelm
Tue, 03 Jan 2017 21:02:46 +0100
changeset 64767 f5c4ffdb1124
parent 64748 155bf8632104
child 64877 31e9920a0dc1
permissions -rw-r--r--
support VSCode DocumentHighlights; clarified modules;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/PIDE/rendering.scala
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     3
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     4
Isabelle-specific implementation of quasi-abstract rendering and
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     5
markup interpretation.
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     6
*/
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     7
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     8
package isabelle
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     9
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    10
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    11
object Rendering
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    12
{
64676
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    13
  /* message priorities */
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    14
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    15
  val state_pri = 1
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    16
  val writeln_pri = 2
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    17
  val information_pri = 3
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    18
  val tracing_pri = 4
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    19
  val warning_pri = 5
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    20
  val legacy_pri = 6
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    21
  val error_pri = 7
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    22
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    23
  val message_pri = Map(
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    24
    Markup.STATE -> state_pri,
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    25
    Markup.STATE_MESSAGE -> state_pri,
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    26
    Markup.WRITELN -> writeln_pri,
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    27
    Markup.WRITELN_MESSAGE -> writeln_pri,
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    28
    Markup.INFORMATION -> information_pri,
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    29
    Markup.INFORMATION_MESSAGE -> information_pri,
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    30
    Markup.TRACING -> tracing_pri,
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    31
    Markup.TRACING_MESSAGE -> tracing_pri,
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    32
    Markup.WARNING -> warning_pri,
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    33
    Markup.WARNING_MESSAGE -> warning_pri,
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    34
    Markup.LEGACY -> legacy_pri,
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    35
    Markup.LEGACY_MESSAGE -> legacy_pri,
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    36
    Markup.ERROR -> error_pri,
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    37
    Markup.ERROR_MESSAGE -> error_pri)
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    38
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    39
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    40
  /* markup elements */
fd2df1ea3bb4 clarified modules;
wenzelm
parents: 64660
diff changeset
    41
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    42
  private val tooltip_descriptions =
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    43
    Map(
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    44
      Markup.CITATION -> "citation",
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    45
      Markup.TOKEN_RANGE -> "inner syntax token",
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    46
      Markup.FREE -> "free variable",
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    47
      Markup.SKOLEM -> "skolem variable",
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    48
      Markup.BOUND -> "bound variable",
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    49
      Markup.VAR -> "schematic variable",
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    50
      Markup.TFREE -> "free type variable",
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    51
      Markup.TVAR -> "schematic type variable")
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    52
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    53
  private val tooltip_elements =
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    54
    Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    55
      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    56
      Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    57
      Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    58
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    59
  private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    60
    Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
    61
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
    62
  val caret_focus_elements = Markup.Elements(Markup.ENTITY)
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    63
}
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    64
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    65
abstract class Rendering(
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    66
  val snapshot: Document.Snapshot,
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    67
  val options: Options,
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    68
  val resources: Resources)
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    69
{
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    70
  override def toString: String = "Rendering(" + snapshot.toString + ")"
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    71
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    72
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    73
  /* tooltips */
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    74
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    75
  def tooltip_margin: Int
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    76
  def timing_threshold: Double
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    77
64748
155bf8632104 clarified multiple tooltips;
wenzelm
parents: 64676
diff changeset
    78
  def tooltips(range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    79
  {
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    80
    def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    81
      r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    82
    {
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    83
      val r = snapshot.convert(r0)
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    84
      val (t, info) = prev.info
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    85
      if (prev.range == r)
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    86
        Text.Info(r, (t, info :+ p))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    87
      else Text.Info(r, (t, Vector(p)))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    88
    }
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    89
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    90
    val results =
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    91
      snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    92
        range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    93
        {
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    94
          case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    95
            Some(Text.Info(r, (t1 + t2, info)))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    96
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    97
          case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
64660
ef85bb6491b3 omit unused markup;
wenzelm
parents: 64654
diff changeset
    98
          if kind != "" && kind != Markup.ML_DEF =>
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    99
            val kind1 = Word.implode(Word.explode('_', kind))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   100
            val txt1 =
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   101
              if (name == "") kind1
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   102
              else if (kind1 == "") quote(name)
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   103
              else kind1 + " " + quote(name)
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   104
            val t = prev.info._1
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   105
            val txt2 =
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   106
              if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   107
                "\n" + t.message
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   108
              else ""
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   109
            Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   110
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   111
          case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
64654
31b681e38c70 clarified signature;
wenzelm
parents: 64648
diff changeset
   112
            val file = resources.append_file(snapshot.node_name.master_dir, name)
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   113
            val text =
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   114
              if (name == file) "file " + quote(file)
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   115
              else "path " + quote(name) + "\nfile " + quote(file)
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   116
            Some(add(prev, r, (true, XML.Text(text))))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   117
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   118
          case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) =>
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   119
            val text = "doc " + quote(name)
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   120
            Some(add(prev, r, (true, XML.Text(text))))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   121
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   122
          case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   123
            Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   124
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   125
          case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   126
          if name == Markup.SORTING || name == Markup.TYPING =>
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   127
            Some(add(prev, r, (true, Rendering.pretty_typing("::", body))))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   128
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   129
          case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   130
            Some(add(prev, r, (true, Pretty.block(0, body))))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   131
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   132
          case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   133
            Some(add(prev, r, (false, Rendering.pretty_typing("ML:", body))))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   134
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   135
          case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) =>
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   136
            val text =
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   137
              if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   138
              else "breakpoint (disabled)"
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   139
            Some(add(prev, r, (true, XML.Text(text))))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   140
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   141
          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   142
            val lang = Word.implode(Word.explode('_', language))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   143
            Some(add(prev, r, (true, XML.Text("language: " + lang))))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   144
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   145
          case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   146
            val descr = if (kind == "") "expression" else "expression: " + kind
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   147
            Some(add(prev, r, (true, XML.Text(descr))))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   148
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   149
          case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   150
            Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   151
          case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   152
            Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   153
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   154
          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   155
            Rendering.tooltip_descriptions.get(name).
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   156
              map(descr => add(prev, r, (true, XML.Text(descr))))
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   157
        }).map(_.info)
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   158
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   159
    results.map(_.info).flatMap(res => res._2.toList) match {
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   160
      case Nil => None
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   161
      case tips =>
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   162
        val r = Text.Range(results.head.range.start, results.last.range.stop)
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   163
        val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
64748
155bf8632104 clarified multiple tooltips;
wenzelm
parents: 64676
diff changeset
   164
        Some(Text.Info(r, all_tips))
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   165
    }
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   166
  }
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   167
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   168
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   169
  /* caret focus */
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   170
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   171
  private def entity_focus(range: Text.Range,
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   172
    check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] =
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   173
  {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   174
    val results =
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   175
      snapshot.cumulate[Set[Long]](range, Set.empty, Rendering.caret_focus_elements, _ =>
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   176
          {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   177
            case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   178
              props match {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   179
                case Markup.Entity.Def(i) if check(true, i) => Some(serials + i)
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   180
                case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   181
                case _ => None
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   182
              }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   183
            case _ => None
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   184
          })
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   185
    (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   186
  }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   187
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   188
  def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   189
  {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   190
    val focus_defs = entity_focus(caret_range)
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   191
    if (focus_defs.nonEmpty) focus_defs
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   192
    else {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   193
      val visible_defs = entity_focus(visible_range)
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   194
      entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i))
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   195
    }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   196
  }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   197
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   198
  def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   199
  {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   200
    val focus = caret_focus(caret_range, visible_range)
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   201
    if (focus.nonEmpty) {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   202
      val results =
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   203
        snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ =>
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   204
          {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   205
            case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   206
              props match {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   207
                case Markup.Entity.Def(i) if focus(i) => Some(true)
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   208
                case Markup.Entity.Ref(i) if focus(i) => Some(true)
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   209
                case _ => None
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   210
              }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   211
          })
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   212
      for (info <- results if info.info) yield info.range
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   213
    }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   214
    else Nil
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64748
diff changeset
   215
  }
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   216
}