diff --git a/settings.gradle.kts b/settings.gradle.kts
index 260c6a0f7a1f9c9158a3c4e6d8446e7bbe56b020..36680e8c5b61e03ee4472c5d00410e8080f9ee9e 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 e86d1daef477dbc04b24022e9d5b8ed887bd4838..3e34983c1d6ac095609619917bf17e43da716a28 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 57d3d9ccc4c8eb31de89e0fbd08bf99ec6615943..c0cf930206b6b9323e1447bc41a39d1e23124532 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 1f751b120b8fb90dbbab7c38d3f5217cc9893501..1d6e1effa78079aa9196250a04b5389aa035d8ee 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 6eb1e55814e20ad4824510dae70d91dfce5d8c53..3812518fb94c6176b866c73bf37c949d91d3cfd6 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 6bd2fe10f69d760ba1b397123980a5b1c27bd502..3f2a06dfe8058cf671785b4b42f603bb87d2aebd 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 dd42b43b55b0f0fc324af26cd3aa102a1b86975f..1d699a147b3ece53f96b3ad8a0616bb3e6079d08 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 8c51998438a95c2d8888658365a15d0fa97c8646..3095312d88db9cc62ee027a794f395c2b23fa9c9 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