src/Tools/VSCode/src/protocol.scala
author wenzelm
Thu Dec 22 11:08:58 2016 +0100 (2016-12-22)
changeset 64655 ea34f36ff6a5
parent 64651 ea5620f7b0d8
child 64675 c557279d93f2
permissions -rw-r--r--
clarified message;
     1 /*  Title:      Tools/VSCode/src/protocol.scala
     2     Author:     Makarius
     3 
     4 Message formats for Language Server Protocol 2.0, see
     5 https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md
     6 */
     7 
     8 package isabelle.vscode
     9 
    10 
    11 import isabelle._
    12 
    13 
    14 object Protocol
    15 {
    16   /* abstract message */
    17 
    18   object Message
    19   {
    20     val empty: Map[String, JSON.T] = Map("jsonrpc" -> "2.0")
    21   }
    22 
    23 
    24   /* notification */
    25 
    26   object Notification
    27   {
    28     def apply(method: String, params: JSON.T): JSON.T =
    29       Message.empty + ("method" -> method) + ("params" -> params)
    30 
    31     def unapply(json: JSON.T): Option[(String, Option[JSON.T])] =
    32       for {
    33         method <- JSON.string(json, "method")
    34         params = JSON.value(json, "params")
    35       } yield (method, params)
    36   }
    37 
    38   class Notification0(name: String)
    39   {
    40     def unapply(json: JSON.T): Option[Unit] =
    41       json match {
    42         case Notification(method, _) if method == name => Some(())
    43         case _ => None
    44       }
    45   }
    46 
    47 
    48   /* request message */
    49 
    50   sealed case class Id(id: Any)
    51   {
    52     require(
    53       id.isInstanceOf[Int] ||
    54       id.isInstanceOf[Long] ||
    55       id.isInstanceOf[Double] ||
    56       id.isInstanceOf[String])
    57 
    58     override def toString: String = id.toString
    59   }
    60 
    61   object RequestMessage
    62   {
    63     def apply(id: Id, method: String, params: JSON.T): JSON.T =
    64       Message.empty + ("id" -> id.id) + ("method" -> method) + ("params" -> params)
    65 
    66     def unapply(json: JSON.T): Option[(Id, String, Option[JSON.T])] =
    67       for {
    68         id <- JSON.long(json, "id") orElse JSON.double(json, "id") orElse JSON.string(json, "id")
    69         method <- JSON.string(json, "method")
    70         params = JSON.value(json, "params")
    71       } yield (Id(id), method, params)
    72   }
    73 
    74   class Request0(name: String)
    75   {
    76     def unapply(json: JSON.T): Option[Id] =
    77       json match {
    78         case RequestMessage(id, method, _) if method == name => Some(id)
    79         case _ => None
    80       }
    81   }
    82 
    83   class RequestTextDocumentPosition(name: String)
    84   {
    85     def unapply(json: JSON.T): Option[(Id, Line.Node_Position)] =
    86       json match {
    87         case RequestMessage(id, method, Some(TextDocumentPosition(node_pos))) if method == name =>
    88           Some((id, node_pos))
    89         case _ => None
    90       }
    91   }
    92 
    93 
    94   /* response message */
    95 
    96   object ResponseMessage
    97   {
    98     def apply(id: Id, result: Option[JSON.T] = None, error: Option[ResponseError] = None): JSON.T =
    99       Message.empty + ("id" -> id.id) ++
   100       (result match { case Some(x) => Map("result" -> x) case None => Map.empty }) ++
   101       (error match { case Some(x) => Map("error" -> x.json) case None => Map.empty })
   102 
   103     def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T =
   104       if (error == "") apply(id, result = result)
   105       else apply(id, error = Some(ResponseError(code = ErrorCodes.serverErrorEnd, message = error)))
   106   }
   107 
   108   sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None)
   109   {
   110     def json: JSON.T =
   111       Map("code" -> code, "message" -> message) ++
   112       (data match { case Some(x) => Map("data" -> x) case None => Map.empty })
   113   }
   114 
   115   object ErrorCodes
   116   {
   117     val ParseError = -32700
   118     val InvalidRequest = -32600
   119     val MethodNotFound = -32601
   120     val InvalidParams = -32602
   121     val InternalError = -32603
   122     val serverErrorStart = -32099
   123     val serverErrorEnd = -32000
   124   }
   125 
   126 
   127   /* init and exit */
   128 
   129   object Initialize extends Request0("initialize")
   130   {
   131     def reply(id: Id, error: String): JSON.T =
   132       ResponseMessage.strict(id, Some(Map("capabilities" -> ServerCapabilities.json)), error)
   133   }
   134 
   135   object ServerCapabilities
   136   {
   137     val json: JSON.T =
   138       Map(
   139         "textDocumentSync" -> 1,
   140         "hoverProvider" -> true,
   141         "definitionProvider" -> true)
   142   }
   143 
   144   object Shutdown extends Request0("shutdown")
   145   {
   146     def reply(id: Id, error: String): JSON.T =
   147       ResponseMessage.strict(id, Some("OK"), error)
   148   }
   149 
   150   object Exit extends Notification0("exit")
   151 
   152 
   153   /* document positions */
   154 
   155   object Position
   156   {
   157     def apply(pos: Line.Position): JSON.T =
   158       Map("line" -> pos.line, "character" -> pos.column)
   159 
   160     def unapply(json: JSON.T): Option[Line.Position] =
   161       for {
   162         line <- JSON.int(json, "line")
   163         column <- JSON.int(json, "character")
   164       } yield Line.Position(line, column)
   165   }
   166 
   167   object Range
   168   {
   169     def apply(range: Line.Range): JSON.T =
   170       Map("start" -> Position(range.start), "end" -> Position(range.stop))
   171 
   172     def unapply(json: JSON.T): Option[Line.Range] =
   173       (JSON.value(json, "start"), JSON.value(json, "end")) match {
   174         case (Some(Position(start)), Some(Position(stop))) => Some(Line.Range(start, stop))
   175         case _ => None
   176       }
   177   }
   178 
   179   object Location
   180   {
   181     def apply(loc: Line.Node_Range): JSON.T =
   182       Map("uri" -> loc.name, "range" -> Range(loc.range))
   183 
   184     def unapply(json: JSON.T): Option[Line.Node_Range] =
   185       for {
   186         uri <- JSON.string(json, "uri")
   187         range_json <- JSON.value(json, "range")
   188         range <- Range.unapply(range_json)
   189       } yield Line.Node_Range(uri, range)
   190   }
   191 
   192   object TextDocumentPosition
   193   {
   194     def unapply(json: JSON.T): Option[Line.Node_Position] =
   195       for {
   196         doc <- JSON.value(json, "textDocument")
   197         uri <- JSON.string(doc, "uri")
   198         pos_json <- JSON.value(json, "position")
   199         pos <- Position.unapply(pos_json)
   200       } yield Line.Node_Position(uri, pos)
   201   }
   202 
   203 
   204   /* diagnostic messages */
   205 
   206   object MessageType
   207   {
   208     val Error = 1
   209     val Warning = 2
   210     val Info = 3
   211     val Log = 4
   212   }
   213 
   214   object DisplayMessage
   215   {
   216     def apply(message_type: Int, message: String, show: Boolean = true): JSON.T =
   217       Notification(if (show) "window/showMessage" else "window/logMessage",
   218         Map("type" -> message_type, "message" -> message))
   219   }
   220 
   221 
   222   /* document edits */
   223 
   224   object DidOpenTextDocument
   225   {
   226     def unapply(json: JSON.T): Option[(String, String, Long, String)] =
   227       json match {
   228         case Notification("textDocument/didOpen", Some(params)) =>
   229           for {
   230             doc <- JSON.value(params, "textDocument")
   231             uri <- JSON.string(doc, "uri")
   232             lang <- JSON.string(doc, "languageId")
   233             version <- JSON.long(doc, "version")
   234             text <- JSON.string(doc, "text")
   235           } yield (uri, lang, version, text)
   236         case _ => None
   237       }
   238   }
   239 
   240 
   241   sealed abstract class TextDocumentContentChange
   242   case class TextDocumentContent(text: String) extends TextDocumentContentChange
   243   case class TextDocumentChange(range: Line.Range, range_length: Int, text: String)
   244     extends TextDocumentContentChange
   245 
   246   object TextDocumentContentChange
   247   {
   248     def unapply(json: JSON.T): Option[TextDocumentContentChange] =
   249       for { text <- JSON.string(json, "text") }
   250       yield {
   251         (JSON.value(json, "range"), JSON.int(json, "rangeLength")) match {
   252           case (Some(Range(range)), Some(range_length)) =>
   253             TextDocumentChange(range, range_length, text)
   254           case _ => TextDocumentContent(text)
   255         }
   256       }
   257   }
   258 
   259   object DidChangeTextDocument
   260   {
   261     def unapply(json: JSON.T): Option[(String, Long, List[TextDocumentContentChange])] =
   262       json match {
   263         case Notification("textDocument/didChange", Some(params)) =>
   264           for {
   265             doc <- JSON.value(params, "textDocument")
   266             uri <- JSON.string(doc, "uri")
   267             version <- JSON.long(doc, "version")
   268             changes <- JSON.array(params, "contentChanges", TextDocumentContentChange.unapply _)
   269           } yield (uri, version, changes)
   270         case _ => None
   271       }
   272   }
   273 
   274   class TextDocumentNotification(name: String)
   275   {
   276     def unapply(json: JSON.T): Option[String] =
   277       json match {
   278         case Notification(method, Some(params)) if method == name =>
   279           for {
   280             doc <- JSON.value(params, "textDocument")
   281             uri <- JSON.string(doc, "uri")
   282           } yield uri
   283         case _ => None
   284       }
   285   }
   286 
   287   object DidCloseTextDocument extends TextDocumentNotification("textDocument/didClose")
   288   object DidSaveTextDocument extends TextDocumentNotification("textDocument/didSave")
   289 
   290 
   291   /* hover request */
   292 
   293   object Hover extends RequestTextDocumentPosition("textDocument/hover")
   294   {
   295     def reply(id: Id, result: Option[(Line.Range, List[String])]): JSON.T =
   296     {
   297       val res =
   298         result match {
   299           case Some((range, contents)) => Map("contents" -> contents, "range" -> Range(range))
   300           case None => Map("contents" -> Nil)
   301         }
   302       ResponseMessage(id, Some(res))
   303     }
   304   }
   305 
   306 
   307   /* goto definition request */
   308 
   309   object GotoDefinition extends RequestTextDocumentPosition("textDocument/definition")
   310   {
   311     def reply(id: Id, result: List[Line.Node_Range]): JSON.T =
   312       ResponseMessage(id, Some(result.map(Location.apply(_))))
   313   }
   314 }