src/Tools/VSCode/src/vscode_rendering.scala
author wenzelm
Fri Mar 10 21:47:48 2017 +0100 (2017-03-10)
changeset 65176 908d8be90533
parent 65174 c0388fbd8096
child 65196 e8760a98db78
permissions -rw-r--r--
suppress irrelevant markup for VSCode;
wenzelm@64622
     1
/*  Title:      Tools/VSCode/src/vscode_rendering.scala
wenzelm@64622
     2
    Author:     Makarius
wenzelm@64622
     3
wenzelm@64622
     4
Isabelle/VSCode-specific implementation of quasi-abstract rendering and
wenzelm@64622
     5
markup interpretation.
wenzelm@64622
     6
*/
wenzelm@64622
     7
wenzelm@64622
     8
package isabelle.vscode
wenzelm@64622
     9
wenzelm@64622
    10
wenzelm@64622
    11
import isabelle._
wenzelm@64622
    12
wenzelm@64778
    13
import java.io.{File => JFile}
wenzelm@64778
    14
wenzelm@64778
    15
wenzelm@64648
    16
object VSCode_Rendering
wenzelm@64648
    17
{
wenzelm@65104
    18
  /* decorations */
wenzelm@65104
    19
wenzelm@65122
    20
  private def color_decorations(prefix: String, types: Set[Rendering.Color.Value],
wenzelm@65104
    21
    colors: List[Text.Info[Rendering.Color.Value]]): List[Document_Model.Decoration] =
wenzelm@65104
    22
  {
wenzelm@65104
    23
    val color_ranges =
wenzelm@65104
    24
      (Map.empty[Rendering.Color.Value, List[Text.Range]] /: colors) {
wenzelm@65104
    25
        case (m, Text.Info(range, c)) => m + (c -> (range :: m.getOrElse(c, Nil)))
wenzelm@65104
    26
      }
wenzelm@65105
    27
    types.toList.map(c =>
wenzelm@65140
    28
      Document_Model.Decoration.ranges(prefix + c.toString, color_ranges.getOrElse(c, Nil).reverse))
wenzelm@65104
    29
  }
wenzelm@65104
    30
wenzelm@65176
    31
  private val background_colors =
wenzelm@65176
    32
    Rendering.Color.background_colors - Rendering.Color.active - Rendering.Color.active_result -
wenzelm@65176
    33
      Rendering.Color.entity
wenzelm@65176
    34
wenzelm@65122
    35
  private val dotted_colors =
wenzelm@65134
    36
    Set(Rendering.Color.writeln, Rendering.Color.information, Rendering.Color.warning)
wenzelm@65122
    37
wenzelm@65104
    38
wenzelm@64679
    39
  /* diagnostic messages */
wenzelm@64679
    40
wenzelm@64679
    41
  private val message_severity =
wenzelm@64679
    42
    Map(
wenzelm@64679
    43
      Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning,
wenzelm@65095
    44
      Markup.ERROR -> Protocol.DiagnosticSeverity.Error)
wenzelm@64679
    45
wenzelm@64679
    46
wenzelm@64679
    47
  /* markup elements */
wenzelm@64679
    48
wenzelm@64679
    49
  private val diagnostics_elements =
wenzelm@65134
    50
    Markup.Elements(Markup.LEGACY, Markup.ERROR)
wenzelm@65095
    51
wenzelm@65176
    52
  private val background_elements =
wenzelm@65176
    53
    Rendering.background_elements - Markup.ENTITY -- Rendering.active_elements
wenzelm@65176
    54
wenzelm@65122
    55
  private val dotted_elements =
wenzelm@65134
    56
    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING)
wenzelm@65122
    57
wenzelm@65134
    58
  val tooltip_elements =
wenzelm@65134
    59
    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.BAD) ++
wenzelm@65134
    60
    Rendering.tooltip_elements
wenzelm@64679
    61
wenzelm@64648
    62
  private val hyperlink_elements =
wenzelm@64833
    63
    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION)
wenzelm@64648
    64
}
wenzelm@64622
    65
wenzelm@64649
    66
class VSCode_Rendering(
wenzelm@64649
    67
    val model: Document_Model,
wenzelm@64649
    68
    snapshot: Document.Snapshot,
wenzelm@64702
    69
    resources: VSCode_Resources)
wenzelm@64704
    70
  extends Rendering(snapshot, resources.options, resources)
wenzelm@64622
    71
{
wenzelm@64877
    72
  /* completion */
wenzelm@64877
    73
wenzelm@64877
    74
  def completion(range: Text.Range): List[Protocol.CompletionItem] =
wenzelm@64877
    75
    semantic_completion(None, range) match {
wenzelm@64877
    76
      case Some(Text.Info(complete_range, names: Completion.Names)) =>
wenzelm@64877
    77
        model.content.try_get_text(complete_range) match {
wenzelm@64877
    78
          case Some(original) =>
wenzelm@64877
    79
            names.complete(complete_range, Completion.History.empty,
wenzelm@65137
    80
                resources.unicode_symbols, original) match {
wenzelm@64877
    81
              case Some(result) =>
wenzelm@64877
    82
                result.items.map(item =>
wenzelm@64877
    83
                  Protocol.CompletionItem(
wenzelm@64877
    84
                    label = item.replacement,
wenzelm@64877
    85
                    detail = Some(item.description.mkString(" ")),
wenzelm@64877
    86
                    range = Some(model.content.doc.range(item.range))))
wenzelm@64877
    87
              case None => Nil
wenzelm@64877
    88
            }
wenzelm@64877
    89
          case None => Nil
wenzelm@64877
    90
        }
wenzelm@64877
    91
      case _ => Nil
wenzelm@64877
    92
    }
wenzelm@64877
    93
wenzelm@64877
    94
wenzelm@64679
    95
  /* diagnostics */
wenzelm@64679
    96
wenzelm@64679
    97
  def diagnostics: List[Text.Info[Command.Results]] =
wenzelm@64679
    98
    snapshot.cumulate[Command.Results](
wenzelm@64830
    99
      model.content.text_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ =>
wenzelm@64679
   100
      {
wenzelm@64679
   101
        case (res, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(i)), body)))
wenzelm@64679
   102
        if body.nonEmpty => Some(res + (i -> msg))
wenzelm@64679
   103
wenzelm@64679
   104
        case _ => None
wenzelm@64802
   105
      }).filterNot(info => info.info.is_empty)
wenzelm@64679
   106
wenzelm@64679
   107
  def diagnostics_output(results: List[Text.Info[Command.Results]]): List[Protocol.Diagnostic] =
wenzelm@64679
   108
  {
wenzelm@64679
   109
    (for {
wenzelm@64679
   110
      Text.Info(text_range, res) <- results.iterator
wenzelm@64830
   111
      range = model.content.doc.range(text_range)
wenzelm@64679
   112
      (_, XML.Elem(Markup(name, _), body)) <- res.iterator
wenzelm@64679
   113
    } yield {
wenzelm@65107
   114
      val message = resources.output_pretty_message(body)
wenzelm@64679
   115
      val severity = VSCode_Rendering.message_severity.get(name)
wenzelm@64679
   116
      Protocol.Diagnostic(range, message, severity = severity)
wenzelm@64679
   117
    }).toList
wenzelm@64679
   118
  }
wenzelm@64679
   119
wenzelm@64679
   120
wenzelm@65146
   121
  /* text color */
wenzelm@65146
   122
wenzelm@65146
   123
  def text_color(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
wenzelm@65146
   124
  {
wenzelm@65146
   125
    snapshot.select(range, Rendering.text_color_elements, _ =>
wenzelm@65146
   126
      {
wenzelm@65174
   127
        case Text.Info(_, XML.Elem(Markup(name, props), _)) =>
wenzelm@65174
   128
          if (name != Markup.IMPROPER && props.contains((Markup.KIND, Markup.COMMAND))) None
wenzelm@65174
   129
          else Rendering.text_color.get(name)
wenzelm@65146
   130
      })
wenzelm@65146
   131
  }
wenzelm@65146
   132
wenzelm@65146
   133
wenzelm@65122
   134
  /* dotted underline */
wenzelm@65122
   135
wenzelm@65122
   136
  def dotted(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
wenzelm@65122
   137
    message_underline_color(VSCode_Rendering.dotted_elements, range)
wenzelm@65122
   138
wenzelm@65122
   139
wenzelm@65142
   140
  /* spell checker */
wenzelm@65142
   141
wenzelm@65142
   142
  def spell_checker: Document_Model.Decoration =
wenzelm@65142
   143
  {
wenzelm@65142
   144
    val ranges =
wenzelm@65142
   145
      (for {
wenzelm@65142
   146
        spell_checker <- resources.spell_checker.get.iterator
wenzelm@65142
   147
        spell_range <- spell_checker_ranges(model.content.text_range).iterator
wenzelm@65142
   148
        text <- model.content.try_get_text(spell_range).iterator
wenzelm@65142
   149
        info <- spell_checker.marked_words(spell_range.start, text).iterator
wenzelm@65142
   150
      } yield info.range).toList
wenzelm@65142
   151
    Document_Model.Decoration.ranges("spell_checker", ranges)
wenzelm@65142
   152
  }
wenzelm@65142
   153
wenzelm@65142
   154
wenzelm@65095
   155
  /* decorations */
wenzelm@65095
   156
wenzelm@65120
   157
  def decorations: List[Document_Model.Decoration] = // list of canonical length and order
wenzelm@65176
   158
    VSCode_Rendering.color_decorations("background_", VSCode_Rendering.background_colors,
wenzelm@65176
   159
      background(VSCode_Rendering.background_elements, model.content.text_range, Set.empty)) :::
wenzelm@65143
   160
    VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground_colors,
wenzelm@65122
   161
      foreground(model.content.text_range)) :::
wenzelm@65146
   162
    VSCode_Rendering.color_decorations("text_", Rendering.Color.text_colors,
wenzelm@65146
   163
      text_color(model.content.text_range)) :::
wenzelm@65122
   164
    VSCode_Rendering.color_decorations("dotted_", VSCode_Rendering.dotted_colors,
wenzelm@65142
   165
      dotted(model.content.text_range)) :::
wenzelm@65142
   166
    List(spell_checker)
wenzelm@65095
   167
wenzelm@65095
   168
  def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration =
wenzelm@65095
   169
  {
wenzelm@65095
   170
    val content =
wenzelm@65105
   171
      for (Text.Info(text_range, msgs) <- decoration.content)
wenzelm@65095
   172
      yield {
wenzelm@65095
   173
        val range = model.content.doc.range(text_range)
wenzelm@65173
   174
        Protocol.DecorationOpts(range,
wenzelm@65107
   175
          msgs.map(msg => Protocol.MarkedString(resources.output_pretty_tooltip(msg))))
wenzelm@65095
   176
      }
wenzelm@65095
   177
    Protocol.Decoration(decoration.typ, content)
wenzelm@65095
   178
  }
wenzelm@65095
   179
wenzelm@65095
   180
wenzelm@64622
   181
  /* tooltips */
wenzelm@64622
   182
wenzelm@64622
   183
  def timing_threshold: Double = options.real("vscode_timing_threshold")
wenzelm@64648
   184
wenzelm@64648
   185
wenzelm@64648
   186
  /* hyperlinks */
wenzelm@64648
   187
wenzelm@64667
   188
  def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range)
wenzelm@64667
   189
    : Option[Line.Node_Range] =
wenzelm@64667
   190
  {
wenzelm@64775
   191
    for {
wenzelm@64779
   192
      platform_path <- resources.source_file(source_name)
wenzelm@64778
   193
      file <-
wenzelm@64779
   194
        (try { Some(new JFile(platform_path).getCanonicalFile) }
wenzelm@64778
   195
         catch { case ERROR(_) => None })
wenzelm@64775
   196
    }
wenzelm@64667
   197
    yield {
wenzelm@64778
   198
      Line.Node_Range(file.getPath,
wenzelm@64841
   199
        if (range.start > 0) {
wenzelm@64841
   200
          resources.get_file_content(file) match {
wenzelm@64841
   201
            case Some(text) =>
wenzelm@64841
   202
              val chunk = Symbol.Text_Chunk(text)
wenzelm@64841
   203
              val doc = Line.Document(text, resources.text_length)
wenzelm@64841
   204
              doc.range(chunk.decode(range))
wenzelm@64841
   205
            case _ =>
wenzelm@64841
   206
              Line.Range(Line.Position((line1 - 1) max 0))
wenzelm@64841
   207
          }
wenzelm@64841
   208
        }
wenzelm@64841
   209
        else Line.Range(Line.Position((line1 - 1) max 0)))
wenzelm@64667
   210
    }
wenzelm@64667
   211
  }
wenzelm@64667
   212
wenzelm@64667
   213
  def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] =
wenzelm@64667
   214
  {
wenzelm@64667
   215
    if (snapshot.is_outdated) None
wenzelm@64667
   216
    else
wenzelm@64667
   217
      for {
wenzelm@64667
   218
        start <- snapshot.find_command_position(id, range.start)
wenzelm@64667
   219
        stop <- snapshot.find_command_position(id, range.stop)
wenzelm@64667
   220
      } yield Line.Node_Range(start.name, Line.Range(start.pos, stop.pos))
wenzelm@64667
   221
  }
wenzelm@64667
   222
wenzelm@64667
   223
  def hyperlink_position(pos: Position.T): Option[Line.Node_Range] =
wenzelm@64667
   224
    pos match {
wenzelm@64667
   225
      case Position.Item_File(name, line, range) => hyperlink_source_file(name, line, range)
wenzelm@64667
   226
      case Position.Item_Id(id, range) => hyperlink_command(id, range)
wenzelm@64667
   227
      case _ => None
wenzelm@64667
   228
    }
wenzelm@64667
   229
wenzelm@64667
   230
  def hyperlink_def_position(pos: Position.T): Option[Line.Node_Range] =
wenzelm@64667
   231
    pos match {
wenzelm@64667
   232
      case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range)
wenzelm@64667
   233
      case Position.Item_Def_Id(id, range) => hyperlink_command(id, range)
wenzelm@64667
   234
      case _ => None
wenzelm@64667
   235
    }
wenzelm@64667
   236
wenzelm@64651
   237
  def hyperlinks(range: Text.Range): List[Line.Node_Range] =
wenzelm@64648
   238
  {
wenzelm@64651
   239
    snapshot.cumulate[List[Line.Node_Range]](
wenzelm@64648
   240
      range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
wenzelm@64648
   241
        {
wenzelm@64648
   242
          case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
wenzelm@64759
   243
            val file = resources.append_file(snapshot.node_name.master_dir, name)
wenzelm@64654
   244
            Some(Line.Node_Range(file) :: links)
wenzelm@64648
   245
wenzelm@64667
   246
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
wenzelm@64667
   247
            hyperlink_def_position(props).map(_ :: links)
wenzelm@64667
   248
wenzelm@64667
   249
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
wenzelm@64667
   250
            hyperlink_position(props).map(_ :: links)
wenzelm@64648
   251
wenzelm@64833
   252
          case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
wenzelm@64833
   253
            val iterator =
wenzelm@64833
   254
              for {
wenzelm@64833
   255
                Text.Info(entry_range, (entry, model)) <- resources.bibtex_entries_iterator
wenzelm@64833
   256
                if entry == name
wenzelm@64833
   257
              } yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range))
wenzelm@64833
   258
            if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _))
wenzelm@64833
   259
wenzelm@64648
   260
          case _ => None
wenzelm@64648
   261
        }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
wenzelm@64648
   262
  }
wenzelm@64622
   263
}