changed file handling to use File and fixed output location

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

@@ -5,6 +5,7 @@ import b.language.server.proBMangement.ProBInterface
 import b.language.server.proBMangement.prob.CouldNotFindProBHomeException
 import org.eclipse.lsp4j.*
 import org.eclipse.lsp4j.services.TextDocumentService
+import java.io.File
 import java.net.URI
 import java.util.concurrent.ConcurrentHashMap
 
@@ -35,20 +36,20 @@ class BDocumentService(private val server: ServerInterface,
      */
     override fun didSave(params: DidSaveTextDocumentParams?) {
 
-        communicator.sendDebugMessage("document ${params!!.textDocument.uri} was saved", MessageType.Info)
-        checkDocument(URI(params.textDocument.uri))
+        communicator.sendDebugMessage("document ${File(URI(params!!.textDocument.uri).path)} was saved", MessageType.Info)
+        checkDocument(File(URI(params.textDocument.uri).path))
 
     }
 
     /**
      * checks a document via prob and the set options
-     * @param currentUri the uri to perform actions on
+     * @param file the uri to perform actions on
      */
-    fun checkDocument(currentUri : URI){
+    fun checkDocument(file : File){
 
 
 
-        val clientSettings = server.getDocumentSettings(currentUri.path)
+        val clientSettings = server.getDocumentSettings(file.absolutePath)
         communicator.sendDebugMessage("waiting for document settings", MessageType.Info)
 
         clientSettings.thenAccept{ settings ->
@@ -56,21 +57,22 @@ class BDocumentService(private val server: ServerInterface,
             communicator.sendDebugMessage("settings are $settings", MessageType.Info)
 
             try{
-                val diagnostics: List<Diagnostic> = proBInterface.checkDocument(currentUri, settings)
+                val diagnostics: List<Diagnostic> = proBInterface.checkDocument(file, settings)
 
                 val sortedDiagnostic = diagnostics.groupBy { it.source }
                 sortedDiagnostic.forEach { entry -> communicator.publishDiagnostics(entry.key, entry.value)}
                 communicator.showMessage("Evaluation done: ${diagnostics.size} problem(s)", MessageType.Log)
 
                 val filesWithProblems = sortedDiagnostic.keys.toList()
-                val invalidFiles = calculateToInvalidate(currentUri.path, filesWithProblems)
+                val invalidFiles = calculateToInvalidate(file, filesWithProblems)
                 invalidFiles.forEach{uri -> communicator.publishDiagnostics(uri, listOf())}
                 communicator.sendDebugMessage("invalidating old files $invalidFiles", MessageType.Info)
-                issueTracker[currentUri.path] = filesWithProblems.toSet()
+                issueTracker[file.absolutePath] = filesWithProblems.toSet()
 
             }catch (e : CouldNotFindProBHomeException){
-                communicator.sendDebugMessage(e.message!!, MessageType.Info)
-                communicator.showMessage(e.message, MessageType.Error)
+                
+                communicator.sendDebugMessage(e.localizedMessage, MessageType.Info)
+                communicator.showMessage(e.localizedMessage, MessageType.Error)
             }
         }
 
@@ -79,11 +81,11 @@ class BDocumentService(private val server: ServerInterface,
 
     /**
      * Gets all uris that are no longer contain problems
-     * @param currentUri the uri of the current main file
+     * @param file the uri of the current main file
      * @param filesWithProblems uris of files containing problems
      */
-    private fun calculateToInvalidate(currentUri : String, filesWithProblems : List<String>) : List<String>{
-        val currentlyDisplayed = issueTracker[currentUri].orEmpty()
+    private fun calculateToInvalidate(file : File, filesWithProblems : List<String>) : List<String>{
+        val currentlyDisplayed = issueTracker[file.absolutePath].orEmpty()
         return currentlyDisplayed.subtract(filesWithProblems).toList()
     }
 
@@ -96,8 +98,8 @@ class BDocumentService(private val server: ServerInterface,
      * Registration Options: TextDocumentRegistrationOptions
      */
     override fun didClose(params: DidCloseTextDocumentParams?) {
-        communicator.sendDebugMessage("document ${params!!.textDocument.uri} was closed - removing meta data", MessageType.Info)
-        server.removeDocumentSettings(params.textDocument.uri)
+        communicator.sendDebugMessage("document ${URI(params!!.textDocument.uri).path} was closed - removing meta data", MessageType.Info)
+        server.removeDocumentSettings((URI(params.textDocument.uri).path))
     }
 
     /**
@@ -107,8 +109,9 @@ class BDocumentService(private val server: ServerInterface,
      * Registration Options: TextDocumentChangeRegistrationOptions
      */
     override fun didChange(params: DidChangeTextDocumentParams?) {
-        communicator.sendDebugMessage("document ${params!!.textDocument.uri} was changed", MessageType.Info)
-        checkDocument(URI(params.textDocument.uri))
+
+        communicator.sendDebugMessage("document ${URI(params!!.textDocument.uri).path} was changed", MessageType.Info)
+        checkDocument(File(URI(params.textDocument.uri).path))
     }
 
 }
\ No newline at end of file

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

@@ -2,16 +2,16 @@ package b.language.server.proBMangement
 
 import b.language.server.dataStorage.Settings
 import org.eclipse.lsp4j.Diagnostic
-import java.net.URI
+import java.io.File
 
 interface ProBInterface {
 
     /**
      * Checks the given document with the help of ProB
-     * @param uri the source to check
+     * @param file the source to check
      * @param settings the settings for this document
      * @return a list of all problems found
      */
-    fun checkDocument(uri : URI, settings: Settings) : List<Diagnostic>
+    fun checkDocument(file : File, settings: Settings) : List<Diagnostic>
 
 }
\ No newline at end of file

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

@@ -14,8 +14,9 @@ import de.prob.scripting.ModelFactory
 import de.prob.statespace.AnimationSelector
 import org.eclipse.lsp4j.Diagnostic
 import org.eclipse.lsp4j.MessageType
+import java.io.File
 import java.io.IOException
-import java.net.URI
+import java.lang.Exception
 
 /**
  * Represents the interface to communicate with prob kernel
@@ -30,24 +31,22 @@ class ProBKernel @Inject constructor(private val injector : Injector,
 
     /**
      * Checks the given machine file; prepares all necessary object
-     * @param path the file to check
+     * @param file the file to check
      * @param settings the settings under which the check takes place
      * @return a list with the problems found
      */
-    fun check(path : URI, settings : ProBSettings) : List<Diagnostic>{
+    fun check(file : File, settings : ProBSettings) : List<Diagnostic>{
         communicator.sendDebugMessage("unloading old machine", MessageType.Info)
         unloadMachine()
 
+        val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(file.absolutePath.substringAfterLast(".")))
 
-
-        val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(path.path.substringAfterLast(".")))
-
-        val informationListener = InformationListener(path.path)
+        val informationListener = InformationListener(file, communicator)
         animator.addWarningListener(informationListener)
 
         communicator.sendDebugMessage("loading new machine", MessageType.Info)
 
-        val problems = loadMachine(settings, path, factory)
+        val problems = loadMachine(settings, file, factory)
 
         communicator.sendDebugMessage("returning from kernel problems are $problems", MessageType.Info)
 
@@ -57,10 +56,10 @@ class ProBKernel @Inject constructor(private val injector : Injector,
     /**
      * Does the main work
      * @param settings the settings of the document
-     * @param path the path to the document
+     * @param file the path to the document
      * @param factory a factory
      */
-    private fun loadMachine(settings: ProBSettings, path : URI, factory : ModelFactory<*>): List<Diagnostic> {
+    private fun loadMachine(settings: ProBSettings, file : File, factory : ModelFactory<*>): List<Diagnostic> {
         communicator.sendDebugMessage("creating new state space", MessageType.Info)
 
         val newStateSpace = animator.createStateSpace()
@@ -70,7 +69,7 @@ class ProBKernel @Inject constructor(private val injector : Injector,
         val errors = mutableListOf<ErrorItem>()
 
         try {
-            factory.extract(path.path).loadIntoStateSpace(newStateSpace)
+            factory.extract(file.absolutePath).loadIntoStateSpace(newStateSpace)
         } catch (e: IOException) {
             communicator.sendDebugMessage("IOException ${e.message}", MessageType.Info)
         } catch (e : ProBError){
@@ -96,7 +95,14 @@ class ProBKernel @Inject constructor(private val injector : Injector,
 
         communicator.sendDebugMessage("processing errors", MessageType.Info)
         newStateSpace.kill()
-        return convertErrorItems(errors, path.path)
+        var bla : List<Diagnostic> = emptyList()
+        try {
+            bla = convertErrorItems(errors, file, communicator)
+        }catch (e : Exception){
+            println(e)
+        }
+
+        return bla
     }
 
 

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

@@ -9,7 +9,6 @@ import com.google.inject.Stage
 import org.eclipse.lsp4j.Diagnostic
 import org.eclipse.lsp4j.MessageType
 import java.io.File
-import java.net.URI
 
 /**
  * Creates the prob kernel access and maintenance
@@ -71,13 +70,13 @@ class ProBKernelManager(private val communicator : CommunicatorInterface) : ProB
 
     /**
      * Checks the given document with the help of ProB
-     * @param uri the source to check
+     * @param file the source to check
      * @param settings the settings for this document
      * @return a list of all problems found
      *
      * @throws CouldNotFindProBHomeException the given path ist not "DEFAULT" and wrong
      */
-    override fun checkDocument(uri: URI, settings: Settings): List<Diagnostic> {
+    override fun checkDocument(file : File, settings: Settings): List<Diagnostic> {
 
         communicator.sendDebugMessage("try to use ${settings.probHome} as prob version instead of " + System.getProperty("prob.home"), MessageType.Info)
         val result = checkProBVersionSetting(settings.probHome)
@@ -88,7 +87,7 @@ class ProBKernelManager(private val communicator : CommunicatorInterface) : ProB
 
         communicator.sendDebugMessage("success!", MessageType.Info)
         communicator.sendDebugMessage("checking document", MessageType.Info)
-        return kernel.check(uri, ProBSettings(wdChecks = settings.wdChecks, strictChecks = settings.strictChecks,
+        return kernel.check(file, ProBSettings(wdChecks = settings.wdChecks, strictChecks = settings.strictChecks,
                 performanceHints = settings.performanceHints))
     }
 }
\ No newline at end of file

src/main/kotlin/b/language/server/proBMangement/prob/Util.kt

 package b.language.server.proBMangement.prob
 
+import b.language.server.communication.CommunicatorInterface
 import de.prob.animator.domainobjects.ErrorItem
-import org.eclipse.lsp4j.Diagnostic
-import org.eclipse.lsp4j.DiagnosticSeverity
-import org.eclipse.lsp4j.Position
-import org.eclipse.lsp4j.Range
+import org.eclipse.lsp4j.*
 import java.io.File
 
-fun convertErrorItems(errorItems: List<ErrorItem>, currentLoadedFile : String) : List<Diagnostic>{
+
+fun convertErrorItems(errorItems: List<ErrorItem>, currentLoadedFile: File, communicator: CommunicatorInterface) : List<Diagnostic>{
     return  errorItems.map { errorItem ->
         errorItem.locations.map { location ->
-            println(location.filename)
+
+            communicator.sendDebugMessage( File(location.filename).toURI().path, MessageType.Warning)
             Diagnostic(Range(
                     Position(location.startLine - 1, location.startColumn),
                     Position(location.endLine - 1, location.endColumn)),
                     errorItem.message,
                     getErrorItemType(errorItem.type),
-                    separatorToSystems(location.filename))
+
+                File(location.filename).toURI().path)
 
         }.ifEmpty { //Fallback when errors from prob do not have position infos
             listOf(Diagnostic(Range(
@@ -24,27 +25,11 @@ fun convertErrorItems(errorItems: List<ErrorItem>, currentLoadedFile : String) :
                     Position(0,0)),
                     errorItem.message,
                     getErrorItemType(errorItem.type),
-                    separatorToSystems(File(currentLoadedFile).absolutePath)))
+               File(currentLoadedFile.absolutePath).toURI().path))
         }
     }.flatten()
 }
 
-/**
- * ProB spits path out in linux writing which is okay, if we have only one root. However, in windows we can have multiple
- * roots. The path needs then to be normalized for the given OS
- *
- * @param path the path to normalize
- */
-fun separatorToSystems(path : String) : String{
-    return if (File.separatorChar=='\\') {
-        // From Windows to Linux/Mac
-        path.replace('/', File.separatorChar);
-    } else {
-        // From Linux/Mac to Windows
-        path.replace('\\', File.separatorChar);
-    }
-
-}
 
 fun getErrorItemType(errorItem: ErrorItem.Type) : DiagnosticSeverity{
     return when(errorItem){

src/main/kotlin/b/language/server/proBMangement/prob/WarningListener.kt

 package b.language.server.proBMangement.prob
 
+import b.language.server.communication.CommunicatorInterface
 import de.prob.animator.IWarningListener
 import de.prob.animator.domainobjects.ErrorItem
 import org.eclipse.lsp4j.Diagnostic
+import java.io.File
 
 /**
  * Custom collector to collect warnings from prob kernel
  */
-class InformationListener(private val fallbackPath : String) : IWarningListener {
+class InformationListener(private val fallbackPath : File, private val communicator : CommunicatorInterface) : IWarningListener {
     private val warningList : ArrayList<ErrorItem> = arrayListOf()
 
 
@@ -16,6 +18,6 @@ class InformationListener(private val fallbackPath : String) : IWarningListener
     }
 
     fun getInformation() : List<Diagnostic>{
-        return convertErrorItems(warningList, fallbackPath)
+        return convertErrorItems(warningList, fallbackPath, communicator)
     }
 }
\ No newline at end of file

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

 package b.language.server.prob2.proBMangement
 
+import DummyCommunicator
 import b.language.server.BDocumentService
 import b.language.server.ServerInterface
 import b.language.server.communication.CommunicatorInterface
@@ -7,70 +8,13 @@ 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.io.File
-import java.net.URI
 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> {
@@ -95,11 +39,11 @@ class BDocumentServiceTest {
 
         private var counter = 0
 
-        override fun checkDocument(uri: URI, settings: Settings): List<Diagnostic> {
+        override fun checkDocument(file: File, settings: Settings): List<Diagnostic> {
             return if(counter == 0){
                 counter++
                 val realKernel = ProBKernelManager(communicator)
-                realKernel.checkDocument(uri, settings)
+                realKernel.checkDocument(file, settings)
 
             }else{
                 listOf()
@@ -117,9 +61,11 @@ class BDocumentServiceTest {
 
 
 
+        val documentToCheck = File("src/test/resources/WD_M1.mch").absolutePath
+
         val expectedDocument = File("src/test/resources/WD_M1.mch").absolutePath
 
-        documentService.checkDocument(URI("src/test/resources/WD_M1.mch"))
+        documentService.checkDocument(File(documentToCheck))
 
         val targetSet =  communicator.pushedDiagnostics.entries.first().value.map { value -> value.source }.toSet()
 
@@ -138,16 +84,16 @@ class BDocumentServiceTest {
 
         val documentService = BDocumentService(DummyServer(), communicator, ProBKernelManager(communicator))
 
-        val documentToCheck = URI("src/test/resources/WD_M2.mch")
+        val documentToCheck = File("src/test/resources/WD_M2.mch").absolutePath
 
         val expectedDocument = File("src/test/resources/WD_M1.mch").absolutePath
 
 
-        documentService.checkDocument(documentToCheck)
+        documentService.checkDocument(File(documentToCheck))
 
         communicator.pushedDiagnostics.clear()
 
-        documentService.checkDocument(documentToCheck)
+        documentService.checkDocument(File(documentToCheck))
 
         val targetSet =  communicator.pushedDiagnostics.entries.first().value.map { value -> value.source }.toSet()
 
@@ -166,9 +112,9 @@ class BDocumentServiceTest {
 
         val documentService = BDocumentService(DummyServer(), communicator, DummyProBKernelManager(communicator))
 
-        documentService.checkDocument(URI("src/test/resources/WD_M2.mch"))
+        documentService.checkDocument(File(File("src/test/resources/WD_M2.mch").absolutePath))
 
-        documentService.checkDocument(URI("src/test/resources/WD_M2.mch"))
+        documentService.checkDocument(File(File("src/test/resources/WD_M2.mch").absolutePath))
 
         assertEquals(emptyList(), communicator.pushedDiagnostics.entries.first().value)
     }

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

+import b.language.server.communication.CommunicatorInterface
+import org.eclipse.lsp4j.Diagnostic
+import org.eclipse.lsp4j.MessageType
+
+class DummyCommunicator : CommunicatorInterface {
+
+    val pushedDiagnostics :MutableMap<String, List<Diagnostic>> = mutableMapOf()
+    private val pushedDebugMessages = mutableListOf<String>()
+
+
+    /**
+     * 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) {
+        pushedDebugMessages.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) {
+        //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
+    }
+
+}

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

 package b.language.server.prob2.proBMangement
 
+import DummyCommunicator
 import b.language.server.proBMangement.prob.convertErrorItems
 import b.language.server.proBMangement.prob.getErrorItemType
 import de.prob.animator.domainobjects.ErrorItem
@@ -33,7 +34,7 @@ class UtilTest {
                          Position(endLine-1, endCol)),
                  message, DiagnosticSeverity.Error, file.absolutePath)
 
-        val errorItemAfter = convertErrorItems(listOf(errorItem), "dummy").first()
+        val errorItemAfter = convertErrorItems(listOf(errorItem), File("dummy"), DummyCommunicator() ).first()
 
         assertEquals(diagnostic, errorItemAfter)