src/Tools/VSCode/src/protocol.scala
author wenzelm
Tue Dec 20 22:24:16 2016 +0100 (2016-12-20)
changeset 64622 529bbb8977c7
parent 64605 9c1173a7e4cb
child 64648 5d7f741aaccb
permissions -rw-r--r--
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
     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 
    84   /* response message */
    85 
    86   object ResponseMessage
    87   {
    88     def apply(id: Id, result: Option[JSON.T] = None, error: Option[ResponseError] = None): JSON.T =
    89       Message.empty + ("id" -> id.id) ++
    90       (result match { case Some(x) => Map("result" -> x) case None => Map.empty }) ++
    91       (error match { case Some(x) => Map("error" -> x.json) case None => Map.empty })
    92 
    93     def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T =
    94       if (error == "") apply(id, result = result)
    95       else apply(id, error = Some(ResponseError(code = ErrorCodes.serverErrorEnd, message = error)))
    96   }
    97 
    98   sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None)
    99   {
   100     def json: JSON.T =
   101       Map("code" -> code, "message" -> message) ++
   102       (data match { case Some(x) => Map("data" -> x) case None => Map.empty })
   103   }
   104 
   105   object ErrorCodes
   106   {
   107     val ParseError = -32700
   108     val InvalidRequest = -32600
   109     val MethodNotFound = -32601
   110     val InvalidParams = -32602
   111     val InternalError = -32603
   112     val serverErrorStart = -32099
   113     val serverErrorEnd = -32000
   114   }
   115 
   116 
   117   /* init and exit */
   118 
   119   object Initialize extends Request0("initialize")
   120   {
   121     def reply(id: Id, error: String): JSON.T =
   122       ResponseMessage.strict(id, Some(Map("capabilities" -> ServerCapabilities.json)), error)
   123   }
   124 
   125   object ServerCapabilities
   126   {
   127     val json: JSON.T =
   128       Map("textDocumentSync" -> 1, "hoverProvider" -> true)
   129   }
   130 
   131   object Shutdown extends Request0("shutdown")
   132   {
   133     def reply(id: Id, error: String): JSON.T =
   134       ResponseMessage.strict(id, Some("OK"), error)
   135   }
   136 
   137   object Exit extends Notification0("exit")
   138 
   139 
   140   /* document positions */
   141 
   142   object Position
   143   {
   144     def apply(pos: Line.Position): JSON.T =
   145       Map("line" -> pos.line, "character" -> pos.column)
   146 
   147     def unapply(json: JSON.T): Option[Line.Position] =
   148       for {
   149         line <- JSON.int(json, "line")
   150         column <- JSON.int(json, "character")
   151       } yield Line.Position(line, column)
   152   }
   153 
   154   object Range
   155   {
   156     def apply(range: Line.Range): JSON.T =
   157       Map("start" -> Position(range.start), "end" -> Position(range.stop))
   158 
   159     def unapply(json: JSON.T): Option[Line.Range] =
   160       (JSON.value(json, "start"), JSON.value(json, "end")) match {
   161         case (Some(Position(start)), Some(Position(stop))) => Some(Line.Range(start, stop))
   162         case _ => None
   163       }
   164   }
   165 
   166   object Location
   167   {
   168     def apply(uri: String, range: Line.Range): JSON.T =
   169       Map("uri" -> uri, "range" -> Range(range))
   170 
   171     def unapply(json: JSON.T): Option[(String, Line.Range)] =
   172       for {
   173         uri <- JSON.string(json, "uri")
   174         range_json <- JSON.value(json, "range")
   175         range <- Range.unapply(range_json)
   176       } yield (uri, range)
   177   }
   178 
   179   object TextDocumentPosition
   180   {
   181     def unapply(json: JSON.T): Option[(String, Line.Position)] =
   182       for {
   183         doc <- JSON.value(json, "textDocument")
   184         uri <- JSON.string(doc, "uri")
   185         pos_json <- JSON.value(json, "position")
   186         pos <- Position.unapply(pos_json)
   187       } yield (uri, pos)
   188   }
   189 
   190 
   191   /* diagnostic messages */
   192 
   193   object MessageType
   194   {
   195     val Error = 1
   196     val Warning = 2
   197     val Info = 3
   198     val Log = 4
   199   }
   200 
   201   object DisplayMessage
   202   {
   203     def apply(message_type: Int, message: String, show: Boolean = true): JSON.T =
   204       Notification(if (show) "window/showMessage" else "window/logMessage",
   205         Map("type" -> message_type, "message" -> message))
   206   }
   207 
   208 
   209   /* document edits */
   210 
   211   object DidOpenTextDocument
   212   {
   213     def unapply(json: JSON.T): Option[(String, String, Long, String)] =
   214       json match {
   215         case Notification("textDocument/didOpen", Some(params)) =>
   216           for {
   217             doc <- JSON.value(params, "textDocument")
   218             uri <- JSON.string(doc, "uri")
   219             lang <- JSON.string(doc, "languageId")
   220             version <- JSON.long(doc, "version")
   221             text <- JSON.string(doc, "text")
   222           } yield (uri, lang, version, text)
   223         case _ => None
   224       }
   225   }
   226 
   227 
   228   sealed abstract class TextDocumentContentChange
   229   case class TextDocumentContent(text: String) extends TextDocumentContentChange
   230   case class TextDocumentChange(range: Line.Range, range_length: Int, text: String)
   231     extends TextDocumentContentChange
   232 
   233   object TextDocumentContentChange
   234   {
   235     def unapply(json: JSON.T): Option[TextDocumentContentChange] =
   236       for { text <- JSON.string(json, "text") }
   237       yield {
   238         (JSON.value(json, "range"), JSON.int(json, "rangeLength")) match {
   239           case (Some(Range(range)), Some(range_length)) =>
   240             TextDocumentChange(range, range_length, text)
   241           case _ => TextDocumentContent(text)
   242         }
   243       }
   244   }
   245 
   246   object DidChangeTextDocument
   247   {
   248     def unapply(json: JSON.T): Option[(String, Long, List[TextDocumentContentChange])] =
   249       json match {
   250         case Notification("textDocument/didChange", Some(params)) =>
   251           for {
   252             doc <- JSON.value(params, "textDocument")
   253             uri <- JSON.string(doc, "uri")
   254             version <- JSON.long(doc, "version")
   255             changes <- JSON.array(params, "contentChanges", TextDocumentContentChange.unapply _)
   256           } yield (uri, version, changes)
   257         case _ => None
   258       }
   259   }
   260 
   261   class TextDocumentNotification(name: String)
   262   {
   263     def unapply(json: JSON.T): Option[String] =
   264       json match {
   265         case Notification(method, Some(params)) if method == name =>
   266           for {
   267             doc <- JSON.value(params, "textDocument")
   268             uri <- JSON.string(doc, "uri")
   269           } yield uri
   270         case _ => None
   271       }
   272   }
   273 
   274   object DidCloseTextDocument extends TextDocumentNotification("textDocument/didClose")
   275   object DidSaveTextDocument extends TextDocumentNotification("textDocument/didSave")
   276 
   277 
   278   /* hover request */
   279 
   280   object Hover
   281   {
   282     def unapply(json: JSON.T): Option[(Id, String, Line.Position)] =
   283       json match {
   284         case RequestMessage(id, "textDocument/hover", Some(TextDocumentPosition(uri, pos))) =>
   285           Some((id, uri, pos))
   286         case _ => None
   287       }
   288 
   289     def reply(id: Id, result: Option[(Line.Range, List[String])]): JSON.T =
   290     {
   291       val res =
   292         result match {
   293           case Some((range, contents)) => Map("contents" -> contents, "range" -> Range(range))
   294           case None => Map("contents" -> Nil)
   295         }
   296       ResponseMessage(id, Some(res))
   297     }
   298   }
   299 }