From a2f921f08f5daad39864450f2fa3f0dc4e5e5f21 Mon Sep 17 00:00:00 2001
From: SeeBasTStick <sebastian.stock@hhu.de>
Date: Tue, 22 Sep 2020 16:49:10 +0200
Subject: [PATCH] added information from probKernel
---
settings.gradle.kts | 1 +
src/main/kotlin/b/language/server/App.kt | 2 +-
.../kotlin/b/language/server/BDocumentService.kt | 2 +-
src/main/kotlin/b/language/server/Server.kt | 2 +-
.../server/proBMangement/prob/ProBKernel.kt | 16 ++++++----------
.../proBMangement/prob/ProBKernelManager.kt | 3 ++-
.../b/language/server/proBMangement/prob/Util.kt | 3 +++
.../server/proBMangement/prob/WarningListener.kt | 6 +++---
8 files changed, 18 insertions(+), 17 deletions(-)
diff --git a/settings.gradle.kts b/settings.gradle.kts
index 260c6a0..36680e8 100644
--- a/settings.gradle.kts
+++ b/settings.gradle.kts
@@ -8,3 +8,4 @@
*/
rootProject.name = "b-language-server"
+includeBuild("../prob2_kernel/de.prob2.kernel")
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/App.kt b/src/main/kotlin/b/language/server/App.kt
index e86d1da..3e34983 100644
--- a/src/main/kotlin/b/language/server/App.kt
+++ b/src/main/kotlin/b/language/server/App.kt
@@ -10,7 +10,7 @@ import java.util.concurrent.Future
fun main() {
println("opening connection and waiting ...")
- val socket = ServerSocket(55555)
+ val socket = ServerSocket(55556)
val channel = socket.accept()
println("accepted connection from ${channel.inetAddress}")
startServer(channel.getInputStream(), channel.getOutputStream())
diff --git a/src/main/kotlin/b/language/server/BDocumentService.kt b/src/main/kotlin/b/language/server/BDocumentService.kt
index 57d3d9c..c0cf930 100644
--- a/src/main/kotlin/b/language/server/BDocumentService.kt
+++ b/src/main/kotlin/b/language/server/BDocumentService.kt
@@ -55,7 +55,7 @@ class BDocumentService(private val server: Server,
try{
val diagnostics: List<Diagnostic> = proBInterface.checkDocument(currentUri, settings)
- communicator.sendDebugMessage("created diagnostics $diagnostics", MessageType.Info)
+ communicator.sendDebugMessage("creating diagnostics $diagnostics", MessageType.Info)
communicator.publishDiagnostics(PublishDiagnosticsParams(currentUri, diagnostics))
val filesWithProblems = diagnostics.map { diagnostic -> diagnostic.source }
val invalidFiles = calculateToInvalidate(currentUri, filesWithProblems)
diff --git a/src/main/kotlin/b/language/server/Server.kt b/src/main/kotlin/b/language/server/Server.kt
index 1f751b1..1d6e1ef 100644
--- a/src/main/kotlin/b/language/server/Server.kt
+++ b/src/main/kotlin/b/language/server/Server.kt
@@ -28,7 +28,7 @@ class Server : LanguageServer{
res.capabilities.textDocumentSync = Either.forLeft(TextDocumentSyncKind.Full)
res.capabilities.workspace = WorkspaceServerCapabilities(WorkspaceFoldersOptions())
res.capabilities.workspace.workspaceFolders.supported = true
-
+ res.capabilities.completionProvider = CompletionOptions()
return CompletableFuture.supplyAsync { res }
}
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 6eb1e55..3812518 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
@@ -4,7 +4,6 @@ package b.language.server.proBMangement.prob
import b.language.server.communication.Communicator
import b.language.server.communication.CommunicatorInterface
import b.language.server.dataStorage.ProBSettings
-import com.google.gson.Gson
import com.google.inject.Inject
import com.google.inject.Injector
import de.prob.animator.ReusableAnimator
@@ -19,10 +18,7 @@ import de.prob.statespace.StateSpace
import de.prob.statespace.Trace
import org.eclipse.lsp4j.Diagnostic
import org.eclipse.lsp4j.MessageType
-import org.ietf.jgss.GSSContext
-import java.io.File
import java.io.IOException
-import java.nio.charset.Charset
/**
* Represents the interface to communicate with prob kernel
@@ -43,13 +39,13 @@ 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("Unload old machine", MessageType.Info)
+ Communicator.sendDebugMessage("unloading old machine", MessageType.Info)
unloadMachine()
val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(path.substringAfterLast(".")))
- val warningListener = WarningListener()
- animator.addWarningListener(warningListener)
+ val informationListener = InformationListener()
+ animator.addWarningListener(informationListener)
val parseErrors = mutableListOf<Diagnostic>()
Communicator.sendDebugMessage("loading new machine", MessageType.Info)
@@ -70,7 +66,7 @@ class ProBKernel @Inject constructor(private val injector : Injector,
communicator.sendDebugMessage("returning from kernel", MessageType.Info)
- return listOf(warningListener.getWarnings(), parseErrors, strictProblems).flatten()
+ return listOf(informationListener.getInformation(), parseErrors, strictProblems).flatten()
}
/**
@@ -92,7 +88,7 @@ class ProBKernel @Inject constructor(private val injector : Injector,
resultLint.addAll(newStateSpace.performExtendedStaticChecks())
}
- communicator.sendDebugMessage("returning...", MessageType.Info)
+ communicator.sendDebugMessage("finished evaluation", MessageType.Info)
} catch (e: RuntimeException) {
newStateSpace.kill()
@@ -110,7 +106,7 @@ class ProBKernel @Inject constructor(private val injector : Injector,
*/
private fun executeAdditionalOptions(settings : ProBSettings){
if(settings.wdChecks){
- communicator.sendDebugMessage("Doing WD checks", MessageType.Info)
+ communicator.sendDebugMessage("doing WD checks", MessageType.Info)
animator.execute(CheckWellDefinednessCommand())
}
}
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 6bd2fe1..3f2a06d 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt
@@ -88,7 +88,8 @@ class ProBKernelManager(private val communicator : CommunicatorInterface) : ProB
System.getProperty("prob.home"), MessageType.Info)
val result = checkProBVersionSetting(settings.probHome)
if(!result){
- throw CouldNotFindProBHomeException("searched at ${settings.probHome} for prob but found nothing")
+ throw CouldNotFindProBHomeException("searched at ${settings.probHome} for prob but found nothing - make sure " +
+ "you point to the prob directory not to probcli.sh/probcli")
}
communicator.sendDebugMessage("success!", MessageType.Info)
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 dd42b43..1d699a1 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt
@@ -30,6 +30,9 @@ fun getErrorItemType(errorItem: ErrorItem.Type) : DiagnosticSeverity{
ErrorItem.Type.INTERNAL_ERROR -> {
DiagnosticSeverity.Error
}
+ ErrorItem.Type.MESSAGE -> {
+ DiagnosticSeverity.Information
+ }
else -> {
DiagnosticSeverity.Error
}
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 8c51998..3095312 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/WarningListener.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/WarningListener.kt
@@ -1,6 +1,6 @@
package b.language.server.proBMangement.prob
-import de.prob.animator.IWarningListener
+import de.prob.animator.IInformationListener
import de.prob.animator.domainobjects.ErrorItem
import org.eclipse.lsp4j.Diagnostic
import org.eclipse.lsp4j.DiagnosticSeverity
@@ -8,13 +8,13 @@ import org.eclipse.lsp4j.DiagnosticSeverity
/**
* Custom collector to collect warnings from prob kernel
*/
-class WarningListener : IWarningListener {
+class InformationListener : IInformationListener {
private val warningList : ArrayList<ErrorItem> = arrayListOf()
override fun warningsOccurred(warnings: MutableList<ErrorItem>?) {
warningList.addAll(warnings!!.toList())
}
- fun getWarnings() : List<Diagnostic>{
+ fun getInformation() : List<Diagnostic>{
return convertErrorItems(warningList)
}
}
\ No newline at end of file
--
GitLab