src/Tools/VSCode/src/vscode_rendering.scala
author wenzelm
Sun Jan 08 19:08:26 2017 +0100 (2017-01-08)
changeset 64841 d53696aed874
parent 64833 0f410e3b1d20
child 64870 41e2797af496
permissions -rw-r--r--
added node_name(String): imitate jEdit buffer operations;
more uniform get_file_content for external source file references;
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@64679
    26
      Markup.ERROR -> Protocol.DiagnosticSeverity.Error,
wenzelm@64679
    27
      Markup.BAD -> Protocol.DiagnosticSeverity.Error)
wenzelm@64679
    28
wenzelm@64679
    29
wenzelm@64679
    30
  /* markup elements */
wenzelm@64679
    31
wenzelm@64679
    32
  private val diagnostics_elements =
wenzelm@64679
    33
    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
wenzelm@64679
    34
      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@64679
    46
  /* diagnostics */
wenzelm@64679
    47
wenzelm@64679
    48
  def diagnostics: List[Text.Info[Command.Results]] =
wenzelm@64679
    49
    snapshot.cumulate[Command.Results](
wenzelm@64830
    50
      model.content.text_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ =>
wenzelm@64679
    51
      {
wenzelm@64679
    52
        case (res, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(i)), body)))
wenzelm@64679
    53
        if body.nonEmpty => Some(res + (i -> msg))
wenzelm@64679
    54
wenzelm@64679
    55
        case _ => None
wenzelm@64802
    56
      }).filterNot(info => info.info.is_empty)
wenzelm@64679
    57
wenzelm@64679
    58
  val diagnostics_margin = options.int("vscode_diagnostics_margin")
wenzelm@64679
    59
wenzelm@64679
    60
  def diagnostics_output(results: List[Text.Info[Command.Results]]): List[Protocol.Diagnostic] =
wenzelm@64679
    61
  {
wenzelm@64679
    62
    (for {
wenzelm@64679
    63
      Text.Info(text_range, res) <- results.iterator
wenzelm@64830
    64
      range = model.content.doc.range(text_range)
wenzelm@64679
    65
      (_, XML.Elem(Markup(name, _), body)) <- res.iterator
wenzelm@64679
    66
    } yield {
wenzelm@64679
    67
      val message = Pretty.string_of(body, margin = diagnostics_margin)
wenzelm@64679
    68
      val severity = VSCode_Rendering.message_severity.get(name)
wenzelm@64679
    69
      Protocol.Diagnostic(range, message, severity = severity)
wenzelm@64679
    70
    }).toList
wenzelm@64679
    71
  }
wenzelm@64679
    72
wenzelm@64679
    73
wenzelm@64622
    74
  /* tooltips */
wenzelm@64622
    75
wenzelm@64622
    76
  def tooltip_margin: Int = options.int("vscode_tooltip_margin")
wenzelm@64622
    77
  def timing_threshold: Double = options.real("vscode_timing_threshold")
wenzelm@64648
    78
wenzelm@64648
    79
wenzelm@64648
    80
  /* hyperlinks */
wenzelm@64648
    81
wenzelm@64667
    82
  def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range)
wenzelm@64667
    83
    : Option[Line.Node_Range] =
wenzelm@64667
    84
  {
wenzelm@64775
    85
    for {
wenzelm@64779
    86
      platform_path <- resources.source_file(source_name)
wenzelm@64778
    87
      file <-
wenzelm@64779
    88
        (try { Some(new JFile(platform_path).getCanonicalFile) }
wenzelm@64778
    89
         catch { case ERROR(_) => None })
wenzelm@64775
    90
    }
wenzelm@64667
    91
    yield {
wenzelm@64778
    92
      Line.Node_Range(file.getPath,
wenzelm@64841
    93
        if (range.start > 0) {
wenzelm@64841
    94
          resources.get_file_content(file) match {
wenzelm@64841
    95
            case Some(text) =>
wenzelm@64841
    96
              val chunk = Symbol.Text_Chunk(text)
wenzelm@64841
    97
              val doc = Line.Document(text, resources.text_length)
wenzelm@64841
    98
              doc.range(chunk.decode(range))
wenzelm@64841
    99
            case _ =>
wenzelm@64841
   100
              Line.Range(Line.Position((line1 - 1) max 0))
wenzelm@64841
   101
          }
wenzelm@64841
   102
        }
wenzelm@64841
   103
        else Line.Range(Line.Position((line1 - 1) max 0)))
wenzelm@64667
   104
    }
wenzelm@64667
   105
  }
wenzelm@64667
   106
wenzelm@64667
   107
  def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] =
wenzelm@64667
   108
  {
wenzelm@64667
   109
    if (snapshot.is_outdated) None
wenzelm@64667
   110
    else
wenzelm@64667
   111
      for {
wenzelm@64667
   112
        start <- snapshot.find_command_position(id, range.start)
wenzelm@64667
   113
        stop <- snapshot.find_command_position(id, range.stop)
wenzelm@64667
   114
      } yield Line.Node_Range(start.name, Line.Range(start.pos, stop.pos))
wenzelm@64667
   115
  }
wenzelm@64667
   116
wenzelm@64667
   117
  def hyperlink_position(pos: Position.T): Option[Line.Node_Range] =
wenzelm@64667
   118
    pos match {
wenzelm@64667
   119
      case Position.Item_File(name, line, range) => hyperlink_source_file(name, line, range)
wenzelm@64667
   120
      case Position.Item_Id(id, range) => hyperlink_command(id, range)
wenzelm@64667
   121
      case _ => None
wenzelm@64667
   122
    }
wenzelm@64667
   123
wenzelm@64667
   124
  def hyperlink_def_position(pos: Position.T): Option[Line.Node_Range] =
wenzelm@64667
   125
    pos match {
wenzelm@64667
   126
      case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range)
wenzelm@64667
   127
      case Position.Item_Def_Id(id, range) => hyperlink_command(id, range)
wenzelm@64667
   128
      case _ => None
wenzelm@64667
   129
    }
wenzelm@64667
   130
wenzelm@64651
   131
  def hyperlinks(range: Text.Range): List[Line.Node_Range] =
wenzelm@64648
   132
  {
wenzelm@64651
   133
    snapshot.cumulate[List[Line.Node_Range]](
wenzelm@64648
   134
      range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
wenzelm@64648
   135
        {
wenzelm@64648
   136
          case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
wenzelm@64759
   137
            val file = resources.append_file(snapshot.node_name.master_dir, name)
wenzelm@64654
   138
            Some(Line.Node_Range(file) :: links)
wenzelm@64648
   139
wenzelm@64667
   140
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
wenzelm@64667
   141
            hyperlink_def_position(props).map(_ :: links)
wenzelm@64667
   142
wenzelm@64667
   143
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
wenzelm@64667
   144
            hyperlink_position(props).map(_ :: links)
wenzelm@64648
   145
wenzelm@64833
   146
          case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
wenzelm@64833
   147
            val iterator =
wenzelm@64833
   148
              for {
wenzelm@64833
   149
                Text.Info(entry_range, (entry, model)) <- resources.bibtex_entries_iterator
wenzelm@64833
   150
                if entry == name
wenzelm@64833
   151
              } yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range))
wenzelm@64833
   152
            if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _))
wenzelm@64833
   153
wenzelm@64648
   154
          case _ => None
wenzelm@64648
   155
        }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
wenzelm@64648
   156
  }
wenzelm@64622
   157
}