src/Tools/VSCode/src/protocol.scala
changeset 64675 c557279d93f2
parent 64651 ea5620f7b0d8
child 64685 0f00e2661164
equal deleted inserted replaced
64673:b5965890e54d 64675:c557279d93f2
   309   object GotoDefinition extends RequestTextDocumentPosition("textDocument/definition")
   309   object GotoDefinition extends RequestTextDocumentPosition("textDocument/definition")
   310   {
   310   {
   311     def reply(id: Id, result: List[Line.Node_Range]): JSON.T =
   311     def reply(id: Id, result: List[Line.Node_Range]): JSON.T =
   312       ResponseMessage(id, Some(result.map(Location.apply(_))))
   312       ResponseMessage(id, Some(result.map(Location.apply(_))))
   313   }
   313   }
       
   314 
       
   315 
       
   316   /* diagnostics */
       
   317 
       
   318   object Diagnostic
       
   319   {
       
   320     def message(range: Line.Range, msg: String, severity: Int): Diagnostic =
       
   321       Diagnostic(range, msg, severity = Some(severity))
       
   322 
       
   323     val error: (Line.Range, String) => Diagnostic = message(_, _, DiagnosticSeverity.Error)
       
   324     val warning: (Line.Range, String) => Diagnostic = message(_, _, DiagnosticSeverity.Warning)
       
   325     val information: (Line.Range, String) => Diagnostic = message(_, _, DiagnosticSeverity.Information)
       
   326     val hint: (Line.Range, String) => Diagnostic = message(_, _, DiagnosticSeverity.Hint)
       
   327   }
       
   328 
       
   329   sealed case class Diagnostic(range: Line.Range, message: String,
       
   330     severity: Option[Int] = None, code: Option[Int] = None, source: Option[String] = None)
       
   331   {
       
   332     def json: JSON.T =
       
   333       Message.empty + ("range" -> Range(range)) + ("message" -> message) ++
       
   334       (severity match { case Some(x) => Map("severity" -> x) case None => Map.empty }) ++
       
   335       (code match { case Some(x) => Map("code" -> x) case None => Map.empty }) ++
       
   336       (source match { case Some(x) => Map("source" -> x) case None => Map.empty })
       
   337   }
       
   338 
       
   339   object DiagnosticSeverity
       
   340   {
       
   341     val Error = 1
       
   342     val Warning = 2
       
   343     val Information = 3
       
   344     val Hint = 4
       
   345   }
       
   346 
       
   347   object PublishDiagnostics
       
   348   {
       
   349     def apply(uri: String, diagnostics: List[Diagnostic]): JSON.T =
       
   350       Notification("textDocument/publishDiagnostics",
       
   351         Map("uri" -> uri, "diagnostics" -> diagnostics.map(_.json)))
       
   352   }
   314 }
   353 }