From d82a07e20b320b9e6b221b38723b1c41bcc9c2f9 Mon Sep 17 00:00:00 2001
From: SeeBasTStick <sebastian.stock@hhu.de>
Date: Sat, 31 Oct 2020 11:38:04 +0100
Subject: [PATCH] fixed problems with resetting documents + tests

---
 .../b/language/server/BDocumentService.kt     |   8 +-
 src/main/kotlin/b/language/server/Server.kt   |   8 +-
 .../b/language/server/ServerInterface.kt      |  11 ++
 .../server/communication/Communicator.kt      |  16 +-
 .../server/proBMangement/prob/ProBKernel.kt   |   7 +-
 .../proBMangement/BDocumentServiceTest.kt     | 174 ++++++++++++++++++
 .../server/prob2/proBMangement/UtilTest.kt    |   6 +-
 src/test/resources/WD_M1.mch                  |   9 +
 src/test/resources/WD_M2.mch                  |  10 +
 9 files changed, 235 insertions(+), 14 deletions(-)
 create mode 100644 src/main/kotlin/b/language/server/ServerInterface.kt
 create mode 100644 src/test/kotlin/b/language/server/prob2/proBMangement/BDocumentServiceTest.kt
 create mode 100644 src/test/resources/WD_M1.mch
 create mode 100644 src/test/resources/WD_M2.mch

diff --git a/src/main/kotlin/b/language/server/BDocumentService.kt b/src/main/kotlin/b/language/server/BDocumentService.kt
index 3e09911..1c5cb96 100644
--- a/src/main/kotlin/b/language/server/BDocumentService.kt
+++ b/src/main/kotlin/b/language/server/BDocumentService.kt
@@ -7,7 +7,7 @@ import org.eclipse.lsp4j.*
 import org.eclipse.lsp4j.services.TextDocumentService
 import java.util.concurrent.ConcurrentHashMap
 
-class BDocumentService(private val server: Server,
+class BDocumentService(private val server: ServerInterface,
                        private val communicator: CommunicatorInterface,
                        private val proBInterface: ProBInterface) : TextDocumentService {
 
@@ -51,11 +51,10 @@ class BDocumentService(private val server: Server,
 
         clientSettings.thenAccept{ settings ->
             communicator.setDebugMode(settings.debugMode)
-            val prob : ProBInterface = ProBCommandLineAccess(communicator)
             communicator.sendDebugMessage("settings are $settings", MessageType.Info)
 
             try{
-                val diagnostics: List<Diagnostic> = prob.checkDocument(currentUri, settings)
+                val diagnostics: List<Diagnostic> = proBInterface.checkDocument(currentUri, settings)
 
                 val sortedDiagnostic = diagnostics.groupBy { it.source }
                 sortedDiagnostic.forEach { entry -> communicator.publishDiagnostics(entry.key, entry.value)}
@@ -75,6 +74,7 @@ class BDocumentService(private val server: Server,
 
     }
 
+
     /**
      * Gets all uris that are no longer contain problems
      * @param currentUri the uri of the current main file
@@ -95,7 +95,7 @@ class BDocumentService(private val server: Server,
      */
     override fun didClose(params: DidCloseTextDocumentParams?) {
         communicator.sendDebugMessage("document ${params!!.textDocument.uri} was closed - removing meta data", MessageType.Info)
-        server.documentSettings.remove(params.textDocument.uri)
+        server.removeDocumentSettings(params.textDocument.uri)
     }
 
     /**
diff --git a/src/main/kotlin/b/language/server/Server.kt b/src/main/kotlin/b/language/server/Server.kt
index 4820acb..58e6238 100644
--- a/src/main/kotlin/b/language/server/Server.kt
+++ b/src/main/kotlin/b/language/server/Server.kt
@@ -11,7 +11,7 @@ import java.util.concurrent.CompletableFuture
 import kotlin.collections.HashMap
 import kotlin.system.exitProcess
 
-class Server : LanguageServer{
+class Server : LanguageServer, ServerInterface {
 
     private val textDocumentService : TextDocumentService = BDocumentService(this, Communicator, ProBKernelManager(Communicator))
     private val bWorkspaceService : WorkspaceService = BWorkspaceService(this, Communicator)
@@ -77,7 +77,7 @@ class Server : LanguageServer{
      * @param uri the uri of the document requested
      * @return settings of the document requested
      */
-    fun getDocumentSettings(uri : String) : CompletableFuture<Settings> {
+    override fun getDocumentSettings(uri : String) : CompletableFuture<Settings> {
         Communicator.sendDebugMessage("requesting configuration for document: $uri", MessageType.Info)
         return if(!configurationAbility){
             val returnValue = CompletableFuture<Settings>()
@@ -95,6 +95,10 @@ class Server : LanguageServer{
         }
     }
 
+    override fun removeDocumentSettings(uri: String) {
+        documentSettings.remove(uri)
+    }
+
 
 
 
diff --git a/src/main/kotlin/b/language/server/ServerInterface.kt b/src/main/kotlin/b/language/server/ServerInterface.kt
new file mode 100644
index 0000000..49f696c
--- /dev/null
+++ b/src/main/kotlin/b/language/server/ServerInterface.kt
@@ -0,0 +1,11 @@
+package b.language.server
+
+import b.language.server.dataStorage.Settings
+import java.util.concurrent.CompletableFuture
+
+interface ServerInterface {
+
+    fun getDocumentSettings(uri : String) : CompletableFuture<Settings>
+
+    fun removeDocumentSettings(uri : String)
+}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/communication/Communicator.kt b/src/main/kotlin/b/language/server/communication/Communicator.kt
index 4e8e8c3..1465443 100644
--- a/src/main/kotlin/b/language/server/communication/Communicator.kt
+++ b/src/main/kotlin/b/language/server/communication/Communicator.kt
@@ -1,5 +1,6 @@
 package b.language.server.communication
 
+import org.eclipse.lsp4j.Diagnostic
 import org.eclipse.lsp4j.MessageParams
 import org.eclipse.lsp4j.MessageType
 import org.eclipse.lsp4j.PublishDiagnosticsParams
@@ -16,13 +17,15 @@ object Communicator : CommunicatorInterface {
 
     private var debugMode : Boolean = true
 
+
     /**
      * Sends the diagnostics
      *
      * @param diagnostics object containing the Diagnostics
      */
-    override fun publishDiagnostics(diagnostics: PublishDiagnosticsParams) {
-        client.publishDiagnostics(diagnostics)
+    override fun publishDiagnostics(target: String, diagnostics: List<Diagnostic>) {
+        client.publishDiagnostics(PublishDiagnosticsParams(target, diagnostics))
+
     }
 
     /**
@@ -58,4 +61,13 @@ object Communicator : CommunicatorInterface {
     override fun setDebugMode(mode : Boolean){
         debugMode = mode
     }
+
+    /**
+     * Can be used to store a messages until a "sendDebugMessage" command is sent. The messages will be sent as FIFO
+     * @param message the message to send
+     * @param severity tne message severity
+     */
+    override fun bufferDebugMessage(message: String, severity: MessageType) {
+        TODO("Not yet implemented")
+    }
 }
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
index 4f351af..4d19fe4 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
@@ -42,15 +42,16 @@ class ProBKernel @Inject constructor(private val injector : Injector,
      * @return a list with the problems found
      */
     fun check(path : String, settings : ProBSettings) : List<Diagnostic>{
-        Communicator.sendDebugMessage("unloading old machine", MessageType.Info)
+        communicator.sendDebugMessage("unloading old machine", MessageType.Info)
         unloadMachine()
 
+
         val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(path.substringAfterLast(".")))
 
         val informationListener = InformationListener(path)
         animator.addWarningListener(informationListener)
 
-        Communicator.sendDebugMessage("loading new machine", MessageType.Info)
+        communicator.sendDebugMessage("loading new machine", MessageType.Info)
 
         val problems = loadMachine(settings, path, factory)
 
@@ -122,12 +123,14 @@ class ProBKernel @Inject constructor(private val injector : Injector,
      * to clean up a machine
      */
     private fun unloadMachine() {
+
         val oldTrace = animationSelector.currentTrace
         if (oldTrace != null) {
             assert(oldTrace.stateSpace === animator.currentStateSpace)
             animationSelector.changeCurrentAnimation(null)
             oldTrace.stateSpace.kill()
         }
+
     }
 
 
diff --git a/src/test/kotlin/b/language/server/prob2/proBMangement/BDocumentServiceTest.kt b/src/test/kotlin/b/language/server/prob2/proBMangement/BDocumentServiceTest.kt
new file mode 100644
index 0000000..48f5eb6
--- /dev/null
+++ b/src/test/kotlin/b/language/server/prob2/proBMangement/BDocumentServiceTest.kt
@@ -0,0 +1,174 @@
+package b.language.server.prob2.proBMangement
+
+import b.language.server.BDocumentService
+import b.language.server.ServerInterface
+import b.language.server.communication.CommunicatorInterface
+import b.language.server.dataStorage.Settings
+import b.language.server.proBMangement.ProBInterface
+import b.language.server.proBMangement.prob.ProBKernelManager
+import org.eclipse.lsp4j.Diagnostic
+import org.eclipse.lsp4j.MessageType
+import org.junit.jupiter.api.Test
+import java.util.concurrent.CompletableFuture
+import kotlin.test.assertEquals
+import kotlin.test.assertTrue
+
+class BDocumentServiceTest {
+    
+    class DummyCommunicator : CommunicatorInterface{
+
+        val pushedDiagnostics :MutableMap<String, List<Diagnostic>> = mutableMapOf()
+
+
+
+        /**
+         * Sends the diagnostics
+         *
+         * @param diagnostics object containing the Diagnostics
+         */
+        override fun publishDiagnostics(target: String, diagnostics: List<Diagnostic>) {
+            pushedDiagnostics[target] = diagnostics
+        }
+
+        /**
+         * Sends a debug message resulting in a output channel message
+         *
+         * @param message the message to send
+         * @param severity the Severity of the message (Error/Info/Warning)
+         */
+        override fun sendDebugMessage(message: String, severity: MessageType) {
+           // println(message)
+        }
+
+        /**
+         * Sends a popup message resulting in a popup message
+         *
+         * @param message the message to send
+         * @param severity the Severity of the message (Error/Info/Warning)
+         */
+        override fun showMessage(message: String, severity: MessageType) {
+            //void
+        }
+
+        /**
+         * To enable/disable debug mode
+         *
+         * @param mode the new state of the debug mode
+         */
+        override fun setDebugMode(mode: Boolean) {
+
+            //void
+        }
+
+        /**
+         * Can be used to store a messages until a "sendDebugMessage" command is sent. The messages will be sent as FIFO
+         * @param message the message to send
+         * @param severity tne message severity
+         */
+        override fun bufferDebugMessage(message: String, severity: MessageType) {
+            //void
+        }
+
+    }
+
+    class DummyServer : ServerInterface{
+        override fun getDocumentSettings(uri: String): CompletableFuture<Settings> {
+            val result = CompletableFuture<Settings>()
+            result.complete(Settings())
+            return result
+        }
+
+        override fun removeDocumentSettings(uri: String) {
+            TODO("Not yet implemented")
+        }
+
+    }
+
+
+
+    /**
+     * Fakes the behavior of the user by returning no errors when called the second time
+     * The user fixed the errors
+     */
+    class DummyProBKernelManager(val communicator : CommunicatorInterface) : ProBInterface{
+
+        private var counter = 0
+
+        override fun checkDocument(uri: String, settings: Settings): List<Diagnostic> {
+            return if(counter == 0){
+                counter++
+                val realKernel = ProBKernelManager(communicator)
+                realKernel.checkDocument(uri, settings)
+
+            }else{
+                listOf()
+            }
+        }
+
+    }
+
+    @Test
+    fun checkDocument_test_documentRegistered() {
+
+        val communicator = DummyCommunicator()
+
+        val documentService = BDocumentService(DummyServer(), communicator, ProBKernelManager(communicator))
+
+        //Filling the internel state with some information
+        documentService.checkDocument("src/test/resources/WD_M1.mch")
+
+        val targetSet =  communicator.pushedDiagnostics.entries.first().value.map { value -> value.source }.toSet()
+
+
+        assertEquals(1, communicator.pushedDiagnostics.entries.size)
+        assertEquals(2, communicator.pushedDiagnostics.entries.first().value.size)
+        assertTrue(targetSet.first().contains("b-language-server/src/test/resources/WD_M1.mch"))
+
+    }
+
+
+    @Test
+    fun checkDocument_test_subDocument_displayed_properly() {
+
+        val communicator = DummyCommunicator()
+
+        val documentService = BDocumentService(DummyServer(), communicator, ProBKernelManager(communicator))
+
+        //Filling the internel state with some information
+        documentService.checkDocument("src/test/resources/WD_M2.mch")
+
+        communicator.pushedDiagnostics.clear()
+
+        documentService.checkDocument("src/test/resources/WD_M2.mch")
+
+        println(communicator.pushedDiagnostics.size)
+
+        val targetSet =  communicator.pushedDiagnostics.entries.first().value.map { value -> value.source }.toSet()
+
+
+          assertEquals(1, communicator.pushedDiagnostics.entries.size)
+        assertEquals(2, communicator.pushedDiagnostics.entries.first().value.size)
+        assertTrue(targetSet.first().contains("b-language-server/src/test/resources/WD_M1.mch"))
+
+    }
+
+
+
+    @Test
+    fun checkDocument_test_unregistered_document_after_no_errors() {
+
+        val communicator = DummyCommunicator()
+
+        val documentService = BDocumentService(DummyServer(), communicator, DummyProBKernelManager(communicator))
+
+        //Filling the internel state with some information
+        documentService.checkDocument("src/test/resources/WD_M2.mch")
+
+        documentService.checkDocument("src/test/resources/WD_M2.mch")
+
+        println(communicator.pushedDiagnostics)
+        val targetSet =  communicator.pushedDiagnostics.entries.first().value.map { value -> value.source }.toSet()
+
+        assertEquals(emptyList(), communicator.pushedDiagnostics.entries.first().value)
+    }
+}
\ No newline at end of file
diff --git a/src/test/kotlin/b/language/server/prob2/proBMangement/UtilTest.kt b/src/test/kotlin/b/language/server/prob2/proBMangement/UtilTest.kt
index 0eea8cf..7b79c99 100644
--- a/src/test/kotlin/b/language/server/prob2/proBMangement/UtilTest.kt
+++ b/src/test/kotlin/b/language/server/prob2/proBMangement/UtilTest.kt
@@ -12,9 +12,7 @@ import kotlin.test.assertEquals
 
 class UtilTest {
 
-    /**
-     * as we using functional programming we don“t test the logic but the functionality
-     */
+
     @Test
     fun generateErrorItem()
     {
@@ -34,7 +32,7 @@ class UtilTest {
                          Position(endLine-1, endCol)),
                  message, DiagnosticSeverity.Error, file)
 
-        val errorItemAfter = convertErrorItems(listOf(errorItem)).first()
+        val errorItemAfter = convertErrorItems(listOf(errorItem), "dummy").first()
 
         assertEquals(diagnostic, errorItemAfter)
 
diff --git a/src/test/resources/WD_M1.mch b/src/test/resources/WD_M1.mch
new file mode 100644
index 0000000..592f7ef
--- /dev/null
+++ b/src/test/resources/WD_M1.mch
@@ -0,0 +1,9 @@
+MACHINE WD_M1
+CONSTANTS x
+PROPERTIES
+  x:NATURAL &
+  10/x > 1
+VARIABLES v
+INVARIANT v:NAT
+INITIALISATION v:=0
+END
\ No newline at end of file
diff --git a/src/test/resources/WD_M2.mch b/src/test/resources/WD_M2.mch
new file mode 100644
index 0000000..0c1bf62
--- /dev/null
+++ b/src/test/resources/WD_M2.mch
@@ -0,0 +1,10 @@
+MACHINE WD_M2 INCLUDES WD_M1
+CONSTANTS y
+PROPERTIES
+  y:NATURAL &
+  10*y > 1
+VARIABLES w
+INVARIANT w:NAT
+INITIALISATION w:=0
+OPERATIONS inc = BEGIN w:=w+1 END
+END
\ No newline at end of file
-- 
GitLab