added prob2 kernel access and some tests

src/main/kotlin/b/language/server/BDocumentService.kt

 package b.language.server
 
 import b.language.server.communication.CommunicatorInterface
-import b.language.server.proBMangement.probCli.CommandCouldNotBeExecutedException
-import b.language.server.proBMangement.probCli.PathCouldNotBeCreatedException
-import b.language.server.proBMangement.probCli.ProBCommandLineAccess
+import b.language.server.proBMangement.ProBFactory
 import b.language.server.proBMangement.ProBInterface
 import org.eclipse.lsp4j.*
 import org.eclipse.lsp4j.services.TextDocumentService
 import java.io.IOException
 import java.util.concurrent.ConcurrentHashMap
 
-class BDocumentService(private val server: Server, private val communicator: CommunicatorInterface) : TextDocumentService {
+class BDocumentService(private val server: Server,
+                       private val communicator: CommunicatorInterface,
+                       private val proBFactory: ProBFactory = ProBFactory()) : TextDocumentService {
 
     private val documents = ConcurrentHashMap<String, String>()
     private val issueTracker : ConcurrentHashMap<String, Set<String>> = ConcurrentHashMap()
@@ -43,7 +43,7 @@ class BDocumentService(private val server: Server, private val communicator: Com
 
     /**
      * checks a document via prob an the set options
-     * @param the uri to perform actions on
+     * @param currentUri uri to perform actions on
      */
     fun checkDocument(currentUri : String){
 
@@ -52,7 +52,7 @@ class BDocumentService(private val server: Server, private val communicator: Com
 
         clientSettings.thenAccept{ settings ->
             communicator.setDebugMode(settings.debugMode)
-            val prob : ProBInterface = ProBCommandLineAccess(communicator)
+            val prob : ProBInterface = proBFactory.getProBAccess(communicator)
             communicator.sendDebugMessage("settings are $settings", MessageType.Info)
 
             try{
@@ -64,12 +64,6 @@ class BDocumentService(private val server: Server, private val communicator: Com
                 invalidFiles.forEach{uri -> communicator.publishDiagnostics(PublishDiagnosticsParams(uri, listOf()))}
                 communicator.sendDebugMessage("invalidating old files $invalidFiles", MessageType.Info)
                 issueTracker[currentUri] = filesWithProblems.toSet()
-            }catch (e : PathCouldNotBeCreatedException){
-                communicator.sendDebugMessage("error path could not be created", MessageType.Info)
-                communicator.showMessage(e.message!!, MessageType.Error)
-            }catch (e : CommandCouldNotBeExecutedException){
-                communicator.sendDebugMessage("command could not be executed", MessageType.Info)
-                communicator.showMessage(e.message!!, MessageType.Error)
             }catch (e : IOException){
                 communicator.sendDebugMessage("command could not be executed", MessageType.Info)
                 communicator.showMessage(e.message!!, MessageType.Error)

src/main/kotlin/b/language/server/Server.kt

@@ -5,12 +5,10 @@ import b.language.server.dataStorage.Settings
 import com.google.gson.JsonObject
 import org.eclipse.lsp4j.*
 import org.eclipse.lsp4j.jsonrpc.messages.Either
-import org.eclipse.lsp4j.jsonrpc.services.JsonNotification
 import org.eclipse.lsp4j.services.*
 import java.util.concurrent.CompletableFuture
 import kotlin.collections.HashMap
 import kotlin.system.exitProcess
-import org.eclipse.lsp4j.jsonrpc.services.GenericEndpoint
 
 class Server : LanguageServer{
 

src/main/kotlin/b/language/server/proBMangement/ProBFactory.kt

+package b.language.server.proBMangement
+
+import b.language.server.communication.CommunicatorInterface
+import b.language.server.proBMangement.prob2.ProBKernelManager
+
+
+/**
+ * Generate new Instances of ProBKernelManger
+ */
+class ProBFactory {
+
+    fun getProBAccess(commuicator : CommunicatorInterface) : ProBInterface{
+        return ProBKernelManager(commuicator)
+    }
+
+}
\ No newline at end of file

src/main/kotlin/b/language/server/proBMangement/ProBInterface.kt

@@ -8,8 +8,9 @@ interface ProBInterface {
     /**
      * Checks the given document with the help of ProB
      * @param uri the source to check
+     * @param settings the settings for this document
      * @return a list of all problems found
      */
-    abstract fun checkDocument(uri : String, settings: Settings) : List<Diagnostic>
+    fun checkDocument(uri : String, settings: Settings) : List<Diagnostic>
 
 }
\ No newline at end of file

src/main/kotlin/b/language/server/proBMangement/WrongPathException.kt

+package b.language.server.proBMangement
+
+class WrongPathException (message: String?) : Exception(message)
\ No newline at end of file

src/main/kotlin/b/language/server/proBMangement/prob2/MyWarningListener.kt

@@ -13,6 +13,6 @@ class MyWarningListener : IWarningListener {
     }
 
     fun getWarnings() : List<Diagnostic>{
-        return convertErrorItems(warningList, DiagnosticSeverity.Warning)
+        return convertErrorItems(warningList)
     }
 }
\ No newline at end of file

src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernel.kt

 
+import b.language.server.communication.Communicator
 import b.language.server.dataStorage.ProBSettings
 import b.language.server.proBMangement.prob2.MyWarningListener
 import b.language.server.proBMangement.prob2.convertErrorItems
@@ -14,14 +15,40 @@ import de.prob.statespace.AnimationSelector
 import de.prob.statespace.StateSpace
 import de.prob.statespace.Trace
 import org.eclipse.lsp4j.Diagnostic
-import org.eclipse.lsp4j.DiagnosticSeverity
+import org.eclipse.lsp4j.MessageType
 import java.io.IOException
-import java.nio.file.Paths
 
 
 class ProBKernel @Inject constructor(private val injector : Injector, val classicalBFactory : ClassicalBFactory,
                                      private val animationSelector: AnimationSelector, private val animator : ReusableAnimator) {
 
+    private val communicator : Communicator = Communicator
+
+    fun check(path : String, settings : ProBSettings) : List<Diagnostic>{
+        communicator.sendDebugMessage("Unload old machine", MessageType.Info)
+        unloadMachine()
+        val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(path.substringAfterLast(".")))
+        val warningListener = MyWarningListener()
+        animator.addWarningListener(warningListener)
+        val parseErrors = mutableListOf<Diagnostic>()
+        communicator.sendDebugMessage("Load new machine", MessageType.Info)
+        loadMachine(
+                java.util.function.Function { stateSpace : StateSpace ->
+                    try {
+                        val extractedModel = factory.extract(path)
+                        val stateSpaceWithSettings = extractedModel.load(prepareAdditionalSettings(settings))
+                        extractedModel.loadIntoStateSpace(stateSpaceWithSettings)
+                    } catch (e: IOException) {
+                        throw RuntimeException(e)
+                    } catch (e: ModelTranslationError) {
+                        throw RuntimeException(e)
+                    }catch (e : ProBError){
+                        parseErrors.addAll(convertErrorItems(e.errors))
+                    }
+                    Trace(stateSpace)
+                }, settings)
+        return listOf(warningListener.getWarnings(), parseErrors).flatten()
+    }
 
     private fun loadMachine(newTraceCreator :java.util.function.Function<StateSpace, Trace>, settings: ProBSettings){
         val newStateSpace = animator.createStateSpace()
@@ -35,7 +62,7 @@ class ProBKernel @Inject constructor(private val injector : Injector, val classi
     }
 
     private fun executeAdditionalOptions(settings : ProBSettings){
-        val newStateSpace = animator.createStateSpace()
+        animator.createStateSpace()
         if(settings.wdChecks){
             animator.execute(CheckWellDefinednessCommand())
         }
@@ -51,30 +78,8 @@ class ProBKernel @Inject constructor(private val injector : Injector, val classi
         }
     }
 
-    fun check(path : String, settings : ProBSettings) : List<Diagnostic>{
-        unloadMachine()
-        val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(path.substringAfterLast(".")))
-        val warningListener = MyWarningListener()
-        animator.addWarningListener(warningListener)
-        val parseErrors = mutableListOf<Diagnostic>()
-        loadMachine(
-                java.util.function.Function { stateSpace : StateSpace ->
-                    try {
-                        factory.extract(path).load(prepareAdditionalSettings(settings))
-                        loadIntoStateSpace(stateSpace)
-                    } catch (e: IOException) {
-                        throw RuntimeException(e)
-                    } catch (e: ModelTranslationError) {
-                        throw RuntimeException(e)
-                    }catch (e : ProBError){
-                        parseErrors.addAll(convertErrorItems(e.errors))
-                    }
-                    Trace(stateSpace)
-                }, settings)
-        return listOf(warningListener.getWarnings(), parseErrors).flatten()
-    }
 
-    fun prepareAdditionalSettings(proBSettings: ProBSettings): MutableMap<String, String> {
+    private fun prepareAdditionalSettings(proBSettings: ProBSettings): MutableMap<String, String> {
         val settings = mutableMapOf<String, String>()
         if(proBSettings.performanceHints) {
             settings["STRICT_CLASH_CHECKING"] = "TRUE"

src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelManager.kt

 package b.language.server.proBMangement.prob2
 
 import ProBKernel
+import b.language.server.communication.Communicator
+import b.language.server.communication.CommunicatorInterface
 import b.language.server.dataStorage.ProBSettings
 import b.language.server.dataStorage.Settings
 import b.language.server.proBMangement.ProBInterface
+import b.language.server.proBMangement.WrongPathException
 import com.google.inject.Guice
 import com.google.inject.Stage
 import org.eclipse.lsp4j.Diagnostic
+import org.eclipse.lsp4j.MessageType
 
 /**
  * Setup a connection to ProB2 Kernel
  */
-class ProBKernelManager : ProBInterface{
+class ProBKernelManager(private val communicator : CommunicatorInterface) : ProBInterface{
 
     private lateinit var kernel : ProBKernel
+    private var lastProBHome : String = "DEFAULT"
 
     /**
      * Checks the given document with the help of ProB
      * @param uri the source to check
+     * @param settings the settings for this document
      * @return a list of all problems found
      */
     override fun checkDocument(uri: String, settings: Settings): List<Diagnostic> {
         val proBSettings = ProBSettings(settings.wdChecks, settings.strictChecks, settings.performanceHints)
         val probHome = settings.probHome.absolutePath
 
-        if(probHome != "DEFAULT" && !this::kernel.isInitialized)
-        {
+        communicator.sendDebugMessage("checking document", MessageType.Info)
+
+        return if(probHome == lastProBHome && this::kernel.isInitialized){
+            kernel.check(uri, proBSettings)
+        }else{
+            lastProBHome = probHome
+            setup(probHome).check(uri, proBSettings)
+        }
+
+    }
+
+    /**
+     * @param probHome the home of prob; DEFAULT for the prob version delivered with the library
+     * @return an instance of prob kernel
+     */
+    fun setup(probHome : String) : ProBKernel{
         if(probHome != "DEFAULT"){
             System.setProperty("prob.home", probHome)
+            communicator.sendDebugMessage("$probHome selected", MessageType.Info)
+        }else{
+            communicator.sendDebugMessage("default prob selected", MessageType.Info)
         }
+
         val injector = Guice.createInjector(Stage.PRODUCTION, ProBKernelModule())
+        val kernel : ProBKernel
+        try{
             kernel = injector.getInstance(ProBKernel::class.java)
+        }catch (e : de.prob.exception.CliError){
+            communicator.sendDebugMessage("wrong path to prob", MessageType.Error)
+            throw WrongPathException("wrong path to prob $probHome")
         }
-
-        return kernel.check(uri, proBSettings)
+        return kernel
     }
 
 

src/test/kotlin/b/language/server/ProBCommandLineTest.kt

@@ -3,7 +3,6 @@ package b.language.server
 import b.language.server.dataStorage.Position
 import b.language.server.dataStorage.Problem
 import b.language.server.dataStorage.Settings
-import b.language.server.proBMangement.probCli.ProBCommandLineAccess
 import com.google.gson.Gson
 import org.eclipse.lsp4j.Diagnostic
 import org.eclipse.lsp4j.DiagnosticSeverity
@@ -15,7 +14,7 @@ import kotlin.test.assertEquals
 import kotlin.test.assertTrue
 
 class ProBCommandLineTest{
-
+    /*
     @Test
     fun test_readProblems(@TempDir tempPath : File = File("tmp"))
     {
@@ -191,6 +190,6 @@ class ProBCommandLineTest{
         val result = ProBCommandLineAccess().createFolder(errorDict, errorPath)
         assertTrue(result)
     }
-
+*/
 
 }
\ No newline at end of file

src/test/kotlin/b/language/server/communication/DummyCommunication.kt

+package b.language.server.communication
+
+import b.language.server.communication.CommunicatorInterface
+import org.eclipse.lsp4j.MessageType
+import org.eclipse.lsp4j.PublishDiagnosticsParams
+
+
+/**
+ * The Communicator is a side effect class, we don´t want side effects in out tests; especially such that are for
+ * debug purpose only
+ */
+class DummyCommunication : CommunicatorInterface {
+
+    val outputCollector = mutableListOf<String>()
+
+    /**
+     * Sends the diagnostics
+     *
+     * @param diagnostics object containing the Diagnostics
+     */
+    override fun publishDiagnostics(diagnostics: PublishDiagnosticsParams) {}
+
+    /**
+     * 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) {
+        outputCollector.add(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) {}
+
+    /**
+     * To enable/disable debug mode
+     *
+     * @param mode the new state of the debug mode
+     */
+    override fun setDebugMode(mode: Boolean) {
+
+    }
+}
\ No newline at end of file

src/test/kotlin/b/language/server/prob2/proBMangement/ProBKernelManagerTest.kt

+package b.language.server.prob2.proBMangement
+
+import b.language.server.communication.DummyCommunication
+import b.language.server.proBMangement.WrongPathException
+import b.language.server.proBMangement.prob2.ProBKernelManager
+import org.junit.jupiter.api.Assertions
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.assertThrows
+import org.junit.jupiter.api.function.Executable
+import kotlin.test.assertEquals
+
+class ProBKernelManagerTest {
+
+    @Test
+    fun testCorrectBaseSetup(){
+        val dummyCommunication = DummyCommunication()
+        val proBKernelManager = ProBKernelManager(dummyCommunication)
+
+        proBKernelManager.setup("DEFAULT")
+
+        assertEquals(listOf("default prob selected"), dummyCommunication.outputCollector)
+    }
+
+
+    @Test
+    fun testCorrectBaseSetupWrongPath(){
+        val dummyCommunication = DummyCommunication()
+        val proBKernelManager = ProBKernelManager(dummyCommunication)
+
+        Assertions.assertThrows(WrongPathException::class.java) { proBKernelManager.setup("NOTDEFAULT") }
+    }
+
+    @Test
+    fun testCheckDocument(){
+
+    }
+}
\ No newline at end of file