Merge pull request #156 from viperproject/meilers_lsp_warnings

Fixed handling of warnings
viperproject · Jul 17, 2023 · e6ef7b8 · e6ef7b8
2 parents 7592927 + 29c9294
commit e6ef7b8
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 3 deletions.
diff --git a/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala b/src/main/scala/viper/server/frontends/http/jsonWriters/ViperIDEProtocol.scala
@@ -438,6 +438,10 @@ object ViperIDEProtocol extends akka.http.scaladsl.marshallers.sprayjson.SprayJs
     override def write(obj: WarningsDuringTypechecking): JsArray = JsArray(obj.warnings.map(_.asInstanceOf[AbstractError].toJson).toVector)
   })
 
+  implicit val warningsDuringVerification_writer: RootJsonFormat[WarningsDuringVerification] = lift(new RootJsonWriter[WarningsDuringVerification] {
+    override def write(obj: WarningsDuringVerification): JsArray = JsArray(obj.warnings.map(_.asInstanceOf[AbstractError].toJson).toVector)
+  })
+
   implicit val simpleMessage_writer: RootJsonFormat[SimpleMessage] = lift(new RootJsonWriter[SimpleMessage] {
     override def write(obj: SimpleMessage): JsObject = JsObject("text" -> JsString(obj.text))
   })

diff --git a/src/main/scala/viper/server/frontends/lsp/FileManager.scala b/src/main/scala/viper/server/frontends/lsp/FileManager.scala
@@ -216,6 +216,15 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
       case InvalidArgumentsReport(_, errors) =>
         markErrorsAsReported(errors)
         processErrors(backendClassName, errors, Some(s"Invalid arguments have been passed to the backend $backendClassName:"))
+      case WarningsDuringParsing(warnings) =>
+        markErrorsAsReported(warnings)
+        processErrors(backendClassName, warnings)
+      case WarningsDuringTypechecking(warnings) =>
+        markErrorsAsReported(warnings)
+        processErrors(backendClassName, warnings)
+      case WarningsDuringVerification(warnings) =>
+        markErrorsAsReported(warnings)
+        processErrors(backendClassName, warnings)
       case EntitySuccessMessage(_, concerning, _, _) =>
         if (progress == null) {
           coordinator.logger.debug("The backend must send a VerificationStart message before the ...Verified message.")
@@ -243,7 +252,7 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
         val newErrors = failure.errors.filterNot(hasAlreadyBeenReported)
         markErrorsAsReported(newErrors)
         processErrors(backendClassName, newErrors)
-      // the completion handler is not yet invoked (but as part of Status.Success)
+        // the completion handler is not yet invoked (but as part of Status.Success)
       case m: Message => coordinator.client.notifyUnhandledViperServerMessage(UnhandledViperServerMessageTypeParams(m.name, m.toString, LogLevel.Info.id))
       case Status.Success =>
         // Success is sent when the stream is completed
@@ -258,13 +267,23 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
     private def processErrors(backendClassName: String, errors: Seq[AbstractError], errorMsgPrefix: Option[String] = None): Unit = {
       val diags = errors.map(err => {
         var errorType: String = ""
+        var severity = DiagnosticSeverity.Error
         if (err.fullId != null && err.fullId == "typechecker.error") {
           typeCheckingCompleted = false
           errorType = "Typechecker error"
         } else if (err.fullId != null && err.fullId == "parser.error") {
           parsingCompleted = false
           typeCheckingCompleted = false
           errorType = "Parser error"
+        } else if (err.fullId != null && err.fullId == "typechecker.warning") {
+          severity = DiagnosticSeverity.Warning
+          errorType = "Typechecker warning"
+        } else if (err.fullId != null && err.fullId == "parser.warning") {
+          severity = DiagnosticSeverity.Warning
+          errorType = "Parser warning"
+        } else if (err.fullId != null && err.fullId == "verifier.warning") {
+          severity = DiagnosticSeverity.Warning
+          errorType = "Verification warning"
         } else {
           errorType = "Verification error"
         }
@@ -287,9 +306,8 @@ class FileManager(coordinator: ClientCoordinator, file_uri: String)(implicit exe
           s"${if(err.fullId != null) "[" + err.fullId + "] " else ""}" +
           s"${range.getStart.getLine + 1}:${range.getStart.getCharacter + 1} $errMsgPrefixWithWhitespace${err.readableMessage}s")
 
-
         val cachFlag: String = if(err.cached) "(cached)" else ""
-        new Diagnostic(range, errMsgPrefixWithWhitespace + err.readableMessage + cachFlag, DiagnosticSeverity.Error, "")
+        new Diagnostic(range, errMsgPrefixWithWhitespace + err.readableMessage + cachFlag, severity, "")
       })
 
       diagnostics.appendAll(diags)