src/Tools/VSCode/src/vscode_rendering.scala
author wenzelm
Sat Mar 04 13:36:06 2017 +0100 (2017-03-04)
changeset 65104 66b19d05dcee
parent 65095 eb21a4f70b0e
child 65105 1f47b92021de
permissions -rw-r--r--
decorations for background and foreground colors;
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@65104
    20
  def color_decorations(prefix: String, types: Rendering.Color.ValueSet,
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@65104
    27
    for (c <- types.toList)
wenzelm@65104
    28
    yield {
wenzelm@65104
    29
      val typ = prefix + c.toString
wenzelm@65104
    30
      val content =
wenzelm@65104
    31
        color_ranges.getOrElse(c, Nil).reverse.map(r => Text.Info(r, Nil: XML.Body))
wenzelm@65104
    32
      Document_Model.Decoration(typ, content)
wenzelm@65104
    33
    }
wenzelm@65104
    34
  }
wenzelm@65104
    35
wenzelm@65104
    36
wenzelm@64679
    37
  /* diagnostic messages */
wenzelm@64679
    38
wenzelm@64679
    39
  private val message_severity =
wenzelm@64679
    40
    Map(
wenzelm@64762
    41
      Markup.WRITELN -> Protocol.DiagnosticSeverity.Information,
wenzelm@64679
    42
      Markup.INFORMATION -> Protocol.DiagnosticSeverity.Information,
wenzelm@64679
    43
      Markup.WARNING -> Protocol.DiagnosticSeverity.Warning,
wenzelm@64679
    44
      Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning,
wenzelm@65095
    45
      Markup.ERROR -> Protocol.DiagnosticSeverity.Error)
wenzelm@64679
    46
wenzelm@64679
    47
wenzelm@64679
    48
  /* markup elements */
wenzelm@64679
    49
wenzelm@64679
    50
  private val diagnostics_elements =
wenzelm@65095
    51
    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
wenzelm@65095
    52
wenzelm@65095
    53
  private val bad_elements = Markup.Elements(Markup.BAD)
wenzelm@64679
    54
wenzelm@64648
    55
  private val hyperlink_elements =
wenzelm@64833
    56
    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION)
wenzelm@64648
    57
}
wenzelm@64622
    58
wenzelm@64649
    59
class VSCode_Rendering(
wenzelm@64649
    60
    val model: Document_Model,
wenzelm@64649
    61
    snapshot: Document.Snapshot,
wenzelm@64702
    62
    resources: VSCode_Resources)
wenzelm@64704
    63
  extends Rendering(snapshot, resources.options, resources)
wenzelm@64622
    64
{
wenzelm@64877
    65
  /* completion */
wenzelm@64877
    66
wenzelm@64877
    67
  def completion(range: Text.Range): List[Protocol.CompletionItem] =
wenzelm@64877
    68
    semantic_completion(None, range) match {
wenzelm@64877
    69
      case Some(Text.Info(complete_range, names: Completion.Names)) =>
wenzelm@64877
    70
        model.content.try_get_text(complete_range) match {
wenzelm@64877
    71
          case Some(original) =>
wenzelm@64877
    72
            names.complete(complete_range, Completion.History.empty,
wenzelm@64877
    73
                resources.decode_text, original) match {
wenzelm@64877
    74
              case Some(result) =>
wenzelm@64877
    75
                result.items.map(item =>
wenzelm@64877
    76
                  Protocol.CompletionItem(
wenzelm@64877
    77
                    label = item.replacement,
wenzelm@64877
    78
                    detail = Some(item.description.mkString(" ")),
wenzelm@64877
    79
                    range = Some(model.content.doc.range(item.range))))
wenzelm@64877
    80
              case None => Nil
wenzelm@64877
    81
            }
wenzelm@64877
    82
          case None => Nil
wenzelm@64877
    83
        }
wenzelm@64877
    84
      case _ => Nil
wenzelm@64877
    85
    }
wenzelm@64877
    86
wenzelm@64877
    87
wenzelm@64679
    88
  /* diagnostics */
wenzelm@64679
    89
wenzelm@64679
    90
  def diagnostics: List[Text.Info[Command.Results]] =
wenzelm@64679
    91
    snapshot.cumulate[Command.Results](
wenzelm@64830
    92
      model.content.text_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ =>
wenzelm@64679
    93
      {
wenzelm@64679
    94
        case (res, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(i)), body)))
wenzelm@64679
    95
        if body.nonEmpty => Some(res + (i -> msg))
wenzelm@64679
    96
wenzelm@64679
    97
        case _ => None
wenzelm@64802
    98
      }).filterNot(info => info.info.is_empty)
wenzelm@64679
    99
wenzelm@64679
   100
  val diagnostics_margin = options.int("vscode_diagnostics_margin")
wenzelm@64679
   101
wenzelm@64679
   102
  def diagnostics_output(results: List[Text.Info[Command.Results]]): List[Protocol.Diagnostic] =
wenzelm@64679
   103
  {
wenzelm@64679
   104
    (for {
wenzelm@64679
   105
      Text.Info(text_range, res) <- results.iterator
wenzelm@64830
   106
      range = model.content.doc.range(text_range)
wenzelm@64679
   107
      (_, XML.Elem(Markup(name, _), body)) <- res.iterator
wenzelm@64679
   108
    } yield {
wenzelm@64870
   109
      val message = resources.output_pretty(body, diagnostics_margin)
wenzelm@64679
   110
      val severity = VSCode_Rendering.message_severity.get(name)
wenzelm@64679
   111
      Protocol.Diagnostic(range, message, severity = severity)
wenzelm@64679
   112
    }).toList
wenzelm@64679
   113
  }
wenzelm@64679
   114
wenzelm@64679
   115
wenzelm@65095
   116
  /* decorations */
wenzelm@65095
   117
wenzelm@65095
   118
  def decorations: List[Document_Model.Decoration] =
wenzelm@65104
   119
    decorations_bad :::
wenzelm@65104
   120
    VSCode_Rendering.color_decorations("background_", Rendering.Color.background,
wenzelm@65104
   121
      background(model.content.text_range, Set.empty)) :::
wenzelm@65104
   122
    VSCode_Rendering.color_decorations("foreground_", Rendering.Color.foreground,
wenzelm@65104
   123
      foreground(model.content.text_range))
wenzelm@65095
   124
wenzelm@65104
   125
  def decorations_bad: List[Document_Model.Decoration] =
wenzelm@65104
   126
  {
wenzelm@65104
   127
    val content =
wenzelm@65104
   128
      snapshot.select(model.content.text_range, VSCode_Rendering.bad_elements, _ =>
wenzelm@65104
   129
        {
wenzelm@65104
   130
          case Text.Info(_, XML.Elem(_, body)) => Some(body)
wenzelm@65104
   131
        })
wenzelm@65104
   132
    List(Document_Model.Decoration(Protocol.Decorations.bad, content))
wenzelm@65104
   133
  }
wenzelm@65095
   134
wenzelm@65095
   135
  def decoration_output(decoration: Document_Model.Decoration): Protocol.Decoration =
wenzelm@65095
   136
  {
wenzelm@65095
   137
    val content =
wenzelm@65095
   138
      for (Text.Info(text_range, body) <- decoration.content)
wenzelm@65095
   139
      yield {
wenzelm@65095
   140
        val range = model.content.doc.range(text_range)
wenzelm@65095
   141
        val msg = resources.output_pretty(body, diagnostics_margin)
wenzelm@65095
   142
        Protocol.DecorationOptions(range, if (msg == "") Nil else List(Protocol.MarkedString(msg)))
wenzelm@65095
   143
      }
wenzelm@65095
   144
    Protocol.Decoration(decoration.typ, content)
wenzelm@65095
   145
  }
wenzelm@65095
   146
wenzelm@65095
   147
wenzelm@64622
   148
  /* tooltips */
wenzelm@64622
   149
wenzelm@64622
   150
  def tooltip_margin: Int = options.int("vscode_tooltip_margin")
wenzelm@64622
   151
  def timing_threshold: Double = options.real("vscode_timing_threshold")
wenzelm@64648
   152
wenzelm@64648
   153
wenzelm@64648
   154
  /* hyperlinks */
wenzelm@64648
   155
wenzelm@64667
   156
  def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range)
wenzelm@64667
   157
    : Option[Line.Node_Range] =
wenzelm@64667
   158
  {
wenzelm@64775
   159
    for {
wenzelm@64779
   160
      platform_path <- resources.source_file(source_name)
wenzelm@64778
   161
      file <-
wenzelm@64779
   162
        (try { Some(new JFile(platform_path).getCanonicalFile) }
wenzelm@64778
   163
         catch { case ERROR(_) => None })
wenzelm@64775
   164
    }
wenzelm@64667
   165
    yield {
wenzelm@64778
   166
      Line.Node_Range(file.getPath,
wenzelm@64841
   167
        if (range.start > 0) {
wenzelm@64841
   168
          resources.get_file_content(file) match {
wenzelm@64841
   169
            case Some(text) =>
wenzelm@64841
   170
              val chunk = Symbol.Text_Chunk(text)
wenzelm@64841
   171
              val doc = Line.Document(text, resources.text_length)
wenzelm@64841
   172
              doc.range(chunk.decode(range))
wenzelm@64841
   173
            case _ =>
wenzelm@64841
   174
              Line.Range(Line.Position((line1 - 1) max 0))
wenzelm@64841
   175
          }
wenzelm@64841
   176
        }
wenzelm@64841
   177
        else Line.Range(Line.Position((line1 - 1) max 0)))
wenzelm@64667
   178
    }
wenzelm@64667
   179
  }
wenzelm@64667
   180
wenzelm@64667
   181
  def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] =
wenzelm@64667
   182
  {
wenzelm@64667
   183
    if (snapshot.is_outdated) None
wenzelm@64667
   184
    else
wenzelm@64667
   185
      for {
wenzelm@64667
   186
        start <- snapshot.find_command_position(id, range.start)
wenzelm@64667
   187
        stop <- snapshot.find_command_position(id, range.stop)
wenzelm@64667
   188
      } yield Line.Node_Range(start.name, Line.Range(start.pos, stop.pos))
wenzelm@64667
   189
  }
wenzelm@64667
   190
wenzelm@64667
   191
  def hyperlink_position(pos: Position.T): Option[Line.Node_Range] =
wenzelm@64667
   192
    pos match {
wenzelm@64667
   193
      case Position.Item_File(name, line, range) => hyperlink_source_file(name, line, range)
wenzelm@64667
   194
      case Position.Item_Id(id, range) => hyperlink_command(id, range)
wenzelm@64667
   195
      case _ => None
wenzelm@64667
   196
    }
wenzelm@64667
   197
wenzelm@64667
   198
  def hyperlink_def_position(pos: Position.T): Option[Line.Node_Range] =
wenzelm@64667
   199
    pos match {
wenzelm@64667
   200
      case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range)
wenzelm@64667
   201
      case Position.Item_Def_Id(id, range) => hyperlink_command(id, range)
wenzelm@64667
   202
      case _ => None
wenzelm@64667
   203
    }
wenzelm@64667
   204
wenzelm@64651
   205
  def hyperlinks(range: Text.Range): List[Line.Node_Range] =
wenzelm@64648
   206
  {
wenzelm@64651
   207
    snapshot.cumulate[List[Line.Node_Range]](
wenzelm@64648
   208
      range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
wenzelm@64648
   209
        {
wenzelm@64648
   210
          case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
wenzelm@64759
   211
            val file = resources.append_file(snapshot.node_name.master_dir, name)
wenzelm@64654
   212
            Some(Line.Node_Range(file) :: links)
wenzelm@64648
   213
wenzelm@64667
   214
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
wenzelm@64667
   215
            hyperlink_def_position(props).map(_ :: links)
wenzelm@64667
   216
wenzelm@64667
   217
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
wenzelm@64667
   218
            hyperlink_position(props).map(_ :: links)
wenzelm@64648
   219
wenzelm@64833
   220
          case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
wenzelm@64833
   221
            val iterator =
wenzelm@64833
   222
              for {
wenzelm@64833
   223
                Text.Info(entry_range, (entry, model)) <- resources.bibtex_entries_iterator
wenzelm@64833
   224
                if entry == name
wenzelm@64833
   225
              } yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range))
wenzelm@64833
   226
            if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _))
wenzelm@64833
   227
wenzelm@64648
   228
          case _ => None
wenzelm@64648
   229
        }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
wenzelm@64648
   230
  }
wenzelm@64622
   231
}