src/Tools/VSCode/src/vscode_rendering.scala
author wenzelm
Wed, 28 Dec 2016 16:45:00 +0100
changeset 64679 b2bf280b7e13
parent 64668 39a6c88c059b
child 64683 c0c09b6dfbe0
permissions -rw-r--r--
more uniform treatment of input/output wrt. client; support for diagnistic messages; misc tuning;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/VSCode/src/vscode_rendering.scala
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     3
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     4
Isabelle/VSCode-specific implementation of quasi-abstract rendering and
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     5
markup interpretation.
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     6
*/
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     7
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     8
package isabelle.vscode
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
     9
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    10
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    11
import isabelle._
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    12
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    13
object VSCode_Rendering
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    14
{
64679
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    15
  /* diagnostic messages */
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    16
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    17
  private val message_severity =
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    18
    Map(
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    19
      Markup.WRITELN -> Protocol.DiagnosticSeverity.Hint,
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    20
      Markup.INFORMATION -> Protocol.DiagnosticSeverity.Information,
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    21
      Markup.WARNING -> Protocol.DiagnosticSeverity.Warning,
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    22
      Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning,
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    23
      Markup.ERROR -> Protocol.DiagnosticSeverity.Error,
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    24
      Markup.BAD -> Protocol.DiagnosticSeverity.Error)
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    25
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    26
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    27
  /* markup elements */
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    28
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    29
  private val diagnostics_elements =
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    30
    Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    31
      Markup.BAD)
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    32
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    33
  private val hyperlink_elements =
64652
ad55f164ae0d VSCode already detects URLs from plain text;
wenzelm
parents: 64651
diff changeset
    34
    Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION)
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    35
}
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    36
64649
d67c3094a0c2 tuned signature -- more explicit types;
wenzelm
parents: 64648
diff changeset
    37
class VSCode_Rendering(
d67c3094a0c2 tuned signature -- more explicit types;
wenzelm
parents: 64648
diff changeset
    38
    val model: Document_Model,
d67c3094a0c2 tuned signature -- more explicit types;
wenzelm
parents: 64648
diff changeset
    39
    snapshot: Document.Snapshot,
d67c3094a0c2 tuned signature -- more explicit types;
wenzelm
parents: 64648
diff changeset
    40
    options: Options,
d67c3094a0c2 tuned signature -- more explicit types;
wenzelm
parents: 64648
diff changeset
    41
    resources: Resources)
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    42
  extends Rendering(snapshot, options, resources)
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    43
{
64679
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    44
  /* diagnostics */
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    45
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    46
  def diagnostics: List[Text.Info[Command.Results]] =
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    47
    snapshot.cumulate[Command.Results](
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    48
      Text.Range.full, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ =>
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    49
      {
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    50
        case (res, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(i)), body)))
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    51
        if body.nonEmpty => Some(res + (i -> msg))
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    52
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    53
        case _ => None
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    54
      })
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    55
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    56
  val diagnostics_margin = options.int("vscode_diagnostics_margin")
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    57
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    58
  def diagnostics_output(results: List[Text.Info[Command.Results]]): List[Protocol.Diagnostic] =
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    59
  {
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    60
    (for {
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    61
      Text.Info(text_range, res) <- results.iterator
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    62
      range = model.doc.range(text_range, model.text_length)
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    63
      (_, XML.Elem(Markup(name, _), body)) <- res.iterator
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    64
    } yield {
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    65
      val message = Pretty.string_of(body, margin = diagnostics_margin)
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    66
      val severity = VSCode_Rendering.message_severity.get(name)
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    67
      Protocol.Diagnostic(range, message, severity = severity)
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    68
    }).toList
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    69
  }
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    70
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    71
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    72
  /* tooltips */
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    73
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    74
  def tooltip_margin: Int = options.int("vscode_tooltip_margin")
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
    75
  def timing_threshold: Double = options.real("vscode_timing_threshold")
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    76
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    77
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    78
  /* hyperlinks */
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
    79
64667
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
    80
  def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range)
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
    81
    : Option[Line.Node_Range] =
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
    82
  {
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
    83
    for (name <- resources.source_file(source_name))
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
    84
    yield {
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
    85
      val opt_text =
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
    86
        try { Some(File.read(Path.explode(name))) } // FIXME content from resources/models
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
    87
        catch { case ERROR(_) => None }
64668
39a6c88c059b proper file:// URL for external references;
wenzelm
parents: 64667
diff changeset
    88
      Line.Node_Range(File.platform_url(name),
64667
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
    89
        opt_text match {
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
    90
          case Some(text) if range.start > 0 =>
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
    91
            val chunk = Symbol.Text_Chunk(text)
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
    92
            val doc = Line.Document(text)
64679
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    93
            def position(offset: Symbol.Offset) =
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64668
diff changeset
    94
              doc.position(chunk.decode(offset), model.text_length)
64667
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
    95
            Line.Range(position(range.start), position(range.stop))
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
    96
          case _ =>
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
    97
            Line.Range(Line.Position((line1 - 1) max 0))
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
    98
        })
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
    99
    }
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   100
  }
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   101
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   102
  def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] =
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   103
  {
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   104
    if (snapshot.is_outdated) None
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   105
    else
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   106
      for {
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   107
        start <- snapshot.find_command_position(id, range.start)
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   108
        stop <- snapshot.find_command_position(id, range.stop)
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   109
      } yield Line.Node_Range(start.name, Line.Range(start.pos, stop.pos))
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   110
  }
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   111
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   112
  def hyperlink_position(pos: Position.T): Option[Line.Node_Range] =
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   113
    pos match {
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   114
      case Position.Item_File(name, line, range) => hyperlink_source_file(name, line, range)
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   115
      case Position.Item_Id(id, range) => hyperlink_command(id, range)
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   116
      case _ => None
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   117
    }
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   118
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   119
  def hyperlink_def_position(pos: Position.T): Option[Line.Node_Range] =
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   120
    pos match {
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   121
      case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range)
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   122
      case Position.Item_Def_Id(id, range) => hyperlink_command(id, range)
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   123
      case _ => None
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   124
    }
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   125
64651
ea5620f7b0d8 clarified signature;
wenzelm
parents: 64649
diff changeset
   126
  def hyperlinks(range: Text.Range): List[Line.Node_Range] =
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
   127
  {
64651
ea5620f7b0d8 clarified signature;
wenzelm
parents: 64649
diff changeset
   128
    snapshot.cumulate[List[Line.Node_Range]](
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
   129
      range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
   130
        {
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
   131
          case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
64654
31b681e38c70 clarified signature;
wenzelm
parents: 64652
diff changeset
   132
            val file = resources.append_file_url(snapshot.node_name.master_dir, name)
31b681e38c70 clarified signature;
wenzelm
parents: 64652
diff changeset
   133
            Some(Line.Node_Range(file) :: links)
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
   134
64667
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   135
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   136
            hyperlink_def_position(props).map(_ :: links)
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   137
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   138
          case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
cdb0d559a24b full range for Position.Item;
wenzelm
parents: 64659
diff changeset
   139
            hyperlink_position(props).map(_ :: links)
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
   140
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
   141
          case _ => None
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
   142
        }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil }
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64622
diff changeset
   143
  }
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff changeset
   144
}