Send SymbExLog also when failing.

viperproject · May 31, 2018 · cca2a72 · cca2a72
1 parent 674445c
commit cca2a72
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 13 deletions.
diff --git a/src/main/scala/viper/server/VerificationWorker.scala b/src/main/scala/viper/server/VerificationWorker.scala
@@ -272,15 +272,13 @@ class ViperBackend(private val _frontend: SilFrontend) {
         //printSuccess();
         _frontend.reporter.report(OverallSuccessMessage(_frontend.getVerifierName, System.currentTimeMillis() - _frontend.startTime))
         // TODO: Think again about where to detect and trigger SymbExLogging
-        if (SymbExLogger.enabled) {
-          _frontend.reporter.report(SymbExLogReport(System.currentTimeMillis(), Some(SymbExLogger.toJSString())))
-        }
       case f@Failure(_) =>
         //printErrors(errors: _*);
         _frontend.reporter.report(OverallFailureMessage(_frontend.getVerifierName, System.currentTimeMillis() - _frontend.startTime, f))
-        if (SymbExLogger.enabled) {
-          _frontend.reporter.report(SymbExLogReport(System.currentTimeMillis(), None))
-        }
+    }
+
+    if (SymbExLogger.enabled) {
+      _frontend.reporter.report(SymbExLogReport(System.currentTimeMillis(), SymbExLogger.toJSString()))
     }
   }
 

diff --git a/src/main/scala/viper/server/ViperIDEProtocol.scala b/src/main/scala/viper/server/ViperIDEProtocol.scala
@@ -206,13 +206,8 @@ object ViperIDEProtocol extends akka.http.scaladsl.marshallers.sprayjson.SprayJs
     override def write(obj: SymbExLogReport) = JsObject(
       //"entity" -> obj.entity.toJson,
       "timestamp" -> obj.timestamp.toJson,
-      obj.stuff match {
-        case Some(stuff) =>
-          //"stuff" -> JsString(s"<json transformer not implemented for attachment ${stuff.toString}>")
-          "stuff" -> JsString(stuff.toString)
-        case _ =>
-          "stuff" -> JsString(s"<empty attachment>")
-      })
+      "log" -> JsString(obj.log)
+    )
   })
 
   implicit val stackTraceElement_writer: RootJsonFormat[StackTraceElement] = lift(new RootJsonWriter[java.lang.StackTraceElement] {