src/Tools/VSCode/src/protocol.scala
author wenzelm
Thu, 25 May 2017 19:23:01 +0200
changeset 65924 9140c9cce351
parent 65922 d2f19f05c0e9
child 65977 c51b74be23b6
permissions -rw-r--r--
clarified output: do not require "method", which is absent for ResponseMessage;
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 =
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   329
      Message.empty + ("label" -> label) ++
64878
wenzelm
parents: 64877
diff changeset
   330
        JSON.optional("kind" -> kind) ++
wenzelm
parents: 64877
diff changeset
   331
        JSON.optional("detail" -> detail) ++
wenzelm
parents: 64877
diff changeset
   332
        JSON.optional("documentation" -> documentation) ++
wenzelm
parents: 64877
diff changeset
   333
        JSON.optional("insertText" -> insertText) ++
wenzelm
parents: 64877
diff changeset
   334
        JSON.optional("range" -> range.map(Range(_)))
64877
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   335
  }
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   336
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   337
  object Completion extends RequestTextDocumentPosition("textDocument/completion")
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   338
  {
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   339
    def reply(id: Id, result: List[CompletionItem]): JSON.T =
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   340
      ResponseMessage(id, Some(result.map(_.json)))
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   341
  }
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   342
31e9920a0dc1 support for semantic completion;
wenzelm
parents: 64777
diff changeset
   343
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   344
  /* hover request */
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   345
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   346
  object Hover extends RequestTextDocumentPosition("textDocument/hover")
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   347
  {
65093
5f08197206ce clarified signature;
wenzelm
parents: 64878
diff changeset
   348
    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
   349
    {
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   350
      val res =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   351
        result match {
64747
54afac94f52b proper content format;
wenzelm
parents: 64693
diff changeset
   352
          case Some((range, contents)) =>
65103
0bf1836ce4b1 tight protocol messages;
wenzelm
parents: 65095
diff changeset
   353
            Map("contents" -> MarkedStrings.json(contents).getOrElse(Nil), "range" -> Range(range))
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   354
          case None => Map("contents" -> Nil)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   355
        }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   356
      ResponseMessage(id, Some(res))
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
  }
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   359
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   360
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   361
  /* goto definition request */
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
  object GotoDefinition extends RequestTextDocumentPosition("textDocument/definition")
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   364
  {
64651
ea5620f7b0d8 clarified signature;
wenzelm
parents: 64649
diff changeset
   365
    def reply(id: Id, result: List[Line.Node_Range]): JSON.T =
64649
d67c3094a0c2 tuned signature -- more explicit types;
wenzelm
parents: 64648
diff changeset
   366
      ResponseMessage(id, Some(result.map(Location.apply(_))))
64648
5d7f741aaccb basic support for hyperlinks / Goto Definition Request;
wenzelm
parents: 64605
diff changeset
   367
  }
64675
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   368
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   369
64767
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   370
  /* document highlights request */
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   371
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   372
  object DocumentHighlight
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   373
  {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   374
    def text(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(1))
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   375
    def read(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(2))
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   376
    def write(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(3))
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   377
  }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   378
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   379
  sealed case class DocumentHighlight(range: Line.Range, kind: Option[Int] = None)
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   380
  {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   381
    def json: JSON.T =
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   382
      kind match {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   383
        case None => Map("range" -> Range(range))
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   384
        case Some(k) => Map("range" -> Range(range), "kind" -> k)
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   385
      }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   386
  }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   387
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   388
  object DocumentHighlights extends RequestTextDocumentPosition("textDocument/documentHighlight")
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   389
  {
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   390
    def reply(id: Id, result: List[DocumentHighlight]): JSON.T =
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   391
      ResponseMessage(id, Some(result.map(_.json)))
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   392
  }
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   393
f5c4ffdb1124 support VSCode DocumentHighlights;
wenzelm
parents: 64762
diff changeset
   394
64675
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   395
  /* diagnostics */
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   396
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   397
  sealed case class Diagnostic(range: Line.Range, message: String,
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   398
    severity: Option[Int] = None, code: Option[Int] = None, source: Option[String] = None)
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   399
  {
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   400
    def json: JSON.T =
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   401
      Message.empty + ("range" -> Range(range)) + ("message" -> message) ++
64878
wenzelm
parents: 64877
diff changeset
   402
      JSON.optional("severity" -> severity) ++
wenzelm
parents: 64877
diff changeset
   403
      JSON.optional("code" -> code) ++
wenzelm
parents: 64877
diff changeset
   404
      JSON.optional("source" -> source)
64675
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   405
  }
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   406
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   407
  object DiagnosticSeverity
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   408
  {
64762
cd545bec3fd0 clarified message severity, based on empirical observation of VSCode 1.8.1;
wenzelm
parents: 64747
diff changeset
   409
    val Error = 1
cd545bec3fd0 clarified message severity, based on empirical observation of VSCode 1.8.1;
wenzelm
parents: 64747
diff changeset
   410
    val Warning = 2
cd545bec3fd0 clarified message severity, based on empirical observation of VSCode 1.8.1;
wenzelm
parents: 64747
diff changeset
   411
    val Information = 3
cd545bec3fd0 clarified message severity, based on empirical observation of VSCode 1.8.1;
wenzelm
parents: 64747
diff changeset
   412
    val Hint = 4
64675
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   413
  }
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   414
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   415
  object PublishDiagnostics
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   416
  {
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64767
diff changeset
   417
    def apply(file: JFile, diagnostics: List[Diagnostic]): JSON.T =
64675
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   418
      Notification("textDocument/publishDiagnostics",
64777
ca09695eb43c clarified Document.Node.Name (again): canonical platform file;
wenzelm
parents: 64767
diff changeset
   419
        Map("uri" -> Url.print_file(file), "diagnostics" -> diagnostics.map(_.json)))
64675
c557279d93f2 support for diagnostics;
wenzelm
parents: 64651
diff changeset
   420
  }
65094
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   421
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   422
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   423
  /* decorations */
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   424
65173
3700be571a01 more compact protocol message;
wenzelm
parents: 65165
diff changeset
   425
  sealed case class DecorationOpts(range: Line.Range, hover_message: List[MarkedString])
65094
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   426
  {
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   427
    def json: JSON.T =
65173
3700be571a01 more compact protocol message;
wenzelm
parents: 65165
diff changeset
   428
      Map("range" -> Range.compact(range)) ++
3700be571a01 more compact protocol message;
wenzelm
parents: 65165
diff changeset
   429
      JSON.optional("hover_message" -> MarkedStrings.json(hover_message))
65094
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   430
  }
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   431
65173
3700be571a01 more compact protocol message;
wenzelm
parents: 65165
diff changeset
   432
  sealed case class Decoration(typ: String, content: List[DecorationOpts])
65094
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   433
  {
65095
eb21a4f70b0e publish decorations like diagnostics;
wenzelm
parents: 65094
diff changeset
   434
    def json(file: JFile): JSON.T =
65094
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   435
      Notification("PIDE/decoration",
65173
3700be571a01 more compact protocol message;
wenzelm
parents: 65165
diff changeset
   436
        Map("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json)))
65094
386d9d487f62 support for decorations;
wenzelm
parents: 65093
diff changeset
   437
  }
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   438
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   439
65201
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
   440
  /* caret handling */
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   441
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   442
  object Caret_Update
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
    def unapply(json: JSON.T): Option[Option[(JFile, Line.Position)]] =
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   445
      json match {
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   446
        case Notification("PIDE/caret_update", Some(params)) =>
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   447
          val caret =
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   448
            for {
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   449
              uri <- JSON.string(params, "uri")
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   450
              if Url.is_wellformed_file(uri)
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   451
              pos <- Position.unapply(params)
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   452
            } yield (Url.canonical_file(uri), pos)
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   453
          Some(caret)
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   454
        case _ => None
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   455
      }
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   456
  }
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   457
65201
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
   458
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
   459
  /* dynamic output */
2d01b30e6ac6 clarified modules;
wenzelm
parents: 65200
diff changeset
   460
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   461
  object Dynamic_Output
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   462
  {
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   463
    def apply(body: String): JSON.T =
65200
1227a68fac7a more explicit message type: allows body to become empty;
wenzelm
parents: 65189
diff changeset
   464
      Notification("PIDE/dynamic_output", Map("body" -> body))
65189
41d2452845fc support for caret handling and dynamic output;
wenzelm
parents: 65173
diff changeset
   465
  }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   466
}