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