diff --git a/src/main/kotlin/b/language/server/BDocumentService.kt b/src/main/kotlin/b/language/server/BDocumentService.kt
index 3e09911c7f120f84a59a4fa8d86a18e8c2c729b1..1c5cb9608a1fc401a4f188f0d9c77e006bf7a468 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 4820acbcce74adcae54c6ec2ac99e422d03ebb8e..58e6238afdb9382fb3e2eed76d02bd7372e0b202 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 0000000000000000000000000000000000000000..49f696c0b255cf02551f6a279613d6fc006766c3
--- /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 4e8e8c3eab8cdf618a65a7b72961547ed60876c8..1465443764aa88bb7d87673ec8bb6153470adfbb 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 4f351af266b9272f2f30e8a070f5b7228ad8a190..4d19fe466ba7f9c0e46ad9b10aa63fb700ce4c93 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 0000000000000000000000000000000000000000..48f5eb642d30f1d767336c9bf0bb101c2785b657
--- /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 0eea8cf11c1a91a295309e6f67f06cda0e611535..7b79c998dd92ced12cb207d128bc63696521dddf 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 0000000000000000000000000000000000000000..592f7efdd8bd29ef4199b9213fe29e3273030dc8
--- /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 0000000000000000000000000000000000000000..0c1bf62e795537a1572b0f80f71cbf390309e73d
--- /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