diff --git a/gradle.properties b/gradle.properties
new file mode 100644
index 0000000000000000000000000000000000000000..d2271f23ed7996c90a3da20bfad660cfe0eee194
--- /dev/null
+++ b/gradle.properties
@@ -0,0 +1 @@
+org.gradle.jvmargs=-Xmx1000m
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/BDocumentService.kt b/src/main/kotlin/b/language/server/BDocumentService.kt
index fce2ef423fc502a50b8d8da2602cbe28dd96f592..44abdc73c21d60fdd3695125577817c8cae17507 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.net.URI
import java.util.concurrent.ConcurrentHashMap
class BDocumentService(private val server: ServerInterface,
@@ -35,18 +36,19 @@ class BDocumentService(private val server: ServerInterface,
override fun didSave(params: DidSaveTextDocumentParams?) {
communicator.sendDebugMessage("document ${params!!.textDocument.uri} was saved", MessageType.Info)
- val currentUri = params.textDocument.uri
- checkDocument(currentUri)
+ checkDocument(URI(params.textDocument.uri))
}
/**
- * checks a document via prob an the set options
+ * checks a document via prob and the set options
* @param currentUri the uri to perform actions on
*/
- fun checkDocument(currentUri : String){
+ fun checkDocument(currentUri : URI){
- val clientSettings = server.getDocumentSettings(currentUri)
+
+
+ val clientSettings = server.getDocumentSettings(currentUri.path)
communicator.sendDebugMessage("waiting for document settings", MessageType.Info)
clientSettings.thenAccept{ settings ->
@@ -61,10 +63,10 @@ class BDocumentService(private val server: ServerInterface,
communicator.showMessage("Evaluation done: ${diagnostics.size} problem(s)", MessageType.Log)
val filesWithProblems = sortedDiagnostic.keys.toList()
- val invalidFiles = calculateToInvalidate(currentUri, filesWithProblems)
+ val invalidFiles = calculateToInvalidate(currentUri.path, filesWithProblems)
invalidFiles.forEach{uri -> communicator.publishDiagnostics(uri, listOf())}
communicator.sendDebugMessage("invalidating old files $invalidFiles", MessageType.Info)
- issueTracker[currentUri] = filesWithProblems.toSet()
+ issueTracker[currentUri.path] = filesWithProblems.toSet()
}catch (e : CouldNotFindProBHomeException){
communicator.sendDebugMessage(e.message!!, MessageType.Info)
@@ -106,8 +108,7 @@ class BDocumentService(private val server: ServerInterface,
*/
override fun didChange(params: DidChangeTextDocumentParams?) {
communicator.sendDebugMessage("document ${params!!.textDocument.uri} was changed", MessageType.Info)
- val currentUri = params.textDocument.uri
- checkDocument(currentUri)
+ checkDocument(URI(params.textDocument.uri))
}
}
\ 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 75060beb895e631bf9e62dfd79068537a2c350c1..2a55d85642162d93fc3a5d1cadc4496e3ecfa23c 100644
--- a/src/main/kotlin/b/language/server/proBMangement/ProBInterface.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/ProBInterface.kt
@@ -2,6 +2,7 @@ package b.language.server.proBMangement
import b.language.server.dataStorage.Settings
import org.eclipse.lsp4j.Diagnostic
+import java.net.URI
interface ProBInterface {
@@ -11,6 +12,6 @@ interface ProBInterface {
* @param settings the settings for this document
* @return a list of all problems found
*/
- fun checkDocument(uri : String, settings: Settings) : List<Diagnostic>
+ fun checkDocument(uri : URI, 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 a623b142db4b6c9f9baa193870bb7a62c55d0ef0..da19fc660307651721d16436fe665f6bd03c1666 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
@@ -15,6 +15,7 @@ import de.prob.statespace.AnimationSelector
import org.eclipse.lsp4j.Diagnostic
import org.eclipse.lsp4j.MessageType
import java.io.IOException
+import java.net.URI
/**
* Represents the interface to communicate with prob kernel
@@ -33,14 +34,15 @@ class ProBKernel @Inject constructor(private val injector : Injector,
* @param settings the settings under which the check takes place
* @return a list with the problems found
*/
- fun check(path : String, settings : ProBSettings) : List<Diagnostic>{
+ fun check(path : URI, settings : ProBSettings) : List<Diagnostic>{
communicator.sendDebugMessage("unloading old machine", MessageType.Info)
unloadMachine()
- val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(path.substringAfterLast(".")))
- val informationListener = InformationListener(path)
+ val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(path.path.substringAfterLast(".")))
+
+ val informationListener = InformationListener(path.path)
animator.addWarningListener(informationListener)
communicator.sendDebugMessage("loading new machine", MessageType.Info)
@@ -58,7 +60,7 @@ class ProBKernel @Inject constructor(private val injector : Injector,
* @param path the path to the document
* @param factory a factory
*/
- private fun loadMachine(settings: ProBSettings, path : String, factory : ModelFactory<*>): List<Diagnostic> {
+ private fun loadMachine(settings: ProBSettings, path : URI, factory : ModelFactory<*>): List<Diagnostic> {
communicator.sendDebugMessage("creating new state space", MessageType.Info)
val newStateSpace = animator.createStateSpace()
@@ -68,7 +70,7 @@ class ProBKernel @Inject constructor(private val injector : Injector,
val errors = mutableListOf<ErrorItem>()
try {
- factory.extract(path).loadIntoStateSpace(newStateSpace)
+ factory.extract(path.path).loadIntoStateSpace(newStateSpace)
} catch (e: IOException) {
communicator.sendDebugMessage("IOException ${e.message}", MessageType.Info)
} catch (e : ProBError){
@@ -94,7 +96,7 @@ class ProBKernel @Inject constructor(private val injector : Injector,
communicator.sendDebugMessage("processing errors", MessageType.Info)
newStateSpace.kill()
- return convertErrorItems(errors, path)
+ return convertErrorItems(errors, path.path)
}
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 cc610a9cd61620dce0a562eab1b76d55ac1967ff..49f0ab41611fc3d7464c23bfad46846b4316c47a 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt
@@ -77,10 +77,7 @@ class ProBKernelManager(private val communicator : CommunicatorInterface) : ProB
*
* @throws CouldNotFindProBHomeException the given path ist not "DEFAULT" and wrong
*/
- override fun checkDocument(uri: String, settings: Settings): List<Diagnostic> {
-
- val path = URI(uri).path
- //Files.exists(Path.of(URI(uri)))
+ override fun checkDocument(uri: URI, 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)
@@ -91,7 +88,7 @@ class ProBKernelManager(private val communicator : CommunicatorInterface) : ProB
communicator.sendDebugMessage("success!", MessageType.Info)
communicator.sendDebugMessage("checking document", MessageType.Info)
- return kernel.check(path, ProBSettings(wdChecks = settings.wdChecks, strictChecks = settings.strictChecks,
+ return kernel.check(uri, ProBSettings(wdChecks = settings.wdChecks, strictChecks = settings.strictChecks,
performanceHints = settings.performanceHints))
}
}
\ 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 ce1fd083587b2dae9e2c1be298033ea6f0972907..cb7c8d2c97e540afae409a5270f6677329c77233 100644
--- a/src/test/kotlin/b/language/server/prob2/proBMangement/BDocumentServiceTest.kt
+++ b/src/test/kotlin/b/language/server/prob2/proBMangement/BDocumentServiceTest.kt
@@ -9,6 +9,8 @@ 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
@@ -56,7 +58,6 @@ class BDocumentServiceTest {
* @param mode the new state of the debug mode
*/
override fun setDebugMode(mode: Boolean) {
-
//void
}
@@ -94,7 +95,7 @@ class BDocumentServiceTest {
private var counter = 0
- override fun checkDocument(uri: String, settings: Settings): List<Diagnostic> {
+ override fun checkDocument(uri: URI, settings: Settings): List<Diagnostic> {
return if(counter == 0){
counter++
val realKernel = ProBKernelManager(communicator)
@@ -114,7 +115,9 @@ class BDocumentServiceTest {
val documentService = BDocumentService(DummyServer(), communicator, ProBKernelManager(communicator))
- documentService.checkDocument("src/test/resources/WD_M1.mch")
+
+
+ documentService.checkDocument(URI("src/test/resources/WD_M1.mch"))
val targetSet = communicator.pushedDiagnostics.entries.first().value.map { value -> value.source }.toSet()
@@ -133,20 +136,22 @@ class BDocumentServiceTest {
val documentService = BDocumentService(DummyServer(), communicator, ProBKernelManager(communicator))
- documentService.checkDocument("src/test/resources/WD_M2.mch")
+ val documentToCheck = URI("src/test/resources/WD_M2.mch")
- communicator.pushedDiagnostics.clear()
+ val expectedDocument = "src/test/resources/WD_M1.mch"
- documentService.checkDocument("src/test/resources/WD_M2.mch")
- println(communicator.pushedDiagnostics.size)
+ documentService.checkDocument(documentToCheck)
- val targetSet = communicator.pushedDiagnostics.entries.first().value.map { value -> value.source }.toSet()
+ communicator.pushedDiagnostics.clear()
+ documentService.checkDocument(documentToCheck)
+
+ val targetSet = communicator.pushedDiagnostics.entries.first().value.map { value -> value.source }.toSet()
assertEquals(2, communicator.pushedDiagnostics.entries.size)
assertEquals(3, communicator.pushedDiagnostics.entries.first().value.size)
- assertTrue(targetSet.first().contains("b-language-server/src/test/resources/WD_M1.mch"))
+ assertEquals(File(expectedDocument).absolutePath, targetSet.first())
}
@@ -159,12 +164,19 @@ class BDocumentServiceTest {
val documentService = BDocumentService(DummyServer(), communicator, DummyProBKernelManager(communicator))
- documentService.checkDocument("src/test/resources/WD_M2.mch")
-
- documentService.checkDocument("src/test/resources/WD_M2.mch")
+ documentService.checkDocument(URI("src/test/resources/WD_M2.mch"))
- println(communicator.pushedDiagnostics)
+ documentService.checkDocument(URI("src/test/resources/WD_M2.mch"))
assertEquals(emptyList(), communicator.pushedDiagnostics.entries.first().value)
}
+
+ /**
+ * Write Tests:
+ * Test different options you can turn on and off
+ * strict, WD, performance
+ * Included files have errors and errors are mapped properly
+ * Included files have no errors
+ * Included files have
+ */
}
\ No newline at end of file