src/Tools/VSCode/src/protocol.scala
author wenzelm
Wed, 14 Jun 2017 11:32:47 +0200
changeset 66090 5e1c1b366ac3
parent 66062 175772371cd0
child 66096 6187612e83c1
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/VSCode/src/protocol.scala
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     3
65165
d98ede9e5917 updated to vscode-languageclient 3.0;
wenzelm
parents: 65160
diff changeset
     4
Message formats for Language Server Protocol 3.0, see
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     5
https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     6
*/
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     7
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     8
package isabelle.vscode
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     9
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    10
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    11
import isabelle._
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    12
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64767
diff changeset
    13
import java.io.{File => JFile}
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64767
diff changeset
    14
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64767
diff changeset
    15
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    16
object Protocol
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    17
{
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    18
  /* abstract message */
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    19
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    20
  object Message
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    21
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    22
    val empty: Map[String, JSON.T] = Map("jsonrpc" -> "2.0")
65922
d2f19f05c0e9 clarified message logging;
wenzelm
parents: 65229
diff changeset
    23
d2f19f05c0e9 clarified message logging;
wenzelm
parents: 65229
diff changeset
    24
    def log(prefix: String, json: JSON.T, logger: Logger, verbose: Boolean)
d2f19f05c0e9 clarified message logging;
wenzelm
parents: 65229
diff changeset
    25
    {
d2f19f05c0e9 clarified message logging;
wenzelm
parents: 65229
diff changeset
    26
      val header: Map[String, Any] =
d2f19f05c0e9 clarified message logging;
wenzelm
parents: 65229
diff changeset
    27
        json match {
65924
9140c9cce351 clarified output: do not require "method", which is absent for ResponseMessage;
wenzelm
parents: 65922
diff changeset
    28
          case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) =>
9140c9cce351 clarified output: do not require "method", which is absent for ResponseMessage;
wenzelm
parents: 65922
diff changeset
    29
            val obj = m.asInstanceOf[Map[String, JSON.T]]
9140c9cce351 clarified output: do not require "method", which is absent for ResponseMessage;
wenzelm
parents: 65922
diff changeset
    30
            obj -- (obj.keySet - "method" - "id")
65922
d2f19f05c0e9 clarified message logging;
wenzelm
parents: 65229
diff changeset
    31
          case _ => Map.empty
d2f19f05c0e9 clarified message logging;
wenzelm
parents: 65229
diff changeset
    32
        }
d2f19f05c0e9 clarified message logging;
wenzelm
parents: 65229
diff changeset
    33
      if (verbose || header.isEmpty) logger(prefix + "\n" + JSON.Format(json))
d2f19f05c0e9 clarified message logging;
wenzelm
parents: 65229
diff changeset
    34
      else logger(prefix + " " + JSON.Format(header))
d2f19f05c0e9 clarified message logging;
wenzelm
parents: 65229
diff changeset
    35
    }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    36
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    37
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    38
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    39
  /* notification */
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    40
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    41
  object Notification
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    42
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    43
    def apply(method: String, params: JSON.T): JSON.T =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    44
      Message.empty + ("method" -> method) + ("params" -> params)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    45
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    46
    def unapply(json: JSON.T): Option[(String, Option[JSON.T])] =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    47
      for {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    48
        method <- JSON.string(json, "method")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    49
        params = JSON.value(json, "params")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    50
      } yield (method, params)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    51
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    52
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    53
  class Notification0(name: String)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    54
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    55
    def unapply(json: JSON.T): Option[Unit] =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    56
      json match {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    57
        case Notification(method, _) if method == name => Some(())
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    58
        case _ => None
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    59
      }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    60
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    61
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    62
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    63
  /* request message */
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    64
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    65
  sealed case class Id(id: Any)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    66
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    67
    require(
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    68
      id.isInstanceOf[Int] ||
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    69
      id.isInstanceOf[Long] ||
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    70
      id.isInstanceOf[Double] ||
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    71
      id.isInstanceOf[String])
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    72
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    73
    override def toString: String = id.toString
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    74
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    75
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    76
  object RequestMessage
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    77
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    78
    def apply(id: Id, method: String, params: JSON.T): JSON.T =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    79
      Message.empty + ("id" -> id.id) + ("method" -> method) + ("params" -> params)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    80
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    81
    def unapply(json: JSON.T): Option[(Id, String, Option[JSON.T])] =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    82
      for {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    83
        id <- JSON.long(json, "id") orElse JSON.double(json, "id") orElse JSON.string(json, "id")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    84
        method <- JSON.string(json, "method")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    85
        params = JSON.value(json, "params")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    86
      } yield (Id(id), method, params)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    87
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    88
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    89
  class Request0(name: String)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    90
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    91
    def unapply(json: JSON.T): Option[Id] =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    92
      json match {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    93
        case RequestMessage(id, method, _) if method == name => Some(id)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    94
        case _ => None
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    95
      }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    96
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    97
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
    98
  class RequestTextDocumentPosition(name: String)
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
    99
  {
64651
ea5620f7b0d8 clarified signature;
wenzelm
parents: 64649
diff changeset
   100
    def unapply(json: JSON.T): Option[(Id, Line.Node_Position)] =
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   101
      json match {
64651
ea5620f7b0d8 clarified signature;
wenzelm
parents: 64649
diff changeset
   102
        case RequestMessage(id, method, Some(TextDocumentPosition(node_pos))) if method == name =>
ea5620f7b0d8 clarified signature;
wenzelm
parents: 64649
diff changeset
   103
          Some((id, node_pos))
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   104
        case _ => None
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   105
      }
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   106
  }
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   107
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   108
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   109
  /* response message */
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   110
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   111
  object ResponseMessage
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   112
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   113
    def apply(id: Id, result: Option[JSON.T] = None, error: Option[ResponseError] = None): JSON.T =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   114
      Message.empty + ("id" -> id.id) ++
64878
wenzelm
parents: 64877
diff changeset
   115
        JSON.optional("result" -> result) ++
wenzelm
parents: 64877
diff changeset
   116
        JSON.optional("error" -> error.map(_.json))
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   117
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   118
    def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   119
      if (error == "") apply(id, result = result)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   120
      else apply(id, error = Some(ResponseError(code = ErrorCodes.serverErrorEnd, message = error)))
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   121
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   122
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   123
  sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   124
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   125
    def json: JSON.T =
64878
wenzelm
parents: 64877
diff changeset
   126
      Map("code" -> code, "message" -> message) ++ JSON.optional("data" -> data)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   127
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   128
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   129
  object ErrorCodes
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   130
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   131
    val ParseError = -32700
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   132
    val InvalidRequest = -32600
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   133
    val MethodNotFound = -32601
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   134
    val InvalidParams = -32602
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   135
    val InternalError = -32603
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   136
    val serverErrorStart = -32099
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   137
    val serverErrorEnd = -32000
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   138
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   139
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   140
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   141
  /* init and exit */
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   142
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   143
  object Initialize extends Request0("initialize")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   144
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   145
    def reply(id: Id, error: String): JSON.T =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   146
      ResponseMessage.strict(id, Some(Map("capabilities" -> ServerCapabilities.json)), error)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   147
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   148
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   149
  object ServerCapabilities
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   150
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   151
    val json: JSON.T =
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   152
      Map(
65160
6e042537555d incremental document changes;
wenzelm
parents: 65106
diff changeset
   153
        "textDocumentSync" -> 2,
64877
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   154
        "completionProvider" -> Map("resolveProvider" -> false, "triggerCharacters" -> Nil),
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   155
        "hoverProvider" -> true,
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   156
        "definitionProvider" -> true,
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   157
        "documentHighlightProvider" -> true)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   158
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   159
65229
cc96b8c3b8cb explicitly ignore "initialized" message;
wenzelm
parents: 65201
diff changeset
   160
  object Initialized extends Notification0("initialized")
cc96b8c3b8cb explicitly ignore "initialized" message;
wenzelm
parents: 65201
diff changeset
   161
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   162
  object Shutdown extends Request0("shutdown")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   163
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   164
    def reply(id: Id, error: String): JSON.T =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   165
      ResponseMessage.strict(id, Some("OK"), error)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   166
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   167
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   168
  object Exit extends Notification0("exit")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   169
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   170
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   171
  /* document positions */
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   172
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   173
  object Position
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   174
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   175
    def apply(pos: Line.Position): JSON.T =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   176
      Map("line" -> pos.line, "character" -> pos.column)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   177
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   178
    def unapply(json: JSON.T): Option[Line.Position] =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   179
      for {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   180
        line <- JSON.int(json, "line")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   181
        column <- JSON.int(json, "character")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   182
      } yield Line.Position(line, column)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   183
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   184
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   185
  object Range
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   186
  {
65173
3700be571a01 more compact protocol message;
wenzelm
parents: 65165
diff changeset
   187
    def compact(range: Line.Range): List[Int] =
3700be571a01 more compact protocol message;
wenzelm
parents: 65165
diff changeset
   188
      List(range.start.line, range.start.column, range.stop.line, range.stop.column)
3700be571a01 more compact protocol message;
wenzelm
parents: 65165
diff changeset
   189
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   190
    def apply(range: Line.Range): JSON.T =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   191
      Map("start" -> Position(range.start), "end" -> Position(range.stop))
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   192
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   193
    def unapply(json: JSON.T): Option[Line.Range] =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   194
      (JSON.value(json, "start"), JSON.value(json, "end")) match {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   195
        case (Some(Position(start)), Some(Position(stop))) => Some(Line.Range(start, stop))
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   196
        case _ => None
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   197
      }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   198
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   199
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   200
  object Location
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   201
  {
64651
ea5620f7b0d8 clarified signature;
wenzelm
parents: 64649
diff changeset
   202
    def apply(loc: Line.Node_Range): JSON.T =
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64767
diff changeset
   203
      Map("uri" -> Url.print_file_name(loc.name), "range" -> Range(loc.range))
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   204
64651
ea5620f7b0d8 clarified signature;
wenzelm
parents: 64649
diff changeset
   205
    def unapply(json: JSON.T): Option[Line.Node_Range] =
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   206
      for {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   207
        uri <- JSON.string(json, "uri")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   208
        range_json <- JSON.value(json, "range")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   209
        range <- Range.unapply(range_json)
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64767
diff changeset
   210
      } yield Line.Node_Range(Url.canonical_file_name(uri), range)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   211
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   212
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   213
  object TextDocumentPosition
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   214
  {
64651
ea5620f7b0d8 clarified signature;
wenzelm
parents: 64649
diff changeset
   215
    def unapply(json: JSON.T): Option[Line.Node_Position] =
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   216
      for {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   217
        doc <- JSON.value(json, "textDocument")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   218
        uri <- JSON.string(doc, "uri")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   219
        pos_json <- JSON.value(json, "position")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   220
        pos <- Position.unapply(pos_json)
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64767
diff changeset
   221
      } yield Line.Node_Position(Url.canonical_file_name(uri), pos)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   222
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   223
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   224
65103
0bf1836ce4b1 tight protocol messages;
wenzelm
parents: 65095
diff changeset
   225
  /* marked strings */
65093
5f08197206ce clarified signature;
wenzelm
parents: 64878
diff changeset
   226
5f08197206ce clarified signature;
wenzelm
parents: 64878
diff changeset
   227
  sealed case class MarkedString(text: String, language: String = "plaintext")
5f08197206ce clarified signature;
wenzelm
parents: 64878
diff changeset
   228
  {
5f08197206ce clarified signature;
wenzelm
parents: 64878
diff changeset
   229
    def json: JSON.T = Map("language" -> language, "value" -> text)
5f08197206ce clarified signature;
wenzelm
parents: 64878
diff changeset
   230
  }
5f08197206ce clarified signature;
wenzelm
parents: 64878
diff changeset
   231
65103
0bf1836ce4b1 tight protocol messages;
wenzelm
parents: 65095
diff changeset
   232
  object MarkedStrings
0bf1836ce4b1 tight protocol messages;
wenzelm
parents: 65095
diff changeset
   233
  {
0bf1836ce4b1 tight protocol messages;
wenzelm
parents: 65095
diff changeset
   234
    def json(msgs: List[MarkedString]): Option[JSON.T] =
0bf1836ce4b1 tight protocol messages;
wenzelm
parents: 65095
diff changeset
   235
      msgs match {
0bf1836ce4b1 tight protocol messages;
wenzelm
parents: 65095
diff changeset
   236
        case Nil => None
0bf1836ce4b1 tight protocol messages;
wenzelm
parents: 65095
diff changeset
   237
        case List(msg) => Some(msg.json)
0bf1836ce4b1 tight protocol messages;
wenzelm
parents: 65095
diff changeset
   238
        case _ => Some(msgs.map(_.json))
0bf1836ce4b1 tight protocol messages;
wenzelm
parents: 65095
diff changeset
   239
      }
0bf1836ce4b1 tight protocol messages;
wenzelm
parents: 65095
diff changeset
   240
  }
0bf1836ce4b1 tight protocol messages;
wenzelm
parents: 65095
diff changeset
   241
65093
5f08197206ce clarified signature;
wenzelm
parents: 64878
diff changeset
   242
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   243
  /* diagnostic messages */
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   244
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   245
  object MessageType
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   246
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   247
    val Error = 1
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   248
    val Warning = 2
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   249
    val Info = 3
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   250
    val Log = 4
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   251
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   252
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   253
  object DisplayMessage
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   254
  {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   255
    def apply(message_type: Int, message: String, show: Boolean = true): JSON.T =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   256
      Notification(if (show) "window/showMessage" else "window/logMessage",
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   257
        Map("type" -> message_type, "message" -> message))
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   258
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   259
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   260
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   261
  /* document edits */
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   262
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   263
  object DidOpenTextDocument
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   264
  {
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64767
diff changeset
   265
    def unapply(json: JSON.T): Option[(JFile, String, Long, String)] =
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   266
      json match {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   267
        case Notification("textDocument/didOpen", Some(params)) =>
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   268
          for {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   269
            doc <- JSON.value(params, "textDocument")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   270
            uri <- JSON.string(doc, "uri")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   271
            lang <- JSON.string(doc, "languageId")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   272
            version <- JSON.long(doc, "version")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   273
            text <- JSON.string(doc, "text")
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64767
diff changeset
   274
          } yield (Url.canonical_file(uri), lang, version, text)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   275
        case _ => None
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   276
      }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   277
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   278
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   279
65160
6e042537555d incremental document changes;
wenzelm
parents: 65106
diff changeset
   280
  sealed case class TextDocumentChange(range: Option[Line.Range], text: String)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   281
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   282
  object DidChangeTextDocument
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   283
  {
65160
6e042537555d incremental document changes;
wenzelm
parents: 65106
diff changeset
   284
    def unapply_change(json: JSON.T): Option[TextDocumentChange] =
6e042537555d incremental document changes;
wenzelm
parents: 65106
diff changeset
   285
      for { text <- JSON.string(json, "text") }
6e042537555d incremental document changes;
wenzelm
parents: 65106
diff changeset
   286
      yield TextDocumentChange(JSON.value(json, "range", Range.unapply _), text)
6e042537555d incremental document changes;
wenzelm
parents: 65106
diff changeset
   287
6e042537555d incremental document changes;
wenzelm
parents: 65106
diff changeset
   288
    def unapply(json: JSON.T): Option[(JFile, Long, List[TextDocumentChange])] =
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   289
      json match {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   290
        case Notification("textDocument/didChange", Some(params)) =>
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   291
          for {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   292
            doc <- JSON.value(params, "textDocument")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   293
            uri <- JSON.string(doc, "uri")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   294
            version <- JSON.long(doc, "version")
65160
6e042537555d incremental document changes;
wenzelm
parents: 65106
diff changeset
   295
            changes <- JSON.array(params, "contentChanges", unapply_change _)
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64767
diff changeset
   296
          } yield (Url.canonical_file(uri), version, changes)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   297
        case _ => None
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   298
      }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   299
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   300
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   301
  class TextDocumentNotification(name: String)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   302
  {
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64767
diff changeset
   303
    def unapply(json: JSON.T): Option[JFile] =
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   304
      json match {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   305
        case Notification(method, Some(params)) if method == name =>
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   306
          for {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   307
            doc <- JSON.value(params, "textDocument")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   308
            uri <- JSON.string(doc, "uri")
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64767
diff changeset
   309
          } yield Url.canonical_file(uri)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   310
        case _ => None
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   311
      }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   312
  }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   313
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   314
  object DidCloseTextDocument extends TextDocumentNotification("textDocument/didClose")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   315
  object DidSaveTextDocument extends TextDocumentNotification("textDocument/didSave")
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   316
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   317
64877
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   318
  /* completion */
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   319
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   320
  sealed case class CompletionItem(
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   321
    label: String,
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   322
    kind: Option[Int] = None,
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   323
    detail: Option[String] = None,
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   324
    documentation: Option[String] = None,
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   325
    insertText: Option[String] = None,
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   326
    range: Option[Line.Range] = None)
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   327
  {
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   328
    def json: JSON.T =
66061
wenzelm
parents: 66052
diff changeset
   329
      Map("label" -> label) ++
wenzelm
parents: 66052
diff changeset
   330
      JSON.optional("kind" -> kind) ++
wenzelm
parents: 66052
diff changeset
   331
      JSON.optional("detail" -> detail) ++
wenzelm
parents: 66052
diff changeset
   332
      JSON.optional("documentation" -> documentation) ++
wenzelm
parents: 66052
diff changeset
   333
      JSON.optional("insertText" -> insertText) ++
66062
175772371cd0 use old-style "textEdit" for the sake of the external protocol (see also vscode-languageserver-node/issues/188);
wenzelm
parents: 66061
diff changeset
   334
      JSON.optional("range" -> range.map(Range(_))) ++
175772371cd0 use old-style "textEdit" for the sake of the external protocol (see also vscode-languageserver-node/issues/188);
wenzelm
parents: 66061
diff changeset
   335
      JSON.optional("textEdit" ->
175772371cd0 use old-style "textEdit" for the sake of the external protocol (see also vscode-languageserver-node/issues/188);
wenzelm
parents: 66061
diff changeset
   336
        range.map(r => Map("range" -> Range(r), "newText" -> insertText.getOrElse(label))))
64877
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   337
  }
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   338
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   339
  object Completion extends RequestTextDocumentPosition("textDocument/completion")
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   340
  {
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   341
    def reply(id: Id, result: List[CompletionItem]): JSON.T =
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   342
      ResponseMessage(id, Some(result.map(_.json)))
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   343
  }
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   344
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   345
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   346
  /* hover request */
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   347
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   348
  object Hover extends RequestTextDocumentPosition("textDocument/hover")
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   349
  {
65093
5f08197206ce clarified signature;
wenzelm
parents: 64878
diff changeset
   350
    def reply(id: Id, result: Option[(Line.Range, List[MarkedString])]): JSON.T =
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   351
    {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   352
      val res =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   353
        result match {
64747
54afac94f52b proper content format;
wenzelm
parents: 64693
diff changeset
   354
          case Some((range, contents)) =>
65103
0bf1836ce4b1 tight protocol messages;
wenzelm
parents: 65095
diff changeset
   355
            Map("contents" -> MarkedStrings.json(contents).getOrElse(Nil), "range" -> Range(range))
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   356
          case None => Map("contents" -> Nil)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   357
        }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   358
      ResponseMessage(id, Some(res))
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   359
    }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   360
  }
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   361
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   362
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   363
  /* goto definition request */
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   364
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   365
  object GotoDefinition extends RequestTextDocumentPosition("textDocument/definition")
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   366
  {
64651
ea5620f7b0d8 clarified signature;
wenzelm
parents: 64649
diff changeset
   367
    def reply(id: Id, result: List[Line.Node_Range]): JSON.T =
64649
d67c3094a0c2 tuned signature -- more explicit types;
wenzelm
parents: 64648
diff changeset
   368
      ResponseMessage(id, Some(result.map(Location.apply(_))))
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   369
  }
64675
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   370
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   371
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   372
  /* document highlights request */
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   373
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   374
  object DocumentHighlight
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   375
  {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   376
    def text(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(1))
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   377
    def read(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(2))
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   378
    def write(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(3))
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   379
  }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   380
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   381
  sealed case class DocumentHighlight(range: Line.Range, kind: Option[Int] = None)
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   382
  {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   383
    def json: JSON.T =
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   384
      kind match {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   385
        case None => Map("range" -> Range(range))
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   386
        case Some(k) => Map("range" -> Range(range), "kind" -> k)
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   387
      }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   388
  }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   389
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   390
  object DocumentHighlights extends RequestTextDocumentPosition("textDocument/documentHighlight")
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   391
  {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   392
    def reply(id: Id, result: List[DocumentHighlight]): JSON.T =
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   393
      ResponseMessage(id, Some(result.map(_.json)))
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   394
  }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   395
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   396
64675
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   397
  /* diagnostics */
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   398
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   399
  sealed case class Diagnostic(range: Line.Range, message: String,
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   400
    severity: Option[Int] = None, code: Option[Int] = None, source: Option[String] = None)
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   401
  {
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   402
    def json: JSON.T =
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   403
      Message.empty + ("range" -> Range(range)) + ("message" -> message) ++
64878
wenzelm
parents: 64877
diff changeset
   404
      JSON.optional("severity" -> severity) ++
wenzelm
parents: 64877
diff changeset
   405
      JSON.optional("code" -> code) ++
wenzelm
parents: 64877
diff changeset
   406
      JSON.optional("source" -> source)
64675
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   407
  }
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   408
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   409
  object DiagnosticSeverity
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   410
  {
64762
cd545bec3fd0 clarified message severity, based on empirical observation of VSCode 1.8.1;
wenzelm
parents: 64747
diff changeset
   411
    val Error = 1
cd545bec3fd0 clarified message severity, based on empirical observation of VSCode 1.8.1;
wenzelm
parents: 64747
diff changeset
   412
    val Warning = 2
cd545bec3fd0 clarified message severity, based on empirical observation of VSCode 1.8.1;
wenzelm
parents: 64747
diff changeset
   413
    val Information = 3
cd545bec3fd0 clarified message severity, based on empirical observation of VSCode 1.8.1;
wenzelm
parents: 64747
diff changeset
   414
    val Hint = 4
64675
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   415
  }
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   416
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   417
  object PublishDiagnostics
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   418
  {
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64767
diff changeset
   419
    def apply(file: JFile, diagnostics: List[Diagnostic]): JSON.T =
64675
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   420
      Notification("textDocument/publishDiagnostics",
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64767
diff changeset
   421
        Map("uri" -> Url.print_file(file), "diagnostics" -> diagnostics.map(_.json)))
64675
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   422
  }
65094
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   423
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   424
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   425
  /* decorations */
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   426
65173
3700be571a01 more compact protocol message;
wenzelm
parents: 65165
diff changeset
   427
  sealed case class DecorationOpts(range: Line.Range, hover_message: List[MarkedString])
65094
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   428
  {
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   429
    def json: JSON.T =
65173
3700be571a01 more compact protocol message;
wenzelm
parents: 65165
diff changeset
   430
      Map("range" -> Range.compact(range)) ++
3700be571a01 more compact protocol message;
wenzelm
parents: 65165
diff changeset
   431
      JSON.optional("hover_message" -> MarkedStrings.json(hover_message))
65094
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   432
  }
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   433
65173
3700be571a01 more compact protocol message;
wenzelm
parents: 65165
diff changeset
   434
  sealed case class Decoration(typ: String, content: List[DecorationOpts])
65094
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   435
  {
65095
eb21a4f70b0e publish decorations like diagnostics;
wenzelm
parents: 65094
diff changeset
   436
    def json(file: JFile): JSON.T =
65094
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   437
      Notification("PIDE/decoration",
65173
3700be571a01 more compact protocol message;
wenzelm
parents: 65165
diff changeset
   438
        Map("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json)))
65094
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   439
  }
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   440
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   441
65201
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
   442
  /* caret handling */
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   443
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   444
  object Caret_Update
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   445
  {
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   446
    def unapply(json: JSON.T): Option[Option[(JFile, Line.Position)]] =
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   447
      json match {
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   448
        case Notification("PIDE/caret_update", Some(params)) =>
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   449
          val caret =
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   450
            for {
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   451
              uri <- JSON.string(params, "uri")
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   452
              if Url.is_wellformed_file(uri)
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   453
              pos <- Position.unapply(params)
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   454
            } yield (Url.canonical_file(uri), pos)
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   455
          Some(caret)
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   456
        case _ => None
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   457
      }
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   458
  }
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   459
65201
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
   460
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
   461
  /* dynamic output */
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
   462
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   463
  object Dynamic_Output
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   464
  {
66090
wenzelm
parents: 66062
diff changeset
   465
    def apply(content: String): JSON.T =
wenzelm
parents: 66062
diff changeset
   466
      Notification("PIDE/dynamic_output", Map("content" -> content))
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   467
  }
65977
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents: 65924
diff changeset
   468
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents: 65924
diff changeset
   469
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   470
  /* preview */
65977
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents: 65924
diff changeset
   471
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   472
  object Preview_Request
65977
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents: 65924
diff changeset
   473
  {
65983
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   474
    def unapply(json: JSON.T): Option[(JFile, Int)] =
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   475
      json match {
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   476
        case Notification("PIDE/preview_request", Some(params)) =>
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   477
          for {
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   478
            uri <- JSON.string(params, "uri")
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   479
            if Url.is_wellformed_file(uri)
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   480
            column <- JSON.int(params, "column")
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   481
          } yield (Url.canonical_file(uri), column)
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   482
        case _ => None
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   483
      }
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   484
  }
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   485
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   486
  object Preview_Response
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   487
  {
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   488
    def apply(file: JFile, column: Int, label: String, content: String): JSON.T =
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   489
      Notification("PIDE/preview_response",
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   490
        Map(
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   491
          "uri" -> Url.print_file(file),
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   492
          "column" -> column,
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   493
          "label" -> label,
d8c5603c1732 explicit preview request/response;
wenzelm
parents: 65979
diff changeset
   494
          "content" -> content))
65977
c51b74be23b6 provide preview content on Scala side (similar to output);
wenzelm
parents: 65924
diff changeset
   495
  }
66052
39eb61b1fa51 provide information about Isabelle symbols within VSCode;
wenzelm
parents: 65983
diff changeset
   496
39eb61b1fa51 provide information about Isabelle symbols within VSCode;
wenzelm
parents: 65983
diff changeset
   497
39eb61b1fa51 provide information about Isabelle symbols within VSCode;
wenzelm
parents: 65983
diff changeset
   498
  /* Isabelle symbols */
39eb61b1fa51 provide information about Isabelle symbols within VSCode;
wenzelm
parents: 65983
diff changeset
   499
39eb61b1fa51 provide information about Isabelle symbols within VSCode;
wenzelm
parents: 65983
diff changeset
   500
  object Symbols_Request extends Notification0("PIDE/symbols_request")
39eb61b1fa51 provide information about Isabelle symbols within VSCode;
wenzelm
parents: 65983
diff changeset
   501
39eb61b1fa51 provide information about Isabelle symbols within VSCode;
wenzelm
parents: 65983
diff changeset
   502
  object Symbols
39eb61b1fa51 provide information about Isabelle symbols within VSCode;
wenzelm
parents: 65983
diff changeset
   503
  {
39eb61b1fa51 provide information about Isabelle symbols within VSCode;
wenzelm
parents: 65983
diff changeset
   504
    def apply(): JSON.T =
39eb61b1fa51 provide information about Isabelle symbols within VSCode;
wenzelm
parents: 65983
diff changeset
   505
    {
39eb61b1fa51 provide information about Isabelle symbols within VSCode;
wenzelm
parents: 65983
diff changeset
   506
      val entries =
39eb61b1fa51 provide information about Isabelle symbols within VSCode;
wenzelm
parents: 65983
diff changeset
   507
        for ((sym, code) <- Symbol.codes)
39eb61b1fa51 provide information about Isabelle symbols within VSCode;
wenzelm
parents: 65983
diff changeset
   508
        yield Map("symbol" -> sym, "name" -> Symbol.names(sym), "code" -> code)
39eb61b1fa51 provide information about Isabelle symbols within VSCode;
wenzelm
parents: 65983
diff changeset
   509
      Notification("PIDE/symbols", Map("entries" -> entries))
39eb61b1fa51 provide information about Isabelle symbols within VSCode;
wenzelm
parents: 65983
diff changeset
   510
    }
39eb61b1fa51 provide information about Isabelle symbols within VSCode;
wenzelm
parents: 65983
diff changeset
   511
  }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   512
}