diff --git a/src/main/kotlin/b/language/server/BDocumentService.kt b/src/main/kotlin/b/language/server/BDocumentService.kt
index 44abdc73c21d60fdd3695125577817c8cae17507..6ca34585bfe3347d61a2d2247e2a02300921eb61 100644
--- a/src/main/kotlin/b/language/server/BDocumentService.kt
+++ b/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
diff --git a/src/main/kotlin/b/language/server/proBMangement/ProBInterface.kt b/src/main/kotlin/b/language/server/proBMangement/ProBInterface.kt
index 2a55d85642162d93fc3a5d1cadc4496e3ecfa23c..43c4789b492052a51425c421ca319254290752b6 100644
--- a/src/main/kotlin/b/language/server/proBMangement/ProBInterface.kt
+++ b/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
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 da19fc660307651721d16436fe665f6bd03c1666..9bc58679504256ef6812f341183eeb4803b6bcca 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
+++ b/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
}
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt
index 49f0ab41611fc3d7464c23bfad46846b4316c47a..d77bd03d4c3095adc743e1ca09ae4554f797eb07 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt
+++ b/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
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt b/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt
index d51c726748f6c8461cf23f1b586c441f6fcdc880..3bf5dc5f76a3c199d7d841b0126bdeec14c34b7e 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt
@@ -1,22 +1,23 @@
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){
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/WarningListener.kt b/src/main/kotlin/b/language/server/proBMangement/prob/WarningListener.kt
index 683149e07a8649037103076e477436b0ab42ae9f..f78cfe4e01ed11dde26e08d4440e976460c3cea3 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/WarningListener.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/WarningListener.kt
@@ -1,13 +1,15 @@
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
diff --git a/src/test/kotlin/b/language/server/prob2/proBMangement/BDocumentServiceTest.kt b/src/test/kotlin/b/language/server/prob2/proBMangement/BDocumentServiceTest.kt
index 283a36ef04ff03b4a4062551511802f8505f28a1..799f0070505c48e26c19b701bda2509ca3f41924 100644
--- a/src/test/kotlin/b/language/server/prob2/proBMangement/BDocumentServiceTest.kt
+++ b/src/test/kotlin/b/language/server/prob2/proBMangement/BDocumentServiceTest.kt
@@ -1,5 +1,6 @@
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)
}
diff --git a/src/test/kotlin/b/language/server/prob2/proBMangement/DummyCommunicator.kt b/src/test/kotlin/b/language/server/prob2/proBMangement/DummyCommunicator.kt
new file mode 100644
index 0000000000000000000000000000000000000000..59f47648ee8e41c5af519e813d92a89f653650c2
--- /dev/null
+++ b/src/test/kotlin/b/language/server/prob2/proBMangement/DummyCommunicator.kt
@@ -0,0 +1,58 @@
+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
+ }
+
+}
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 466c6f872fbca2680ac261a4ff3340fdd0fa351f..a0b2af5c4361fd0ceda3a6b1a756d8d6a9594078 100644
--- a/src/test/kotlin/b/language/server/prob2/proBMangement/UtilTest.kt
+++ b/src/test/kotlin/b/language/server/prob2/proBMangement/UtilTest.kt
@@ -1,5 +1,6 @@
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)