src/Tools/VSCode/src/vscode_rendering.scala
author wenzelm
Mon Mar 11 18:58:06 2019 +0100 (2 months ago ago)
changeset 70079 990c6e8faf2c
parent 69261 c78c95d2a3d1
permissions -rw-r--r--
tuned signature;
wenzelm@64623
     1
/*  Title:      Tools/VSCode/src/vscode_rendering.scala
wenzelm@64623
     2
    Author:     Makarius
wenzelm@64623
     3
wenzelm@64623
     4
Isabelle/VSCode-specific implementation of quasi-abstract rendering and
wenzelm@64623
     5
markup interpretation.
wenzelm@64623
     6
*/
wenzelm@64623
     7
wenzelm@64623
     8
package isabelle.vscode
wenzelm@64623
     9
wenzelm@64623
    10
wenzelm@64623
    11
import isabelle._
wenzelm@64623
    12
wenzelm@64778
    13
import java.io.{File => JFile}
wenzelm@64778
    14
wenzelm@65913
    15
import scala.annotation.tailrec
wenzelm@65913
    16
wenzelm@64778
    17
wenzelm@64648
    18
object VSCode_Rendering
wenzelm@64648
    19
{
wenzelm@65105
    20
  /* decorations */
wenzelm@65105
    21
wenzelm@65122
    22
  private def color_decorations(prefix: String, types: Set[Rendering.Color.Value],
wenzelm@65105
    23
    colors: List[Text.Info[Rendering.Color.Value]]): List[Document_Model.Decoration] =
wenzelm@65105
    24
  {
wenzelm@65105
    25
    val color_ranges =
wenzelm@65105
    26
      (Map.empty[Rendering.Color.Value, List[Text.Range]] /: colors) {
wenzelm@65105
    27
        case (m, Text.Info(range, c)) => m + (c -> (range :: m.getOrElse(c, Nil)))
wenzelm@65105
    28
      }
wenzelm@65106
    29
    types.toList.map(c =>
wenzelm@65140
    30
      Document_Model.Decoration.ranges(prefix + c.toString, color_ranges.getOrElse(c, Nil).reverse))
wenzelm@65105
    31
  }
wenzelm@65105
    32
wenzelm@65176
    33
  private val background_colors =
wenzelm@65176
    34
    Rendering.Color.background_colors - Rendering.Color.active - Rendering.Color.active_result -
wenzelm@65176
    35
      Rendering.Color.entity
wenzelm@65176
    36
wenzelm@65122
    37
  private val dotted_colors =
wenzelm@65134
    38
    Set(Rendering.Color.writeln, Rendering.Color.information, Rendering.Color.warning)
wenzelm@65122
    39
wenzelm@65105
    40
wenzelm@64679
    41
  /* diagnostic messages */
wenzelm@64679
    42
wenzelm@64679
    43
  private val message_severity =
wenzelm@64679
    44
    Map(
wenzelm@64679
    45
      Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning,
wenzelm@65095
    46
      Markup.ERROR -> Protocol.DiagnosticSeverity.Error)
wenzelm@64679
    47
wenzelm@64679
    48
wenzelm@64679
    49
  /* markup elements */
wenzelm@64679
    50
wenzelm@64679
    51
  private val diagnostics_elements =
wenzelm@65134
    52
    Markup.Elements(Markup.LEGACY, Markup.ERROR)
wenzelm@65095
    53
wenzelm@65176
    54
  private val background_elements =
wenzelm@65176
    55
    Rendering.background_elements - Markup.ENTITY -- Rendering.active_elements
wenzelm@65176
    56
wenzelm@65122
    57
  private val dotted_elements =
wenzelm@65134
    58
    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING)
wenzelm@65122
    59
wenzelm@65134
    60
  val tooltip_elements =
wenzelm@65134
    61
    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.BAD) ++
wenzelm@65134
    62
    Rendering.tooltip_elements
wenzelm@64679
    63
wenzelm@64648
    64
  private val hyperlink_elements =
wenzelm@64833
    65
    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION)
wenzelm@64648
    66
}
wenzelm@64623
    67
wenzelm@66114
    68
class VSCode_Rendering(snapshot: Document.Snapshot, _model: Document_Model)
wenzelm@66114
    69
  extends Rendering(snapshot, _model.resources.options, _model.session)
wenzelm@64623
    70
{
wenzelm@66054
    71
  rendering =>
wenzelm@66054
    72
wenzelm@66114
    73
  def model: Document_Model = _model
wenzelm@66143
    74
  def resources: VSCode_Resources = model.resources
wenzelm@66114
    75
wenzelm@66054
    76
wenzelm@66152
    77
  /* bibtex */
wenzelm@66152
    78
wenzelm@66152
    79
  def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
wenzelm@66152
    80
    Bibtex.entries_iterator(resources.get_models)
wenzelm@66152
    81
wenzelm@66152
    82
  def bibtex_completion(history: Completion.History, caret: Text.Offset): Option[Completion.Result] =
wenzelm@66152
    83
    Bibtex.completion(history, rendering, caret, resources.get_models)
wenzelm@66152
    84
wenzelm@66152
    85
wenzelm@64877
    86
  /* completion */
wenzelm@64877
    87
wenzelm@66054
    88
  def completion(caret_pos: Line.Position, caret: Text.Offset): List[Protocol.CompletionItem] =
wenzelm@66054
    89
  {
wenzelm@66054
    90
    val doc = model.content.doc
wenzelm@66057
    91
    val line = caret_pos.line
wenzelm@66057
    92
    doc.offset(Line.Position(line)) match {
wenzelm@66057
    93
      case None => Nil
wenzelm@66057
    94
      case Some(line_start) =>
wenzelm@66057
    95
        val history = Completion.History.empty
wenzelm@66057
    96
        val caret_range = before_caret_range(caret)
wenzelm@66054
    97
wenzelm@66057
    98
        val syntax = model.syntax()
wenzelm@66057
    99
        val syntax_completion =
wenzelm@67005
   100
          syntax.complete(history, unicode = false, explicit = true,
wenzelm@66057
   101
            line_start, doc.lines(line).text, caret - line_start,
wenzelm@66057
   102
            language_context(caret_range) getOrElse syntax.language_context)
wenzelm@64877
   103
wenzelm@66057
   104
        val (no_completion, semantic_completion) =
wenzelm@66057
   105
          rendering.semantic_completion_result(
wenzelm@66114
   106
            history, false, syntax_completion.map(_.range), caret_range)
wenzelm@66054
   107
wenzelm@66057
   108
        if (no_completion) Nil
wenzelm@66057
   109
        else {
wenzelm@66121
   110
          val results =
wenzelm@66157
   111
            Completion.Result.merge(history,
wenzelm@66151
   112
              semantic_completion,
wenzelm@66151
   113
              syntax_completion,
wenzelm@66153
   114
              VSCode_Spell_Checker.completion(rendering, caret),
wenzelm@66159
   115
              path_completion(caret),
wenzelm@66153
   116
              bibtex_completion(history, caret))
wenzelm@66142
   117
          val items =
wenzelm@66142
   118
            results match {
wenzelm@66142
   119
              case None => Nil
wenzelm@66142
   120
              case Some(result) =>
wenzelm@66142
   121
                result.items.map(item =>
wenzelm@66142
   122
                  Protocol.CompletionItem(
wenzelm@66142
   123
                    label = item.replacement,
wenzelm@66142
   124
                    detail = Some(item.description.mkString(" ")),
wenzelm@66142
   125
                    range = Some(doc.range(item.range))))
wenzelm@66142
   126
            }
wenzelm@66142
   127
          items ::: VSCode_Spell_Checker.menu_items(rendering, caret)
wenzelm@66057
   128
        }
wenzelm@66054
   129
    }
wenzelm@66054
   130
  }
wenzelm@66054
   131
wenzelm@64877
   132
wenzelm@64679
   133
  /* diagnostics */
wenzelm@64679
   134
wenzelm@64679
   135
  def diagnostics: List[Text.Info[Command.Results]] =
wenzelm@64679
   136
    snapshot.cumulate[Command.Results](
wenzelm@67824
   137
      model.content.text_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements,
wenzelm@67824
   138
        command_states =>
wenzelm@67824
   139
          {
wenzelm@67824
   140
            case (res, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, Markup.Serial(i)), body)))
wenzelm@67824
   141
            if body.nonEmpty => Some(res + (i -> msg))
wenzelm@64679
   142
wenzelm@67824
   143
            case (res, Text.Info(_, msg)) =>
wenzelm@67824
   144
              Command.State.get_result_proper(command_states, msg.markup.properties).map(res + _)
wenzelm@67824
   145
wenzelm@67824
   146
            case _ => None
wenzelm@67824
   147
          }).filterNot(info => info.info.is_empty)
wenzelm@64679
   148
wenzelm@64679
   149
  def diagnostics_output(results: List[Text.Info[Command.Results]]): List[Protocol.Diagnostic] =
wenzelm@64679
   150
  {
wenzelm@64679
   151
    (for {
wenzelm@64679
   152
      Text.Info(text_range, res) <- results.iterator
wenzelm@64830
   153
      range = model.content.doc.range(text_range)
wenzelm@64679
   154
      (_, XML.Elem(Markup(name, _), body)) <- res.iterator
wenzelm@64679
   155
    } yield {
wenzelm@66143
   156
      val message = resources.output_pretty_message(body)
wenzelm@64679
   157
      val severity = VSCode_Rendering.message_severity.get(name)
wenzelm@64679
   158
      Protocol.Diagnostic(range, message, severity = severity)
wenzelm@64679
   159
    }).toList
wenzelm@64679
   160
  }
wenzelm@64679
   161
wenzelm@64679
   162
wenzelm@65146
   163
  /* text color */
wenzelm@65146
   164
wenzelm@65146
   165
  def text_color(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
wenzelm@65146
   166
  {
wenzelm@65146
   167
    snapshot.select(range, Rendering.text_color_elements, _ =>
wenzelm@65146
   168
      {
wenzelm@65174
   169
        case Text.Info(_, XML.Elem(Markup(name, props), _)) =>
wenzelm@65174
   170
          if (name != Markup.IMPROPER && props.contains((Markup.KIND, Markup.COMMAND))) None
wenzelm@65174
   171
          else Rendering.text_color.get(name)
wenzelm@65146
   172
      })
wenzelm@65146
   173
  }
wenzelm@65146
   174
wenzelm@65146
   175
wenzelm@65913
   176
  /* text overview color */
wenzelm@65913
   177
wenzelm@65913
   178
  private sealed case class Color_Info(
wenzelm@65913
   179
    color: Rendering.Color.Value, offset: Text.Offset, end_offset: Text.Offset, end_line: Int)
wenzelm@65913
   180
wenzelm@65913
   181
  def text_overview_color: List[Text.Info[Rendering.Color.Value]] =
wenzelm@65913
   182
  {
wenzelm@65913
   183
    @tailrec def loop(offset: Text.Offset, line: Int, lines: List[Line], colors: List[Color_Info])
wenzelm@65913
   184
      : List[Text.Info[Rendering.Color.Value]] =
wenzelm@65913
   185
    {
wenzelm@65913
   186
      if (lines.nonEmpty) {
wenzelm@65913
   187
        val end_offset = offset + lines.head.text.length
wenzelm@65913
   188
        val colors1 =
wenzelm@65913
   189
          (overview_color(Text.Range(offset, end_offset)), colors) match {
wenzelm@65913
   190
            case (Some(color), old :: rest) if color == old.color && line == old.end_line =>
wenzelm@65913
   191
              old.copy(end_offset = end_offset, end_line = line + 1) :: rest
wenzelm@65913
   192
            case (Some(color), _) =>
wenzelm@65913
   193
              Color_Info(color, offset, end_offset, line + 1) :: colors
wenzelm@65913
   194
            case (None, _) => colors
wenzelm@65913
   195
          }
wenzelm@65913
   196
        loop(end_offset + 1, line + 1, lines.tail, colors1)
wenzelm@65913
   197
      }
wenzelm@65913
   198
      else {
wenzelm@65913
   199
        colors.reverse.map(info =>
wenzelm@65913
   200
          Text.Info(Text.Range(info.offset, info.end_offset), info.color))
wenzelm@65913
   201
      }
wenzelm@65913
   202
    }
wenzelm@65913
   203
    loop(0, 0, model.content.doc.lines, Nil)
wenzelm@65913
   204
  }
wenzelm@65913
   205
wenzelm@65913
   206
wenzelm@65122
   207
  /* dotted underline */
wenzelm@65122
   208
wenzelm@65122
   209
  def dotted(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
wenzelm@65122
   210
    message_underline_color(VSCode_Rendering.dotted_elements, range)
wenzelm@65122
   211
wenzelm@65122
   212
wenzelm@65095
   213
  /* decorations */
wenzelm@65095
   214
wenzelm@65120
   215
  def decorations: List[Document_Model.Decoration] = // list of canonical length and order
wenzelm@65925
   216
    Par_List.map((f: () => List[Document_Model.Decoration]) => f(),
wenzelm@65925
   217
      List(
wenzelm@65925
   218
        () =>
wenzelm@65925
   219
          VSCode_Rendering.color_decorations("background_", VSCode_Rendering.background_colors,
wenzelm@65925
   220
            background(VSCode_Rendering.background_elements, model.content.text_range, Set.empty)),
wenzelm@65925
   221
        () =>
wenzelm@65925
   222
          VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors,
wenzelm@65925
   223
            foreground(model.content.text_range)),
wenzelm@65925
   224
        () =>
wenzelm@65925
   225
          VSCode_Rendering.color_decorations("text_", Rendering.Color.text_colors,
wenzelm@65925
   226
            text_color(model.content.text_range)),
wenzelm@65925
   227
        () =>
wenzelm@65925
   228
          VSCode_Rendering.color_decorations("text_overview_", Rendering.Color.text_overview_colors,
wenzelm@65925
   229
            text_overview_color),
wenzelm@65925
   230
        () =>
wenzelm@65925
   231
          VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors,
wenzelm@65925
   232
            dotted(model.content.text_range)))).flatten :::
wenzelm@66141
   233
    List(VSCode_Spell_Checker.decoration(rendering))
wenzelm@65095
   234
wenzelm@65095
   235
  def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration =
wenzelm@65095
   236
  {
wenzelm@65095
   237
    val content =
wenzelm@65106
   238
      for (Text.Info(text_range, msgs) <- decoration.content)
wenzelm@65095
   239
      yield {
wenzelm@65095
   240
        val range = model.content.doc.range(text_range)
wenzelm@65173
   241
        Protocol.DecorationOpts(range,
wenzelm@66143
   242
          msgs.map(msg => Protocol.MarkedString(resources.output_pretty_tooltip(msg))))
wenzelm@65095
   243
      }
wenzelm@65095
   244
    Protocol.Decoration(decoration.typ, content)
wenzelm@65095
   245
  }
wenzelm@65095
   246
wenzelm@65095
   247
wenzelm@64623
   248
  /* tooltips */
wenzelm@64623
   249
wenzelm@70079
   250
  override def timing_threshold: Double = options.real("vscode_timing_threshold")
wenzelm@64648
   251
wenzelm@64648
   252
wenzelm@64648
   253
  /* hyperlinks */
wenzelm@64648
   254
wenzelm@64667
   255
  def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range)
wenzelm@64667
   256
    : Option[Line.Node_Range] =
wenzelm@64667
   257
  {
wenzelm@64775
   258
    for {
wenzelm@66143
   259
      platform_path <- resources.source_file(source_name)
wenzelm@64778
   260
      file <-
wenzelm@66235
   261
        (try { Some(File.absolute(new JFile(platform_path))) }
wenzelm@64778
   262
         catch { case ERROR(_) => None })
wenzelm@64775
   263
    }
wenzelm@64667
   264
    yield {
wenzelm@64778
   265
      Line.Node_Range(file.getPath,
wenzelm@64841
   266
        if (range.start > 0) {
wenzelm@69261
   267
          resources.get_file_content(resources.node_name(file)) match {
wenzelm@64841
   268
            case Some(text) =>
wenzelm@64841
   269
              val chunk = Symbol.Text_Chunk(text)
wenzelm@65196
   270
              val doc = Line.Document(text)
wenzelm@64841
   271
              doc.range(chunk.decode(range))
wenzelm@64841
   272
            case _ =>
wenzelm@64841
   273
              Line.Range(Line.Position((line1 - 1) max 0))
wenzelm@64841
   274
          }
wenzelm@64841
   275
        }
wenzelm@64841
   276
        else Line.Range(Line.Position((line1 - 1) max 0)))
wenzelm@64667
   277
    }
wenzelm@64667
   278
  }
wenzelm@64667
   279
wenzelm@64667
   280
  def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] =
wenzelm@64667
   281
  {
wenzelm@64667
   282
    if (snapshot.is_outdated) None
wenzelm@64667
   283
    else
wenzelm@64667
   284
      for {
wenzelm@64667
   285
        start <- snapshot.find_command_position(id, range.start)
wenzelm@64667
   286
        stop <- snapshot.find_command_position(id, range.stop)
wenzelm@64667
   287
      } yield Line.Node_Range(start.name, Line.Range(start.pos, stop.pos))
wenzelm@64667
   288
  }
wenzelm@64667
   289
wenzelm@64667
   290
  def hyperlink_position(pos: Position.T): Option[Line.Node_Range] =
wenzelm@64667
   291
    pos match {
wenzelm@64667
   292
      case Position.Item_File(name, line, range) => hyperlink_source_file(name, line, range)
wenzelm@64667
   293
      case Position.Item_Id(id, range) => hyperlink_command(id, range)
wenzelm@64667
   294
      case _ => None
wenzelm@64667
   295
    }
wenzelm@64667
   296
wenzelm@64667
   297
  def hyperlink_def_position(pos: Position.T): Option[Line.Node_Range] =
wenzelm@64667
   298
    pos match {
wenzelm@64667
   299
      case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range)
wenzelm@64667
   300
      case Position.Item_Def_Id(id, range) => hyperlink_command(id, range)
wenzelm@64667
   301
      case _ => None
wenzelm@64667
   302
    }
wenzelm@64667
   303
wenzelm@64651
   304
  def hyperlinks(range: Text.Range): List[Line.Node_Range] =
wenzelm@64648
   305
  {
wenzelm@64651
   306
    snapshot.cumulate[List[Line.Node_Range]](
wenzelm@64648
   307
      range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
wenzelm@64648
   308
        {
wenzelm@64648
   309
          case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
wenzelm@65488
   310
            val file = perhaps_append_file(snapshot.node_name, name)
wenzelm@64654
   311
            Some(Line.Node_Range(file) :: links)
wenzelm@64648
   312
wenzelm@64667
   313
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
wenzelm@64667
   314
            hyperlink_def_position(props).map(_ :: links)
wenzelm@64667
   315
wenzelm@64667
   316
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
wenzelm@64667
   317
            hyperlink_position(props).map(_ :: links)
wenzelm@64648
   318
wenzelm@64833
   319
          case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
wenzelm@64833
   320
            val iterator =
wenzelm@64833
   321
              for {
wenzelm@66152
   322
                Text.Info(entry_range, (entry, model)) <- bibtex_entries_iterator()
wenzelm@64833
   323
                if entry == name
wenzelm@64833
   324
              } yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range))
wenzelm@64833
   325
            if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _))
wenzelm@64833
   326
wenzelm@64648
   327
          case _ => None
wenzelm@64648
   328
        }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
wenzelm@64648
   329
  }
wenzelm@64623
   330
}