src/Pure/PIDE/rendering.scala
author wenzelm
Wed Dec 21 21:18:37 2016 +0100 (2016-12-21)
changeset 64648 5d7f741aaccb
parent 64622 529bbb8977c7
child 64654 31b681e38c70
permissions -rw-r--r--
basic support for hyperlinks / Goto Definition Request;
wenzelm@64622
     1
/*  Title:      Pure/PIDE/rendering.scala
wenzelm@64622
     2
    Author:     Makarius
wenzelm@64622
     3
wenzelm@64622
     4
Isabelle-specific implementation of quasi-abstract rendering and
wenzelm@64622
     5
markup interpretation.
wenzelm@64622
     6
*/
wenzelm@64622
     7
wenzelm@64622
     8
package isabelle
wenzelm@64622
     9
wenzelm@64622
    10
wenzelm@64622
    11
object Rendering
wenzelm@64622
    12
{
wenzelm@64622
    13
  private val tooltip_descriptions =
wenzelm@64622
    14
    Map(
wenzelm@64622
    15
      Markup.CITATION -> "citation",
wenzelm@64622
    16
      Markup.TOKEN_RANGE -> "inner syntax token",
wenzelm@64622
    17
      Markup.FREE -> "free variable",
wenzelm@64622
    18
      Markup.SKOLEM -> "skolem variable",
wenzelm@64622
    19
      Markup.BOUND -> "bound variable",
wenzelm@64622
    20
      Markup.VAR -> "schematic variable",
wenzelm@64622
    21
      Markup.TFREE -> "free type variable",
wenzelm@64622
    22
      Markup.TVAR -> "schematic type variable")
wenzelm@64622
    23
wenzelm@64622
    24
  private val tooltip_elements =
wenzelm@64622
    25
    Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
wenzelm@64622
    26
      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
wenzelm@64622
    27
      Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
wenzelm@64622
    28
      Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
wenzelm@64622
    29
wenzelm@64622
    30
  private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
wenzelm@64622
    31
    Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
wenzelm@64622
    32
}
wenzelm@64622
    33
wenzelm@64622
    34
abstract class Rendering(
wenzelm@64622
    35
  val snapshot: Document.Snapshot,
wenzelm@64622
    36
  val options: Options,
wenzelm@64622
    37
  val resources: Resources)
wenzelm@64622
    38
{
wenzelm@64622
    39
  override def toString: String = "Rendering(" + snapshot.toString + ")"
wenzelm@64622
    40
wenzelm@64622
    41
wenzelm@64622
    42
  /* resources */
wenzelm@64622
    43
wenzelm@64622
    44
  def resolve_file(name: String): String =
wenzelm@64622
    45
    if (Path.is_valid(name))
wenzelm@64622
    46
      resources.append(snapshot.node_name.master_dir, Path.explode(name))
wenzelm@64622
    47
    else name
wenzelm@64622
    48
wenzelm@64648
    49
  def resolve_file_url(name: String): String =
wenzelm@64648
    50
    if (Path.is_valid(name))
wenzelm@64648
    51
      "file://" + resources.append(snapshot.node_name.master_dir, Path.explode(name))
wenzelm@64648
    52
    else name
wenzelm@64648
    53
wenzelm@64622
    54
wenzelm@64622
    55
  /* tooltips */
wenzelm@64622
    56
wenzelm@64622
    57
  def tooltip_margin: Int
wenzelm@64622
    58
  def timing_threshold: Double
wenzelm@64622
    59
wenzelm@64622
    60
  def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
wenzelm@64622
    61
  {
wenzelm@64622
    62
    def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
wenzelm@64622
    63
      r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
wenzelm@64622
    64
    {
wenzelm@64622
    65
      val r = snapshot.convert(r0)
wenzelm@64622
    66
      val (t, info) = prev.info
wenzelm@64622
    67
      if (prev.range == r)
wenzelm@64622
    68
        Text.Info(r, (t, info :+ p))
wenzelm@64622
    69
      else Text.Info(r, (t, Vector(p)))
wenzelm@64622
    70
    }
wenzelm@64622
    71
wenzelm@64622
    72
    val results =
wenzelm@64622
    73
      snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
wenzelm@64622
    74
        range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
wenzelm@64622
    75
        {
wenzelm@64622
    76
          case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
wenzelm@64622
    77
            Some(Text.Info(r, (t1 + t2, info)))
wenzelm@64622
    78
wenzelm@64622
    79
          case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
wenzelm@64622
    80
          if kind != "" &&
wenzelm@64622
    81
            kind != Markup.ML_DEF &&
wenzelm@64622
    82
            kind != Markup.ML_OPEN &&
wenzelm@64622
    83
            kind != Markup.ML_STRUCTURE =>
wenzelm@64622
    84
            val kind1 = Word.implode(Word.explode('_', kind))
wenzelm@64622
    85
            val txt1 =
wenzelm@64622
    86
              if (name == "") kind1
wenzelm@64622
    87
              else if (kind1 == "") quote(name)
wenzelm@64622
    88
              else kind1 + " " + quote(name)
wenzelm@64622
    89
            val t = prev.info._1
wenzelm@64622
    90
            val txt2 =
wenzelm@64622
    91
              if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
wenzelm@64622
    92
                "\n" + t.message
wenzelm@64622
    93
              else ""
wenzelm@64622
    94
            Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
wenzelm@64622
    95
wenzelm@64622
    96
          case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
wenzelm@64622
    97
            val file = resolve_file(name)
wenzelm@64622
    98
            val text =
wenzelm@64622
    99
              if (name == file) "file " + quote(file)
wenzelm@64622
   100
              else "path " + quote(name) + "\nfile " + quote(file)
wenzelm@64622
   101
            Some(add(prev, r, (true, XML.Text(text))))
wenzelm@64622
   102
wenzelm@64622
   103
          case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) =>
wenzelm@64622
   104
            val text = "doc " + quote(name)
wenzelm@64622
   105
            Some(add(prev, r, (true, XML.Text(text))))
wenzelm@64622
   106
wenzelm@64622
   107
          case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
wenzelm@64622
   108
            Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
wenzelm@64622
   109
wenzelm@64622
   110
          case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
wenzelm@64622
   111
          if name == Markup.SORTING || name == Markup.TYPING =>
wenzelm@64622
   112
            Some(add(prev, r, (true, Rendering.pretty_typing("::", body))))
wenzelm@64622
   113
wenzelm@64622
   114
          case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
wenzelm@64622
   115
            Some(add(prev, r, (true, Pretty.block(0, body))))
wenzelm@64622
   116
wenzelm@64622
   117
          case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
wenzelm@64622
   118
            Some(add(prev, r, (false, Rendering.pretty_typing("ML:", body))))
wenzelm@64622
   119
wenzelm@64622
   120
          case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) =>
wenzelm@64622
   121
            val text =
wenzelm@64622
   122
              if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
wenzelm@64622
   123
              else "breakpoint (disabled)"
wenzelm@64622
   124
            Some(add(prev, r, (true, XML.Text(text))))
wenzelm@64622
   125
wenzelm@64622
   126
          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
wenzelm@64622
   127
            val lang = Word.implode(Word.explode('_', language))
wenzelm@64622
   128
            Some(add(prev, r, (true, XML.Text("language: " + lang))))
wenzelm@64622
   129
wenzelm@64622
   130
          case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
wenzelm@64622
   131
            val descr = if (kind == "") "expression" else "expression: " + kind
wenzelm@64622
   132
            Some(add(prev, r, (true, XML.Text(descr))))
wenzelm@64622
   133
wenzelm@64622
   134
          case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
wenzelm@64622
   135
            Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
wenzelm@64622
   136
          case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
wenzelm@64622
   137
            Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
wenzelm@64622
   138
wenzelm@64622
   139
          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
wenzelm@64622
   140
            Rendering.tooltip_descriptions.get(name).
wenzelm@64622
   141
              map(descr => add(prev, r, (true, XML.Text(descr))))
wenzelm@64622
   142
        }).map(_.info)
wenzelm@64622
   143
wenzelm@64622
   144
    results.map(_.info).flatMap(res => res._2.toList) match {
wenzelm@64622
   145
      case Nil => None
wenzelm@64622
   146
      case tips =>
wenzelm@64622
   147
        val r = Text.Range(results.head.range.start, results.last.range.stop)
wenzelm@64622
   148
        val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
wenzelm@64622
   149
        Some(Text.Info(r, Library.separate(Pretty.fbrk, all_tips)))
wenzelm@64622
   150
    }
wenzelm@64622
   151
  }
wenzelm@64622
   152
}