From cca2a72993c4b63c9d82d6c16068ed78aa2fe578 Mon Sep 17 00:00:00 2001
From: Alessio Aurecchia <alessio@aurecchia.ch>
Date: Thu, 31 May 2018 15:40:26 +0200
Subject: [PATCH] Send SymbExLog also when failing.

---
 src/main/scala/viper/server/VerificationWorker.scala | 10 ++++------
 src/main/scala/viper/server/ViperIDEProtocol.scala   |  9 ++-------
 2 files changed, 6 insertions(+), 13 deletions(-)

diff --git a/src/main/scala/viper/server/VerificationWorker.scala b/src/main/scala/viper/server/VerificationWorker.scala
index 3ce302e..c457a8a 100644
--- 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
index 1484c5d..1413362 100644
--- 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] {