diff --git a/build.gradle.kts b/build.gradle.kts
index 6f541ad966a2f41dc6cc7584cc4b5f5fcffcc756..36c6a8e889f927be41922a25cba1488c21d3c3ce 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -32,7 +32,7 @@ dependencies {
implementation("org.jetbrains.kotlin:kotlin-stdlib-jdk8")
- // implementation("org.jetbrains.kotlinx:kotlinx-coroutines-core:1.3.9")
+ implementation("org.jetbrains.kotlinx:kotlinx-coroutines-core:1.3.9")
// eclipse lsp implementation
@@ -53,6 +53,10 @@ dependencies {
implementation( "com.google.guava", "guava", "28.2-jre")
+ // https://mvnrepository.com/artifact/org.zeromq/jeromq
+ implementation ("org.zeromq", "jeromq", "0.5.2")
+
+
}
diff --git a/src/main/kotlin/b/language/server/App.kt b/src/main/kotlin/b/language/server/App.kt
index 014cb395c7398e42d9f1ac5f07ef89818d3175ef..66ef528f9a9f2a6624e1fe7a74cc8f4619f4b224 100644
--- a/src/main/kotlin/b/language/server/App.kt
+++ b/src/main/kotlin/b/language/server/App.kt
@@ -1,18 +1,32 @@
package b.language.server
+import b.language.server.proBMangement.prob.ProBKernelManager
import org.eclipse.lsp4j.jsonrpc.Launcher
import org.eclipse.lsp4j.launch.LSPLauncher
import org.eclipse.lsp4j.services.LanguageClient
-import java.io.InputStream
-import java.io.OutputStream
+import java.io.*
+import java.net.InetAddress
+import java.net.ServerSocket
+import java.net.Socket
+import java.nio.charset.StandardCharsets
import java.util.concurrent.Future
fun main() {
- startServer(System.`in`, System.out)
+ println("opening connection and waiting ...")
+ val socket = ServerSocket(5555)
+ val channel = socket.accept()
+ println("accepted connection from ${channel.inetAddress}")
+ startServer(channel.getInputStream(), channel.getOutputStream())
}
fun startServer(inputStream: InputStream, outputStream: OutputStream){
+
+ println("starting kernel")
+ val kernel = ProBKernelManager()
+ kernel.start()
+ println("done")
+
val server = Server()
val launcher : Launcher<LanguageClient> = LSPLauncher.createServerLauncher(server, inputStream, outputStream)
val startListing : Future<*> = launcher.startListening()
diff --git a/src/main/kotlin/b/language/server/BDocumentService.kt b/src/main/kotlin/b/language/server/BDocumentService.kt
index 057d5af103f31ed8a753605eed3ad6ec70142367..54bb9bb3d597bbbcebb16f3465a993e391f08aa3 100644
--- a/src/main/kotlin/b/language/server/BDocumentService.kt
+++ b/src/main/kotlin/b/language/server/BDocumentService.kt
@@ -1,7 +1,6 @@
package b.language.server
import b.language.server.communication.CommunicatorInterface
-import b.language.server.proBMangement.ProBFactory
import b.language.server.proBMangement.ProBInterface
import org.eclipse.lsp4j.*
import org.eclipse.lsp4j.services.TextDocumentService
@@ -10,7 +9,7 @@ import java.util.concurrent.ConcurrentHashMap
class BDocumentService(private val server: Server,
private val communicator: CommunicatorInterface,
- private val proBFactory: ProBFactory = ProBFactory()) : TextDocumentService {
+ private val proBInterface: ProBInterface) : TextDocumentService {
private val documents = ConcurrentHashMap<String, String>()
private val issueTracker : ConcurrentHashMap<String, Set<String>> = ConcurrentHashMap()
@@ -52,11 +51,10 @@ class BDocumentService(private val server: Server,
clientSettings.thenAccept{ settings ->
communicator.setDebugMode(settings.debugMode)
- val prob : ProBInterface = proBFactory.getProBAccess(communicator)
communicator.sendDebugMessage("settings are $settings", MessageType.Info)
try{
- val diagnostics: List<Diagnostic> = prob.checkDocument(currentUri, settings)
+ val diagnostics: List<Diagnostic> = proBInterface.checkDocument(currentUri, settings)
communicator.sendDebugMessage("created diagnostics $diagnostics", MessageType.Info)
communicator.publishDiagnostics(PublishDiagnosticsParams(currentUri, diagnostics))
val filesWithProblems = diagnostics.map { diagnostic -> diagnostic.source }
diff --git a/src/main/kotlin/b/language/server/BWorkspaceService.kt b/src/main/kotlin/b/language/server/BWorkspaceService.kt
index 7dfc24dc30730e95391dde72e21e0bee3a5d1a92..86952c373a3124505e161356b45e5c8de4fd5af7 100644
--- a/src/main/kotlin/b/language/server/BWorkspaceService.kt
+++ b/src/main/kotlin/b/language/server/BWorkspaceService.kt
@@ -1,16 +1,14 @@
package b.language.server
import b.language.server.communication.Communicator
-import b.language.server.dataStorage.Settings
-import com.google.gson.Gson
import com.google.gson.JsonObject
import org.eclipse.lsp4j.DidChangeConfigurationParams
import org.eclipse.lsp4j.DidChangeWatchedFilesParams
import org.eclipse.lsp4j.MessageType
import org.eclipse.lsp4j.services.WorkspaceService
-import java.io.File
-class BWorkspaceService(private val server : Server) : WorkspaceService {
+
+class BWorkspaceService(private val server: Server) : WorkspaceService {
/**
* The watched files notification is sent from the client to the server when
* the client detects changes to file watched by the language client.
diff --git a/src/main/kotlin/b/language/server/Server.kt b/src/main/kotlin/b/language/server/Server.kt
index 0f4a0f7a66b8a817ab4cebb05fd5e6425f6b3b08..17cbfa336e45cd5ae195c6937a9a59a4d80dc0de 100644
--- a/src/main/kotlin/b/language/server/Server.kt
+++ b/src/main/kotlin/b/language/server/Server.kt
@@ -2,6 +2,8 @@ package b.language.server
import b.language.server.communication.Communicator
import b.language.server.dataStorage.Settings
+import b.language.server.proBMangement.prob.ProBKernelConnector
+import b.language.server.proBMangement.prob.ProBKernelManager
import com.google.gson.JsonObject
import org.eclipse.lsp4j.*
import org.eclipse.lsp4j.jsonrpc.messages.Either
@@ -10,9 +12,9 @@ import java.util.concurrent.CompletableFuture
import kotlin.collections.HashMap
import kotlin.system.exitProcess
-class Server : LanguageServer{
+class Server() : LanguageServer{
- private val textDocumentService : TextDocumentService = BDocumentService(this, Communicator)
+ private val textDocumentService : TextDocumentService = BDocumentService(this, Communicator, ProBKernelConnector(Communicator))
private val bWorkspaceService : WorkspaceService = BWorkspaceService(this)
lateinit var languageClient : LanguageClient
var globalSettings : Settings = Settings()
@@ -20,6 +22,8 @@ class Server : LanguageServer{
var configurationAbility : Boolean = true
+
+
override fun initialize(params: InitializeParams?): CompletableFuture<InitializeResult> {
val res = InitializeResult(ServerCapabilities())
res.capabilities.textDocumentSync = Either.forLeft(TextDocumentSyncKind.Full)
@@ -91,6 +95,7 @@ class Server : LanguageServer{
val configurationItem = ConfigurationItem()
configurationItem.scopeUri = uri
configurationItem.section = "languageServer"
+
val requestedConfig = languageClient.configuration(ConfigurationParams(listOf(configurationItem)))
documentSettings[uri] = CompletableFuture.allOf(requestedConfig).thenApply{ castJsonToSetting(requestedConfig.get().first() as JsonObject) }
documentSettings[uri]!!
@@ -98,4 +103,7 @@ class Server : LanguageServer{
}
+
+
+
}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/communication/CommunicationCollector.kt b/src/main/kotlin/b/language/server/communication/CommunicationCollector.kt
new file mode 100644
index 0000000000000000000000000000000000000000..73a32adb60cbdb1ee04de3d0bc6a9e02589ad85d
--- /dev/null
+++ b/src/main/kotlin/b/language/server/communication/CommunicationCollector.kt
@@ -0,0 +1,46 @@
+package b.language.server.communication
+
+import org.eclipse.lsp4j.MessageType
+import org.eclipse.lsp4j.PublishDiagnosticsParams
+
+class CommunicationCollector : CommunicatorInterface {
+
+ val log : MutableList<Pair<String, MessageType>> = mutableListOf()
+ /**
+ * Sends the diagnostics
+ *
+ * @param diagnostics object containing the Diagnostics
+ */
+ override fun publishDiagnostics(diagnostics: PublishDiagnosticsParams) {
+ TODO("Not yet implemented")
+ }
+
+ /**
+ * 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) {
+ log.add(Pair(message, severity))
+ }
+
+ /**
+ * 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) {
+ TODO("Not yet implemented")
+ }
+
+ /**
+ * To enable/disable debug mode
+ *
+ * @param mode the new state of the debug mode
+ */
+ override fun setDebugMode(mode: Boolean) {
+ TODO("Not yet implemented")
+ }
+}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/communication/Communicator.kt b/src/main/kotlin/b/language/server/communication/Communicator.kt
index 7b8f5912b1abfdb1d4cd4b0c6b9bbcb3e06bd0d8..10fb9a7efc467d150a57447822c09f981eeed277 100644
--- a/src/main/kotlin/b/language/server/communication/Communicator.kt
+++ b/src/main/kotlin/b/language/server/communication/Communicator.kt
@@ -33,6 +33,7 @@ object Communicator : CommunicatorInterface {
*/
override fun sendDebugMessage(message: String, severity: MessageType) {
if(debugMode) {
+ System.err.println("Debug messages $message")
client.logMessage(MessageParams(severity, message))
}
diff --git a/src/main/kotlin/b/language/server/proBMangement/CommandCouldNotBeExecutedException.kt b/src/main/kotlin/b/language/server/proBMangement/CommandCouldNotBeExecutedException.kt
deleted file mode 100644
index 01c9b006b379f66fbaffa656aeff0f81da69c1f2..0000000000000000000000000000000000000000
--- a/src/main/kotlin/b/language/server/proBMangement/CommandCouldNotBeExecutedException.kt
+++ /dev/null
@@ -1,3 +0,0 @@
-package b.language.server.proBMangement
-
-class CommandCouldNotBeExecutedException(message: String?) : Exception(message)
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/PathCouldNotBeCreatedException.kt b/src/main/kotlin/b/language/server/proBMangement/PathCouldNotBeCreatedException.kt
deleted file mode 100644
index 57f2ddefbe8df4fb3dbdf319dd6b5cd9d71fdc24..0000000000000000000000000000000000000000
--- a/src/main/kotlin/b/language/server/proBMangement/PathCouldNotBeCreatedException.kt
+++ /dev/null
@@ -1,3 +0,0 @@
-package b.language.server.proBMangement
-
-class PathCouldNotBeCreatedException(message: String?) : Exception(message)
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/ProBCommandLineAccess.kt b/src/main/kotlin/b/language/server/proBMangement/ProBCommandLineAccess.kt
deleted file mode 100644
index a75f679e22a6e47da742ac747ac7e9fa0982b975..0000000000000000000000000000000000000000
--- a/src/main/kotlin/b/language/server/proBMangement/ProBCommandLineAccess.kt
+++ /dev/null
@@ -1,200 +0,0 @@
-package b.language.server.proBMangement
-
-import b.language.server.communication.CommunicatorInterface
-import b.language.server.dataStorage.Problem
-import b.language.server.dataStorage.Settings
-import com.google.gson.Gson
-import org.eclipse.lsp4j.*
-import java.io.*
-import java.net.URI
-
-
-/**
- * Access ProB via command line
- */
-class ProBCommandLineAccess(val communicator : CommunicatorInterface) : ProBInterface{
- /**
- * Checks the given document with the help of ProB; Will setup all needed steps to ensure a clean process
- * @param uri the source to check
- * @return a list of all problems found
- */
- override fun checkDocument(uri : String, settings: Settings): List<Diagnostic> {
- communicator.sendDebugMessage("checking document ($uri) with proB", MessageType.Info )
- val realUri = URI(uri)
- val path = File(realUri.path)
- val errorPath = File(path.parent + "/tmp/_error.json")
- val errorDict = File(path.parent + "/tmp")
-
- val result = createFolder(errorDict, errorPath)
- if(!result){
- throw PathCouldNotBeCreatedException("The Path leading to $errorPath has not been created due some issue.")
- }
- communicator.sendDebugMessage("creation successful", MessageType.Info)
- val command = buildCommand(settings, path, errorPath)
- communicator.sendDebugMessage("sending command <$command> to proB", MessageType.Info)
-
- performActionOnDocument(command)
-
- val problems = readProblems(errorPath.path)
- communicator.sendDebugMessage("found the following problems: $problems", MessageType.Info)
-
- return transformProblems(problems)
- }
-
-
- /**
- * Constructs the commandline call to proB depending on the given settings
- * @param settings the settings for the document
- * @param fileToCheck the current documents address
- * @param errorPath the path to dump the ndjson message
- * @return the execution ready command
- */
- fun buildCommand(settings : Settings, fileToCheck : File, errorPath : File) : String{
- val configuration = " -p MAX_INITIALISATIONS 0 -version "
- val ndjson = " -p NDJSON_ERROR_LOG_FILE "
- val wd : String = if(settings.wdChecks){
- " -wd-check -release_java_parser "
- }else{
- " "
- }
- val strict : String = if(settings.strictChecks){
- " -p STRICT_CLASH_CHECKING TRUE -p TYPE_CHECK_DEFINITIONS TRUE -lint "
- }else{
- " "
- }
- val performanceHints : String = if(settings.performanceHints){
- " -p PERFORMANCE_INFO TRUE "
- }else{
- " "
- }
-
- val probHome = settings.probHome
-
- return probHome.path +
- configuration +
- performanceHints +
- strict +
- wd +
- fileToCheck.absoluteFile +
- ndjson +
- errorPath.absoluteFile
-
- }
-
-
- /**
- * Creates the tmp folder and an empty ndjson file; will recreate an empty ndjson file to ensure clean messages
- * @param errorDict the path of the tmp dict
- * @param errorPath the path to the error file
- * @return success of the action
- */
- fun createFolder(errorDict : File, errorPath: File) : Boolean{
- communicator.sendDebugMessage("creating -----huhu----- errorDict $errorDict and errorFile $errorPath", MessageType.Info)
- errorDict.mkdirs()
- FileWriter(errorPath, false).close()
- return errorDict.exists() && errorPath.exists()
- }
-
- /**
- * Executes the given command
- * @param command to execute
- * @throws CommandCouldNotBeExecutedException probcli failed to execute the given command
- * @throws IOException failed to reach probcli
- */
- fun performActionOnDocument(command : String) {
-
- val process: Process = Runtime.getRuntime().exec(command)
-
- val output : InputStream = process.inputStream
-
-
- // process.waitFor() //we must wait here to ensure correct behavior when reading an error
- val exitStatus = process.onExit()
- val outputAsString = String(output.readAllBytes())
- communicator.sendDebugMessage("output of execution + ${exitStatus.isCompletedExceptionally}", MessageType.Info)
- if(!outputAsString.contains("ProB Command Line Interface")){
- throw CommandCouldNotBeExecutedException("Error when trying to call probcli with command $command")
- }
- }
-
-
- /**
- * Reads the errors and transforms them to java objects
- * @param path the path to the error document
- * @return the list of read errors
- */
- fun readProblems(path : String): List<Problem> {
- val jsonStrings : ArrayList<String> = ArrayList()
- BufferedReader(FileReader(path)).use { br ->
- var line: String?
- while (br.readLine().also { line = it } != null) {
- jsonStrings.add(line!!)
- }
- }
-
- val strings = jsonStrings.toList().map { string -> Gson().fromJson(string, Problem::class.java) }
- return strings
-
- }
-
- /**
- * Transforms errors to error messages
- * @param problems the list of errors to transform
- * @return the transformed errors
- */
- fun transformProblems(problems : List<Problem>): List<Diagnostic> {
- return problems.
- /**
- * Some errors from prob_cli have negative values when there is no exact error location - we set them
- * to the first line
- */
- map{ problem ->
- if (problem.start.line == -1 && problem.start.col == -1 &&
- problem.end.line == -1 && problem.end.col == -1)
- {
- print(Integer.MAX_VALUE)
- Problem(problem.type,
- problem.message,
- problem.reason,
- problem.file,
- b.language.server.dataStorage.Position(1,0),
- b.language.server.dataStorage.Position(1, Integer.MAX_VALUE),
- problem.version)
- }
- else{
- /**
- * Lines are off by one when they get out of vscode
- */
- problem.start.line = problem.start.line - 1
- problem.end.line = problem.end.line - 1
-
- problem
- }
- }
- .map { problem -> Diagnostic(
- Range(
- Position(problem.start.line, problem.start.col),
- Position(problem.end.line, problem.end.col)),
-
- problem.message,
-
- when (problem.type) {
- "error" -> {
- DiagnosticSeverity.Error
- }
- "warning" -> {
- DiagnosticSeverity.Warning
- }
- "information" -> {
- DiagnosticSeverity.Information
- }
- else -> {
- DiagnosticSeverity.Hint
- }
- },
- problem.file
- //code = " probcli v.${problem.version}"
- )
- }
- }
-}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/ProBFactory.kt b/src/main/kotlin/b/language/server/proBMangement/ProBFactory.kt
deleted file mode 100644
index 63efff88c9c3c9d28f68bbb83042f3a36d96bc29..0000000000000000000000000000000000000000
--- a/src/main/kotlin/b/language/server/proBMangement/ProBFactory.kt
+++ /dev/null
@@ -1,16 +0,0 @@
-package b.language.server.proBMangement
-
-import b.language.server.communication.CommunicatorInterface
-import b.language.server.proBMangement.prob2.ProBKernelManager
-
-
-/**
- * Generate new Instances of ProBKernelManger
- */
-class ProBFactory {
-
- fun getProBAccess(commuicator : CommunicatorInterface) : ProBInterface{
- return ProBKernelManager(commuicator)
- }
-
-}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/WrongPathException.kt b/src/main/kotlin/b/language/server/proBMangement/WrongPathException.kt
deleted file mode 100644
index 0fa842ad75f71b34d06f54545e29138ee40a3ccd..0000000000000000000000000000000000000000
--- a/src/main/kotlin/b/language/server/proBMangement/WrongPathException.kt
+++ /dev/null
@@ -1,3 +0,0 @@
-package b.language.server.proBMangement
-
-class WrongPathException (message: String?) : Exception(message)
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/MessageTypes.kt b/src/main/kotlin/b/language/server/proBMangement/prob/MessageTypes.kt
new file mode 100644
index 0000000000000000000000000000000000000000..795d1efac2a671703dc8292bb38fbb7752f79d46
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/MessageTypes.kt
@@ -0,0 +1,7 @@
+package b.language.server.proBMangement.prob
+
+enum class MessageTypes {
+
+ CHECK, KILL
+
+}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob2/MyWarningListener.kt b/src/main/kotlin/b/language/server/proBMangement/prob/MyWarningListener.kt
similarity index 91%
rename from src/main/kotlin/b/language/server/proBMangement/prob2/MyWarningListener.kt
rename to src/main/kotlin/b/language/server/proBMangement/prob/MyWarningListener.kt
index 8fb2f1a43f91b9ba040d93eb337f92a6df4762fb..676130b347a2ef972d33fd4e3a0598e892f7511a 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob2/MyWarningListener.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/MyWarningListener.kt
@@ -1,4 +1,4 @@
-package b.language.server.proBMangement.prob2
+package b.language.server.proBMangement.prob
import de.prob.animator.IWarningListener
import de.prob.animator.domainobjects.ErrorItem
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernel.kt b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
similarity index 76%
rename from src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernel.kt
rename to src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
index d8c2ae3db7a541321fc3ae17abefbe1ffebb7877..10fe68a99764071eef83e10b9d2c503e0c15b06d 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernel.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
@@ -1,9 +1,10 @@
+import b.language.server.communication.CommunicationCollector
import b.language.server.communication.Communicator
import b.language.server.communication.CommunicatorInterface
import b.language.server.dataStorage.ProBSettings
-import b.language.server.proBMangement.prob2.MyWarningListener
-import b.language.server.proBMangement.prob2.convertErrorItems
+import b.language.server.proBMangement.prob.MyWarningListener
+import b.language.server.proBMangement.prob.convertErrorItems
import com.google.inject.Inject
import com.google.inject.Injector
import de.prob.animator.ReusableAnimator
@@ -22,36 +23,39 @@ import java.io.IOException
class ProBKernel @Inject constructor(private val injector : Injector, val classicalBFactory : ClassicalBFactory,
private val animationSelector: AnimationSelector,
- private val animator : ReusableAnimator
- // private val communicator: Communicator
-) {
+ private val animator : ReusableAnimator) {
- val communicator = Communicator
- fun check(path : String, settings : ProBSettings) : List<Diagnostic>{
- communicator.sendDebugMessage("Unload old machine", MessageType.Info)
+ val communicator = CommunicationCollector()
+ fun check(path : String, settings : ProBSettings) : Pair<List<Diagnostic>, List<Pair<String, MessageType>>>{
+ communicator.log.clear()
+
+ Communicator.sendDebugMessage("Unload old machine", MessageType.Info)
unloadMachine()
val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(path.substringAfterLast(".")))
val warningListener = MyWarningListener()
animator.addWarningListener(warningListener)
val parseErrors = mutableListOf<Diagnostic>()
- communicator.sendDebugMessage("Load new machine", MessageType.Info)
+ Communicator.sendDebugMessage("Load new machine", MessageType.Info)
loadMachine(
- java.util.function.Function { stateSpace : StateSpace ->
+ { stateSpace : StateSpace ->
try {
val extractedModel = factory.extract(path)
val stateSpaceWithSettings = extractedModel.load(prepareAdditionalSettings(settings))
extractedModel.loadIntoStateSpace(stateSpaceWithSettings)
} catch (e: IOException) {
- throw RuntimeException(e)
+ // throw RuntimeException(e)
+ communicator.sendDebugMessage("IOException ${e.message}", MessageType.Info)
} catch (e: ModelTranslationError) {
- throw RuntimeException(e)
+ communicator.sendDebugMessage("ModelTranslationError ${e.message}", MessageType.Info)
+
+ // throw RuntimeException(e)
}catch (e : ProBError){
parseErrors.addAll(convertErrorItems(e.errors))
}
Trace(stateSpace)
}, settings)
- return listOf(warningListener.getWarnings(), parseErrors).flatten()
+ return Pair(listOf(warningListener.getWarnings(), parseErrors).flatten(), communicator.log)
}
private fun loadMachine(newTraceCreator :java.util.function.Function<StateSpace, Trace>, settings: ProBSettings){
@@ -66,7 +70,7 @@ class ProBKernel @Inject constructor(private val injector : Injector, val classi
}
private fun executeAdditionalOptions(settings : ProBSettings){
- animator.createStateSpace()
+ // animator.createStateSpace()
if(settings.wdChecks){
animator.execute(CheckWellDefinednessCommand())
}
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelConnector.kt b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelConnector.kt
new file mode 100644
index 0000000000000000000000000000000000000000..4027ccf4381db5dcb47f7f09ddfb765ffca10acc
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelConnector.kt
@@ -0,0 +1,87 @@
+package b.language.server.proBMangement.prob
+
+import b.language.server.communication.CommunicatorInterface
+import b.language.server.dataStorage.Settings
+import b.language.server.proBMangement.ProBInterface
+import com.google.gson.Gson
+import com.google.gson.JsonSyntaxException
+import org.eclipse.lsp4j.Diagnostic
+import org.eclipse.lsp4j.MessageType
+import org.zeromq.SocketType
+
+import org.zeromq.ZContext
+import org.zeromq.ZMQ
+
+
+class ProBKernelConnector(val communicator : CommunicatorInterface) : ProBInterface, ServerConnection{
+
+
+ private val context = ZContext()
+ private val socket: ZMQ.Socket = context.createSocket(SocketType.REQ)
+
+ init {
+ socket.connect("tcp://localhost:5557")
+ }
+
+ /**
+ * Checks the given document with the help of ProB
+ * @param uri the source to check
+ * @param settings the settings for this document
+ * @return a list of all problems found
+ */
+ override fun checkDocument(uri: String, settings: Settings): List<Diagnostic> {
+ communicator.sendDebugMessage("start checking, submitting to prob server " , MessageType.Info)
+ val reply = send(Request(MessageTypes.CHECK, uri, settings))
+ communicator.sendDebugMessage("got reply " , MessageType.Info)
+ System.err.println("getting reply $reply")
+ deliverDebugMessages(reply.messages)
+ System.err.println("deliverd messages")
+ return reply.diagnostics
+ }
+
+
+ /**
+ * sends a request to the b kernel thread
+ * @param payLoad the request to be send
+ * @return a reply
+ */
+ fun send(payLoad : Request) : Reply{
+ communicator.sendDebugMessage("sending... " , MessageType.Info)
+
+ socket.send(Gson().toJson(payLoad))
+ communicator.sendDebugMessage("rec... " , MessageType.Info)
+
+ val recv = socket.recvStr()
+ communicator.sendDebugMessage("rec: $recv " , MessageType.Info)
+
+ System.err.println("deserialize message")
+ val answer = try{
+ Gson().fromJson(recv, Reply::class.java)
+ }catch (e : JsonSyntaxException){
+ System.err.println("Failed..")
+ throw Exception(e)
+ }
+ System.err.println("deserialize message done")
+
+ communicator.sendDebugMessage("answer $answer" , MessageType.Info)
+
+ return answer
+ }
+
+ /**
+ * Delivers Messages we got from the b kernel thread
+ * @param messages list with the messages
+ */
+ fun deliverDebugMessages(messages : List<Pair<String, MessageType>>){
+ messages.forEach{ message -> communicator.sendDebugMessage(message.first, message.second) }
+ }
+
+
+ /**
+ * Orders the server to shutdown the process it keeps, clean up and shutdown itself
+ */
+ override fun kill(): Reply {
+ socket.send(Gson().toJson(Request(MessageTypes.KILL)))
+ return Gson().fromJson(socket.recvStr(), Reply::class.java)
+ }
+}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt
new file mode 100644
index 0000000000000000000000000000000000000000..4b1b9fdb774b197332bd1a85ddb4e55f263ca44f
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt
@@ -0,0 +1,96 @@
+package b.language.server.proBMangement.prob
+
+import ProBKernel
+import b.language.server.communication.CommunicationCollector
+import b.language.server.communication.Communicator
+import b.language.server.dataStorage.ProBSettings
+import b.language.server.dataStorage.Settings
+import com.google.gson.Gson
+import com.google.inject.Guice
+import com.google.inject.Stage
+import org.eclipse.lsp4j.MessageType
+import org.zeromq.SocketType
+
+import org.zeromq.ZContext
+import org.zeromq.ZMQ
+import java.net.URI
+
+/**
+ * Creates the prob kernel access and maintaince a stady connection
+ */
+class ProBKernelManager : Thread() {
+
+ private var active = true
+ private lateinit var kernel : ProBKernel
+ private var probHome = ""
+ private val communicator = CommunicationCollector()
+
+
+
+ override fun run() {
+ ZContext().use { context ->
+ val socket: ZMQ.Socket = context.createSocket(SocketType.REP)
+ socket.bind("tcp://*:5557")
+ kernel = setup()
+ while (active) {
+ val message = socket.recvStr()
+ val request = Gson().fromJson(message, Request::class.java)
+ Communicator.sendDebugMessage("manageer got request... " , MessageType.Info)
+
+ val reply = if (request.type==MessageTypes.CHECK){
+ check(request.uri, request.settings)
+ }else{
+ kill()
+ }
+ System.err.println("sending result back")
+ socket.send(Gson().toJson(reply))
+ }
+ }
+ }
+
+
+
+ fun check(uri : String, settings : Settings) : Reply{
+ val path = URI(uri).path
+ System.err.println("start prob")
+ System.err.println("checking file $path")
+ Communicator.sendDebugMessage("checking document", MessageType.Info)
+
+ val result = kernel.check(path, ProBSettings(settings.wdChecks, settings.strictChecks, settings.performanceHints))
+ System.err.println("returning result")
+ return Reply(result.first, result.second)
+ }
+
+ fun kill() : Reply{
+ active = false
+ return Reply(listOf(), listOf())
+ }
+
+
+ /**
+ * @param probHome the home of prob; DEFAULT for the prob version delivered with the library
+ * @return an instance of prob kernel
+ */
+ fun setup() : ProBKernel {
+
+ // Communicator.sendDebugMessage("creating injector...", MessageType.Info)
+
+ System.err.println("Creating injector in thread " + this.id)
+ val injector = Guice.createInjector(Stage.PRODUCTION, ProBKernelModule())
+ System.err.println("Done " + this.id)
+
+ // Communicator.sendDebugMessage("..done", MessageType.Info)
+
+
+ val kernel : ProBKernel
+ try{
+ kernel = injector.getInstance(ProBKernel::class.java)
+ }catch (e : de.prob.exception.CliError){
+ // Communicator.sendDebugMessage("wrong path to prob", MessageType.Error)
+ throw Exception("wrong path to prob $probHome")
+ }
+ // Communicator.sendDebugMessage("returning kernel", MessageType.Info)
+
+ return kernel
+ }
+}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelModule.kt b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelModule.kt
similarity index 64%
rename from src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelModule.kt
rename to src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelModule.kt
index 023d4f0009626b1829b80118fda74a946904e71c..88b8286a32d3d5d2696ac64615652ff791ed3ca6 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelModule.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelModule.kt
@@ -1,4 +1,4 @@
-package b.language.server.proBMangement.prob2
+package b.language.server.proBMangement.prob
import b.language.server.communication.CommunicatorInterface
import com.google.inject.AbstractModule
@@ -7,6 +7,5 @@ import de.prob.MainModule
class ProBKernelModule() : AbstractModule() {
override fun configure() {
install(MainModule())
- // bind(CommunicatorInterface::class.java).toInstance(communicatorInterface)
}
-}
+}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/Reply.kt b/src/main/kotlin/b/language/server/proBMangement/prob/Reply.kt
new file mode 100644
index 0000000000000000000000000000000000000000..0e48ca2587f5c74665034d0a4a205c9ee589c470
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/Reply.kt
@@ -0,0 +1,7 @@
+package b.language.server.proBMangement.prob
+
+import org.eclipse.lsp4j.Diagnostic
+import org.eclipse.lsp4j.MessageType
+
+
+data class Reply(val diagnostics : List<Diagnostic>, val messages : List<Pair<String, MessageType>>)
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/Request.kt b/src/main/kotlin/b/language/server/proBMangement/prob/Request.kt
new file mode 100644
index 0000000000000000000000000000000000000000..4bf4d78a5304185e28c728fbea3b2f6dd20289bd
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/Request.kt
@@ -0,0 +1,5 @@
+package b.language.server.proBMangement.prob
+
+import b.language.server.dataStorage.Settings
+
+data class Request(val type : MessageTypes, val uri : String = String(), val settings : Settings = Settings())
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/ServerConnection.kt b/src/main/kotlin/b/language/server/proBMangement/prob/ServerConnection.kt
new file mode 100644
index 0000000000000000000000000000000000000000..bcadcb2c7cf81d29de5066e95f99a3b1a4722a82
--- /dev/null
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/ServerConnection.kt
@@ -0,0 +1,9 @@
+package b.language.server.proBMangement.prob
+
+interface ServerConnection {
+
+ /**
+ * Orders the server to shutdown the process it keeps, clean up and shutdown itself
+ */
+ fun kill() : Reply
+}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob2/Util.kt b/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt
similarity index 95%
rename from src/main/kotlin/b/language/server/proBMangement/prob2/Util.kt
rename to src/main/kotlin/b/language/server/proBMangement/prob/Util.kt
index 96d7e8bae9f2e6a71e0af52653d4007d55f33f56..83fb00974c7befb909f3e04264cf35c8b4bb9fa6 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob2/Util.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt
@@ -1,4 +1,4 @@
-package b.language.server.proBMangement.prob2
+package b.language.server.proBMangement.prob
import de.prob.animator.domainobjects.ErrorItem
import org.eclipse.lsp4j.Diagnostic
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelManager.kt b/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelManager.kt
deleted file mode 100644
index 4afb8b58642d066238fa96ccecdfe597e0360509..0000000000000000000000000000000000000000
--- a/src/main/kotlin/b/language/server/proBMangement/prob2/ProBKernelManager.kt
+++ /dev/null
@@ -1,84 +0,0 @@
-package b.language.server.proBMangement.prob2
-
-import ProBKernel
-import b.language.server.communication.Communicator
-import b.language.server.communication.CommunicatorInterface
-import b.language.server.dataStorage.ProBSettings
-import b.language.server.dataStorage.Settings
-import b.language.server.proBMangement.ProBInterface
-import b.language.server.proBMangement.WrongPathException
-import com.google.inject.CreationException
-import com.google.inject.Guice
-import com.google.inject.Stage
-import org.eclipse.lsp4j.Diagnostic
-import org.eclipse.lsp4j.MessageType
-import kotlin.concurrent.thread
-
-/**
- * Setup a connection to ProB2 Kernel
- */
-class ProBKernelManager(private val communicator : CommunicatorInterface) : ProBInterface{
-
- private lateinit var kernel : ProBKernel
- private var lastProBHome : String = "DEFAULT"
-
- /**
- * Checks the given document with the help of ProB
- * @param uri the source to check
- * @param settings the settings for this document
- * @return a list of all problems found
- */
- override fun checkDocument(uri: String, settings: Settings): List<Diagnostic> {
- val proBSettings = ProBSettings(settings.wdChecks, settings.strictChecks, settings.performanceHints)
- val probHome = settings.probHome.absolutePath
-
- communicator.sendDebugMessage("checking document", MessageType.Info)
-
- return if(probHome == lastProBHome && this::kernel.isInitialized){
- kernel.check(uri, proBSettings)
- }else{
- lastProBHome = probHome
- setup(probHome).check(uri, proBSettings)
- }
-
- }
-
- /**
- * @param probHome the home of prob; DEFAULT for the prob version delivered with the library
- * @return an instance of prob kernel
- */
- fun setup(probHome : String) : ProBKernel{
- if(false){
- System.setProperty("prob.home", probHome)
- communicator.sendDebugMessage("$probHome selected", MessageType.Info)
- }else{
- communicator.sendDebugMessage("default prob selected", MessageType.Info)
- }
-
- communicator.sendDebugMessage("creating injector...", MessageType.Info)
- System.err.println((communicator as Communicator).client.toString())
- val injector =
- Guice.createInjector(Stage.PRODUCTION, ProBKernelModule())
-
- communicator.sendDebugMessage("..done", MessageType.Info)
- System.err.println((communicator as Communicator).client.toString())
-
-
- val kernel : ProBKernel
- try{
- kernel = injector.getInstance(ProBKernel::class.java)
- }catch (e : de.prob.exception.CliError){
- communicator.sendDebugMessage("wrong path to prob", MessageType.Error)
- throw WrongPathException("wrong path to prob $probHome")
- }
- communicator.sendDebugMessage("returning kernel", MessageType.Info)
-
- return kernel
- }
-
-
- class Test() : Thread(){
-
- }
-
-}
\ No newline at end of file
diff --git a/src/test/kotlin/b/language/server/Client.kt b/src/test/kotlin/b/language/server/Client.kt
new file mode 100644
index 0000000000000000000000000000000000000000..4c12b9d8d60972099a9021558ec6c574e359918f
--- /dev/null
+++ b/src/test/kotlin/b/language/server/Client.kt
@@ -0,0 +1,52 @@
+package b.language.server
+
+import org.eclipse.lsp4j.MessageActionItem
+import org.eclipse.lsp4j.MessageParams
+import org.eclipse.lsp4j.PublishDiagnosticsParams
+import org.eclipse.lsp4j.ShowMessageRequestParams
+import org.eclipse.lsp4j.services.LanguageClient
+import java.util.concurrent.CompletableFuture
+
+class Client : LanguageClient {
+ /**
+ * The telemetry notification is sent from the server to the client to ask
+ * the client to log a telemetry event.
+ */
+ override fun telemetryEvent(`object`: Any?) {
+ TODO("Not yet implemented")
+ }
+
+ /**
+ * Diagnostics notifications are sent from the server to the client to
+ * signal results of validation runs.
+ */
+ override fun publishDiagnostics(diagnostics: PublishDiagnosticsParams?) {
+ TODO("Not yet implemented")
+ }
+
+ /**
+ * The show message notification is sent from a server to a client to ask
+ * the client to display a particular message in the user interface.
+ */
+ override fun showMessage(messageParams: MessageParams?) {
+ println("hi")
+ }
+
+ /**
+ * The show message request is sent from a server to a client to ask the
+ * client to display a particular message in the user interface. In addition
+ * to the show message notification the request allows to pass actions and
+ * to wait for an answer from the client.
+ */
+ override fun showMessageRequest(requestParams: ShowMessageRequestParams?): CompletableFuture<MessageActionItem> {
+ TODO("Not yet implemented")
+ }
+
+ /**
+ * The log message notification is send from the server to the client to ask
+ * the client to log a particular message.
+ */
+ override fun logMessage(message: MessageParams?) {
+ TODO("Not yet implemented")
+ }
+}
\ No newline at end of file
diff --git a/src/test/kotlin/b/language/server/TestApp.kt b/src/test/kotlin/b/language/server/TestApp.kt
new file mode 100644
index 0000000000000000000000000000000000000000..a9238533f49d2dfa554fa4de9b3914e28907fd2a
--- /dev/null
+++ b/src/test/kotlin/b/language/server/TestApp.kt
@@ -0,0 +1,30 @@
+package b.language.server
+
+import b.language.server.proBMangement.prob.ProBKernelManager
+import org.eclipse.lsp4j.jsonrpc.Launcher
+import org.eclipse.lsp4j.launch.LSPLauncher
+import org.eclipse.lsp4j.services.LanguageClient
+import org.eclipse.lsp4j.services.LanguageServer
+import java.io.InputStream
+import java.io.OutputStream
+import java.util.concurrent.Future
+
+
+
+ fun main() {
+ startServer(System.`in`, System.out)
+ }
+
+
+ fun startServer(inputStream: InputStream, outputStream: OutputStream){
+
+
+ val client = Client()
+ val launcher : Launcher<LanguageServer> = LSPLauncher.createClientLauncher(client, inputStream, outputStream)
+ val startListing : Future<*> = launcher.startListening()
+
+
+ startListing.get()
+ }
+
+
diff --git a/src/test/kotlin/b/language/server/prob2/proBMangement/ProBKernelManagerTest.kt b/src/test/kotlin/b/language/server/prob2/proBMangement/ProBKernelManagerTest.kt
index 966ce62b7d4a0cf747b6e499da0ca41da54ce14b..7d41407e6efcc4628e2629c9da71d2e64f92dd6d 100644
--- a/src/test/kotlin/b/language/server/prob2/proBMangement/ProBKernelManagerTest.kt
+++ b/src/test/kotlin/b/language/server/prob2/proBMangement/ProBKernelManagerTest.kt
@@ -1,15 +1,5 @@
package b.language.server.prob2.proBMangement
-import b.language.server.communication.DummyCommunication
-import b.language.server.dataStorage.Settings
-import b.language.server.proBMangement.WrongPathException
-import b.language.server.proBMangement.prob2.ProBKernelManager
-import org.eclipse.lsp4j.Diagnostic
-import org.junit.jupiter.api.Assertions
-import org.junit.jupiter.api.Test
-import java.io.File
-import kotlin.test.assertEquals
-
class ProBKernelManagerTest {
/*
@Test