src/Pure/PIDE/rendering.scala
author wenzelm
Sat Mar 04 21:47:26 2017 +0100 (2017-03-04)
changeset 65107 70b0113fa4ef
parent 65104 66b19d05dcee
child 65121 12c6774a8f65
permissions -rw-r--r--
clarified pretty margin;
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@65101
    13
  /* color */
wenzelm@65101
    14
wenzelm@65101
    15
  object Color extends Enumeration
wenzelm@65101
    16
  {
wenzelm@65104
    17
    // background
wenzelm@65101
    18
    val unprocessed1 = Value("unprocessed1")
wenzelm@65101
    19
    val running1 = Value("running1")
wenzelm@65101
    20
    val bad = Value("bad")
wenzelm@65101
    21
    val intensify = Value("intensify")
wenzelm@65101
    22
    val entity = Value("entity")
wenzelm@65101
    23
    val active = Value("active")
wenzelm@65101
    24
    val active_result = Value("active_result")
wenzelm@65101
    25
    val markdown_item1 = Value("markdown_item1")
wenzelm@65101
    26
    val markdown_item2 = Value("markdown_item2")
wenzelm@65101
    27
    val markdown_item3 = Value("markdown_item3")
wenzelm@65101
    28
    val markdown_item4 = Value("markdown_item4")
wenzelm@65104
    29
    val background = values
wenzelm@65104
    30
wenzelm@65104
    31
    // foreground
wenzelm@65104
    32
    val quoted = Value("quoted")
wenzelm@65104
    33
    val antiquoted = Value("antiquoted")
wenzelm@65104
    34
    val foreground = values -- background
wenzelm@65101
    35
  }
wenzelm@65101
    36
wenzelm@65101
    37
wenzelm@64676
    38
  /* message priorities */
wenzelm@64676
    39
wenzelm@64676
    40
  val state_pri = 1
wenzelm@64676
    41
  val writeln_pri = 2
wenzelm@64676
    42
  val information_pri = 3
wenzelm@64676
    43
  val tracing_pri = 4
wenzelm@64676
    44
  val warning_pri = 5
wenzelm@64676
    45
  val legacy_pri = 6
wenzelm@64676
    46
  val error_pri = 7
wenzelm@64676
    47
wenzelm@64676
    48
  val message_pri = Map(
wenzelm@64676
    49
    Markup.STATE -> state_pri,
wenzelm@64676
    50
    Markup.STATE_MESSAGE -> state_pri,
wenzelm@64676
    51
    Markup.WRITELN -> writeln_pri,
wenzelm@64676
    52
    Markup.WRITELN_MESSAGE -> writeln_pri,
wenzelm@64676
    53
    Markup.INFORMATION -> information_pri,
wenzelm@64676
    54
    Markup.INFORMATION_MESSAGE -> information_pri,
wenzelm@64676
    55
    Markup.TRACING -> tracing_pri,
wenzelm@64676
    56
    Markup.TRACING_MESSAGE -> tracing_pri,
wenzelm@64676
    57
    Markup.WARNING -> warning_pri,
wenzelm@64676
    58
    Markup.WARNING_MESSAGE -> warning_pri,
wenzelm@64676
    59
    Markup.LEGACY -> legacy_pri,
wenzelm@64676
    60
    Markup.LEGACY_MESSAGE -> legacy_pri,
wenzelm@64676
    61
    Markup.ERROR -> error_pri,
wenzelm@64676
    62
    Markup.ERROR_MESSAGE -> error_pri)
wenzelm@64676
    63
wenzelm@64676
    64
wenzelm@64676
    65
  /* markup elements */
wenzelm@64676
    66
wenzelm@65101
    67
  val active_elements =
wenzelm@65101
    68
    Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
wenzelm@65101
    69
      Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
wenzelm@65101
    70
wenzelm@65101
    71
  private val background_elements =
wenzelm@65101
    72
    Protocol.proper_status_elements + Markup.WRITELN_MESSAGE +
wenzelm@65101
    73
      Markup.STATE_MESSAGE + Markup.INFORMATION_MESSAGE +
wenzelm@65101
    74
      Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
wenzelm@65101
    75
      Markup.LEGACY_MESSAGE + Markup.ERROR_MESSAGE +
wenzelm@65101
    76
      Markup.BAD + Markup.INTENSIFY + Markup.ENTITY +
wenzelm@65101
    77
      Markup.Markdown_Item.name ++ active_elements
wenzelm@65101
    78
wenzelm@65101
    79
  private val foreground_elements =
wenzelm@65101
    80
    Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
wenzelm@65101
    81
      Markup.CARTOUCHE, Markup.ANTIQUOTED)
wenzelm@65101
    82
wenzelm@64877
    83
  private val semantic_completion_elements =
wenzelm@64877
    84
    Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
wenzelm@64877
    85
wenzelm@64622
    86
  private val tooltip_descriptions =
wenzelm@64622
    87
    Map(
wenzelm@64622
    88
      Markup.CITATION -> "citation",
wenzelm@64622
    89
      Markup.TOKEN_RANGE -> "inner syntax token",
wenzelm@64622
    90
      Markup.FREE -> "free variable",
wenzelm@64622
    91
      Markup.SKOLEM -> "skolem variable",
wenzelm@64622
    92
      Markup.BOUND -> "bound variable",
wenzelm@64622
    93
      Markup.VAR -> "schematic variable",
wenzelm@64622
    94
      Markup.TFREE -> "free type variable",
wenzelm@64622
    95
      Markup.TVAR -> "schematic type variable")
wenzelm@64622
    96
wenzelm@64622
    97
  private val tooltip_elements =
wenzelm@64622
    98
    Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
wenzelm@64622
    99
      Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
wenzelm@64622
   100
      Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH,
wenzelm@64622
   101
      Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet)
wenzelm@64622
   102
wenzelm@64622
   103
  private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
wenzelm@64622
   104
    Pretty.block(XML.Text(kind) :: Pretty.brk(1) :: body)
wenzelm@64767
   105
wenzelm@64767
   106
  val caret_focus_elements = Markup.Elements(Markup.ENTITY)
wenzelm@64622
   107
}
wenzelm@64622
   108
wenzelm@64622
   109
abstract class Rendering(
wenzelm@64622
   110
  val snapshot: Document.Snapshot,
wenzelm@64622
   111
  val options: Options,
wenzelm@64622
   112
  val resources: Resources)
wenzelm@64622
   113
{
wenzelm@64622
   114
  override def toString: String = "Rendering(" + snapshot.toString + ")"
wenzelm@64622
   115
wenzelm@64622
   116
wenzelm@64877
   117
  /* completion */
wenzelm@64877
   118
wenzelm@64877
   119
  def semantic_completion(completed_range: Option[Text.Range], range: Text.Range)
wenzelm@64877
   120
      : Option[Text.Info[Completion.Semantic]] =
wenzelm@64877
   121
    if (snapshot.is_outdated) None
wenzelm@64877
   122
    else {
wenzelm@64877
   123
      snapshot.select(range, Rendering.semantic_completion_elements, _ =>
wenzelm@64877
   124
        {
wenzelm@64877
   125
          case Completion.Semantic.Info(info) =>
wenzelm@64877
   126
            completed_range match {
wenzelm@64877
   127
              case Some(range0) if range0.contains(info.range) && range0 != info.range => None
wenzelm@64877
   128
              case _ => Some(info)
wenzelm@64877
   129
            }
wenzelm@64877
   130
          case _ => None
wenzelm@64877
   131
        }).headOption.map(_.info)
wenzelm@64877
   132
    }
wenzelm@64877
   133
wenzelm@64877
   134
wenzelm@64622
   135
  /* tooltips */
wenzelm@64622
   136
wenzelm@64622
   137
  def timing_threshold: Double
wenzelm@64622
   138
wenzelm@64748
   139
  def tooltips(range: Text.Range): Option[Text.Info[List[XML.Tree]]] =
wenzelm@64622
   140
  {
wenzelm@64622
   141
    def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
wenzelm@64622
   142
      r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
wenzelm@64622
   143
    {
wenzelm@64622
   144
      val r = snapshot.convert(r0)
wenzelm@64622
   145
      val (t, info) = prev.info
wenzelm@64622
   146
      if (prev.range == r)
wenzelm@64622
   147
        Text.Info(r, (t, info :+ p))
wenzelm@64622
   148
      else Text.Info(r, (t, Vector(p)))
wenzelm@64622
   149
    }
wenzelm@64622
   150
wenzelm@64622
   151
    val results =
wenzelm@64622
   152
      snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
wenzelm@64622
   153
        range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
wenzelm@64622
   154
        {
wenzelm@64622
   155
          case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
wenzelm@64622
   156
            Some(Text.Info(r, (t1 + t2, info)))
wenzelm@64622
   157
wenzelm@64622
   158
          case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _)))
wenzelm@64660
   159
          if kind != "" && kind != Markup.ML_DEF =>
wenzelm@64622
   160
            val kind1 = Word.implode(Word.explode('_', kind))
wenzelm@64622
   161
            val txt1 =
wenzelm@64622
   162
              if (name == "") kind1
wenzelm@64622
   163
              else if (kind1 == "") quote(name)
wenzelm@64622
   164
              else kind1 + " " + quote(name)
wenzelm@64622
   165
            val t = prev.info._1
wenzelm@64622
   166
            val txt2 =
wenzelm@64622
   167
              if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
wenzelm@64622
   168
                "\n" + t.message
wenzelm@64622
   169
              else ""
wenzelm@64622
   170
            Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
wenzelm@64622
   171
wenzelm@64622
   172
          case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
wenzelm@64654
   173
            val file = resources.append_file(snapshot.node_name.master_dir, name)
wenzelm@64622
   174
            val text =
wenzelm@64622
   175
              if (name == file) "file " + quote(file)
wenzelm@64622
   176
              else "path " + quote(name) + "\nfile " + quote(file)
wenzelm@64622
   177
            Some(add(prev, r, (true, XML.Text(text))))
wenzelm@64622
   178
wenzelm@64622
   179
          case (prev, Text.Info(r, XML.Elem(Markup.Doc(name), _))) =>
wenzelm@64622
   180
            val text = "doc " + quote(name)
wenzelm@64622
   181
            Some(add(prev, r, (true, XML.Text(text))))
wenzelm@64622
   182
wenzelm@64622
   183
          case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
wenzelm@64622
   184
            Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
wenzelm@64622
   185
wenzelm@64622
   186
          case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
wenzelm@64622
   187
          if name == Markup.SORTING || name == Markup.TYPING =>
wenzelm@64622
   188
            Some(add(prev, r, (true, Rendering.pretty_typing("::", body))))
wenzelm@64622
   189
wenzelm@64622
   190
          case (prev, Text.Info(r, XML.Elem(Markup(Markup.CLASS_PARAMETER, _), body))) =>
wenzelm@64622
   191
            Some(add(prev, r, (true, Pretty.block(0, body))))
wenzelm@64622
   192
wenzelm@64622
   193
          case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
wenzelm@64622
   194
            Some(add(prev, r, (false, Rendering.pretty_typing("ML:", body))))
wenzelm@64622
   195
wenzelm@64622
   196
          case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) =>
wenzelm@64622
   197
            val text =
wenzelm@64622
   198
              if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
wenzelm@64622
   199
              else "breakpoint (disabled)"
wenzelm@64622
   200
            Some(add(prev, r, (true, XML.Text(text))))
wenzelm@64622
   201
wenzelm@64622
   202
          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
wenzelm@64622
   203
            val lang = Word.implode(Word.explode('_', language))
wenzelm@64622
   204
            Some(add(prev, r, (true, XML.Text("language: " + lang))))
wenzelm@64622
   205
wenzelm@64622
   206
          case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
wenzelm@64622
   207
            val descr = if (kind == "") "expression" else "expression: " + kind
wenzelm@64622
   208
            Some(add(prev, r, (true, XML.Text(descr))))
wenzelm@64622
   209
wenzelm@64622
   210
          case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
wenzelm@64622
   211
            Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
wenzelm@64622
   212
          case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
wenzelm@64622
   213
            Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
wenzelm@64622
   214
wenzelm@64622
   215
          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
wenzelm@64622
   216
            Rendering.tooltip_descriptions.get(name).
wenzelm@64622
   217
              map(descr => add(prev, r, (true, XML.Text(descr))))
wenzelm@64622
   218
        }).map(_.info)
wenzelm@64622
   219
wenzelm@64622
   220
    results.map(_.info).flatMap(res => res._2.toList) match {
wenzelm@64622
   221
      case Nil => None
wenzelm@64622
   222
      case tips =>
wenzelm@64622
   223
        val r = Text.Range(results.head.range.start, results.last.range.stop)
wenzelm@64622
   224
        val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
wenzelm@64748
   225
        Some(Text.Info(r, all_tips))
wenzelm@64622
   226
    }
wenzelm@64622
   227
  }
wenzelm@64767
   228
wenzelm@64767
   229
wenzelm@65101
   230
  /* text background */
wenzelm@65101
   231
wenzelm@65101
   232
  def background(range: Text.Range, focus: Set[Long]): List[Text.Info[Rendering.Color.Value]] =
wenzelm@65101
   233
  {
wenzelm@65101
   234
    for {
wenzelm@65101
   235
      Text.Info(r, result) <-
wenzelm@65101
   236
        snapshot.cumulate[(List[Markup], Option[Rendering.Color.Value])](
wenzelm@65101
   237
          range, (List(Markup.Empty), None), Rendering.background_elements,
wenzelm@65101
   238
          command_states =>
wenzelm@65101
   239
            {
wenzelm@65101
   240
              case (((markups, color), Text.Info(_, XML.Elem(markup, _))))
wenzelm@65101
   241
              if markups.nonEmpty && Protocol.proper_status_elements(markup.name) =>
wenzelm@65101
   242
                Some((markup :: markups, color))
wenzelm@65101
   243
              case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
wenzelm@65101
   244
                Some((Nil, Some(Rendering.Color.bad)))
wenzelm@65101
   245
              case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
wenzelm@65101
   246
                Some((Nil, Some(Rendering.Color.intensify)))
wenzelm@65101
   247
              case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
wenzelm@65101
   248
                props match {
wenzelm@65101
   249
                  case Markup.Entity.Def(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
wenzelm@65101
   250
                  case Markup.Entity.Ref(i) if focus(i) => Some((Nil, Some(Rendering.Color.entity)))
wenzelm@65101
   251
                  case _ => None
wenzelm@65101
   252
                }
wenzelm@65101
   253
              case (_, Text.Info(_, XML.Elem(Markup.Markdown_Item(depth), _))) =>
wenzelm@65101
   254
                val color =
wenzelm@65101
   255
                  depth match {
wenzelm@65101
   256
                    case 1 => Rendering.Color.markdown_item1
wenzelm@65101
   257
                    case 2 => Rendering.Color.markdown_item2
wenzelm@65101
   258
                    case 3 => Rendering.Color.markdown_item3
wenzelm@65101
   259
                    case _ => Rendering.Color.markdown_item4
wenzelm@65101
   260
                  }
wenzelm@65101
   261
                Some((Nil, Some(color)))
wenzelm@65101
   262
              case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
wenzelm@65101
   263
                command_states.collectFirst(
wenzelm@65101
   264
                  { case st if st.results.defined(serial) => st.results.get(serial).get }) match
wenzelm@65101
   265
                {
wenzelm@65101
   266
                  case Some(Protocol.Dialog_Result(res)) if res == result =>
wenzelm@65101
   267
                    Some((Nil, Some(Rendering.Color.active_result)))
wenzelm@65101
   268
                  case _ =>
wenzelm@65101
   269
                    Some((Nil, Some(Rendering.Color.active)))
wenzelm@65101
   270
                }
wenzelm@65101
   271
              case (_, Text.Info(_, elem)) =>
wenzelm@65101
   272
                if (Rendering.active_elements(elem.name))
wenzelm@65101
   273
                  Some((Nil, Some(Rendering.Color.active)))
wenzelm@65101
   274
                else None
wenzelm@65101
   275
            })
wenzelm@65101
   276
      color <-
wenzelm@65101
   277
        (result match {
wenzelm@65101
   278
          case (markups, opt_color) if markups.nonEmpty =>
wenzelm@65101
   279
            val status = Protocol.Status.make(markups.iterator)
wenzelm@65101
   280
            if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
wenzelm@65101
   281
            else if (status.is_running) Some(Rendering.Color.running1)
wenzelm@65101
   282
            else opt_color
wenzelm@65101
   283
          case (_, opt_color) => opt_color
wenzelm@65101
   284
        })
wenzelm@65101
   285
    } yield Text.Info(r, color)
wenzelm@65101
   286
  }
wenzelm@65101
   287
wenzelm@65101
   288
wenzelm@65101
   289
  /* text foreground */
wenzelm@65101
   290
wenzelm@65101
   291
  def foreground(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
wenzelm@65101
   292
    snapshot.select(range, Rendering.foreground_elements, _ =>
wenzelm@65101
   293
      {
wenzelm@65101
   294
        case Text.Info(_, elem) =>
wenzelm@65101
   295
          if (elem.name == Markup.ANTIQUOTED) Some(Rendering.Color.antiquoted)
wenzelm@65101
   296
          else Some(Rendering.Color.quoted)
wenzelm@65101
   297
      })
wenzelm@65101
   298
wenzelm@65101
   299
wenzelm@64767
   300
  /* caret focus */
wenzelm@64767
   301
wenzelm@64767
   302
  private def entity_focus(range: Text.Range,
wenzelm@64767
   303
    check: (Boolean, Long) => Boolean = (is_def: Boolean, i: Long) => is_def): Set[Long] =
wenzelm@64767
   304
  {
wenzelm@64767
   305
    val results =
wenzelm@64767
   306
      snapshot.cumulate[Set[Long]](range, Set.empty, Rendering.caret_focus_elements, _ =>
wenzelm@64767
   307
          {
wenzelm@64767
   308
            case (serials, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
wenzelm@64767
   309
              props match {
wenzelm@64767
   310
                case Markup.Entity.Def(i) if check(true, i) => Some(serials + i)
wenzelm@64767
   311
                case Markup.Entity.Ref(i) if check(false, i) => Some(serials + i)
wenzelm@64767
   312
                case _ => None
wenzelm@64767
   313
              }
wenzelm@64767
   314
            case _ => None
wenzelm@64767
   315
          })
wenzelm@64767
   316
    (Set.empty[Long] /: results){ case (s1, Text.Info(_, s2)) => s1 ++ s2 }
wenzelm@64767
   317
  }
wenzelm@64767
   318
wenzelm@64767
   319
  def caret_focus(caret_range: Text.Range, visible_range: Text.Range): Set[Long] =
wenzelm@64767
   320
  {
wenzelm@64767
   321
    val focus_defs = entity_focus(caret_range)
wenzelm@64767
   322
    if (focus_defs.nonEmpty) focus_defs
wenzelm@64767
   323
    else {
wenzelm@64767
   324
      val visible_defs = entity_focus(visible_range)
wenzelm@64767
   325
      entity_focus(caret_range, (is_def: Boolean, i: Long) => !is_def && visible_defs.contains(i))
wenzelm@64767
   326
    }
wenzelm@64767
   327
  }
wenzelm@64767
   328
wenzelm@64767
   329
  def caret_focus_ranges(caret_range: Text.Range, visible_range: Text.Range): List[Text.Range] =
wenzelm@64767
   330
  {
wenzelm@64767
   331
    val focus = caret_focus(caret_range, visible_range)
wenzelm@64767
   332
    if (focus.nonEmpty) {
wenzelm@64767
   333
      val results =
wenzelm@64767
   334
        snapshot.cumulate[Boolean](visible_range, false, Rendering.caret_focus_elements, _ =>
wenzelm@64767
   335
          {
wenzelm@64767
   336
            case (_, Text.Info(_, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
wenzelm@64767
   337
              props match {
wenzelm@64767
   338
                case Markup.Entity.Def(i) if focus(i) => Some(true)
wenzelm@64767
   339
                case Markup.Entity.Ref(i) if focus(i) => Some(true)
wenzelm@64767
   340
                case _ => None
wenzelm@64767
   341
              }
wenzelm@64767
   342
          })
wenzelm@64767
   343
      for (info <- results if info.info) yield info.range
wenzelm@64767
   344
    }
wenzelm@64767
   345
    else Nil
wenzelm@64767
   346
  }
wenzelm@64622
   347
}