diff --git a/src/main/kotlin/b/language/server/App.kt b/src/main/kotlin/b/language/server/App.kt index 66ef528f9a9f2a6624e1fe7a74cc8f4619f4b224..52445468b15d8c43025d9c057a1b029b1805fe03 100644 --- a/src/main/kotlin/b/language/server/App.kt +++ b/src/main/kotlin/b/language/server/App.kt @@ -22,11 +22,6 @@ fun main() { 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 54bb9bb3d597bbbcebb16f3465a993e391f08aa3..57d3d9ccc4c8eb31de89e0fbd08bf99ec6615943 100644 --- a/src/main/kotlin/b/language/server/BDocumentService.kt +++ b/src/main/kotlin/b/language/server/BDocumentService.kt @@ -2,14 +2,14 @@ package b.language.server import b.language.server.communication.CommunicatorInterface 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.IOException import java.util.concurrent.ConcurrentHashMap class BDocumentService(private val server: Server, private val communicator: CommunicatorInterface, - private val proBInterface: ProBInterface) : TextDocumentService { + private val proBInterface: ProBInterface) : TextDocumentService { private val documents = ConcurrentHashMap<String, String>() private val issueTracker : ConcurrentHashMap<String, Set<String>> = ConcurrentHashMap() @@ -62,9 +62,10 @@ class BDocumentService(private val server: Server, invalidFiles.forEach{uri -> communicator.publishDiagnostics(PublishDiagnosticsParams(uri, listOf()))} communicator.sendDebugMessage("invalidating old files $invalidFiles", MessageType.Info) issueTracker[currentUri] = filesWithProblems.toSet() - }catch (e : IOException){ - communicator.sendDebugMessage("command could not be executed", MessageType.Info) - communicator.showMessage(e.message!!, MessageType.Error) + + }catch (e : CouldNotFindProBHomeException){ + communicator.sendDebugMessage(e.message!!, MessageType.Info) + communicator.showMessage(e.message, MessageType.Error) } } diff --git a/src/main/kotlin/b/language/server/Server.kt b/src/main/kotlin/b/language/server/Server.kt index 17cbfa336e45cd5ae195c6937a9a59a4d80dc0de..554624e40ede0a8db3459d5e9cdfebbb5226a2b9 100644 --- a/src/main/kotlin/b/language/server/Server.kt +++ b/src/main/kotlin/b/language/server/Server.kt @@ -2,7 +2,6 @@ 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.* @@ -12,11 +11,11 @@ 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, ProBKernelConnector(Communicator)) + private val textDocumentService : TextDocumentService = BDocumentService(this, Communicator, ProBKernelManager(Communicator)) private val bWorkspaceService : WorkspaceService = BWorkspaceService(this) - lateinit var languageClient : LanguageClient + private lateinit var languageClient : LanguageClient var globalSettings : Settings = Settings() val documentSettings : HashMap<String, CompletableFuture<Settings>> = HashMap() var configurationAbility : Boolean = true @@ -30,9 +29,6 @@ class Server() : LanguageServer{ res.capabilities.workspace = WorkspaceServerCapabilities(WorkspaceFoldersOptions()) res.capabilities.workspace.workspaceFolders.supported = true - // languageClient.registerCapability( - // RegistrationParams(listOf(Registration("all_config_changes", "didChangeConfiguration" , bWorkspaceService)))) - return CompletableFuture.supplyAsync { res } } @@ -75,9 +71,6 @@ class Server() : LanguageServer{ } - - - /** * Get the settings for the current document - will fallback to global settings eventually; If setting not cached * method will try to get setting from the client diff --git a/src/main/kotlin/b/language/server/Util.kt b/src/main/kotlin/b/language/server/Util.kt index 9ba375500fce670aa7af3b6ada0d8b6b5e5ff609..18cee9e6ef858402b4f238d4d948d1e40f29d5ec 100644 --- a/src/main/kotlin/b/language/server/Util.kt +++ b/src/main/kotlin/b/language/server/Util.kt @@ -13,11 +13,11 @@ import java.io.File * @return the settings object */ fun castJsonToSetting(json : JsonObject) : Settings { - return Settings(Gson().fromJson(json.get("maxNumberOfProblems"), Int::class.java), + return Settings( Gson().fromJson(json.get("wdChecks"), Boolean::class.java), Gson().fromJson(json.get("strictChecks"), Boolean::class.java), Gson().fromJson(json.get("performanceHints"), Boolean::class.java), - File(Gson().fromJson(json.get("probHome"), String::class.java)), + Gson().fromJson(json.get("probHome"), String::class.java), Gson().fromJson(json.get("debugMode"), Boolean::class.java)) } diff --git a/src/main/kotlin/b/language/server/dataStorage/Position.kt b/src/main/kotlin/b/language/server/dataStorage/Position.kt deleted file mode 100644 index 14e00846910be7754a8e37eaef51b9d21f26d946..0000000000000000000000000000000000000000 --- a/src/main/kotlin/b/language/server/dataStorage/Position.kt +++ /dev/null @@ -1,4 +0,0 @@ -package b.language.server.dataStorage - - -class Position(var line : Int, var col : Int) \ No newline at end of file diff --git a/src/main/kotlin/b/language/server/dataStorage/Problem.kt b/src/main/kotlin/b/language/server/dataStorage/Problem.kt deleted file mode 100644 index 75648c672771ab97bb1f3ca6423b704172cc2f89..0000000000000000000000000000000000000000 --- a/src/main/kotlin/b/language/server/dataStorage/Problem.kt +++ /dev/null @@ -1,18 +0,0 @@ -package b.language.server.dataStorage - - -/** - * kotlin representation of prob ndjson problems - */ -/** - * @param type type of the problem (error/warning/information( - * @param message problem message - * @param reason reason for the problem to occur - * @param file the file where the problem occurred - * @param start start position of the problem - * @param end end position of the problem - * @version version of porbcli - */ -data class Problem(val type : String , val message: String, val reason : String, val file : String, val start : Position, - val end : Position, val version : String) - diff --git a/src/main/kotlin/b/language/server/dataStorage/Settings.kt b/src/main/kotlin/b/language/server/dataStorage/Settings.kt index 895add03742e44d44057ba0fcbbb90f89bf7edcc..50b5117c6b7131fab64445a1446dcd0ae1daffa7 100644 --- a/src/main/kotlin/b/language/server/dataStorage/Settings.kt +++ b/src/main/kotlin/b/language/server/dataStorage/Settings.kt @@ -2,6 +2,6 @@ package b.language.server.dataStorage import java.io.File -data class Settings(val maxNumberOfProblem : Int = 1000, val strictChecks : Boolean = true, val wdChecks : Boolean = true, - val performanceHints : Boolean = true , val probHome : File = File("DEFAULT"), +data class Settings(val strictChecks : Boolean = true, val wdChecks : Boolean = true, + val performanceHints : Boolean = true , val probHome : String = "DEFAULT", val debugMode : Boolean = true) diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/CouldNotFindProBHomeException.kt b/src/main/kotlin/b/language/server/proBMangement/prob/CouldNotFindProBHomeException.kt new file mode 100644 index 0000000000000000000000000000000000000000..e4adfa316c5d0fae6fab84e783f691ca17013495 --- /dev/null +++ b/src/main/kotlin/b/language/server/proBMangement/prob/CouldNotFindProBHomeException.kt @@ -0,0 +1,3 @@ +package b.language.server.proBMangement.prob + +class CouldNotFindProBHomeException(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 deleted file mode 100644 index 795d1efac2a671703dc8292bb38fbb7752f79d46..0000000000000000000000000000000000000000 --- a/src/main/kotlin/b/language/server/proBMangement/prob/MessageTypes.kt +++ /dev/null @@ -1,7 +0,0 @@ -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/prob/ProBKernel.kt b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt index 10fe68a99764071eef83e10b9d2c503e0c15b06d..966642bdb6a6d0ab92d6102bf84dd0516826c60a 100644 --- a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt +++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt @@ -1,10 +1,9 @@ +package b.language.server.proBMangement.prob + -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.prob.MyWarningListener -import b.language.server.proBMangement.prob.convertErrorItems import com.google.inject.Inject import com.google.inject.Injector import de.prob.animator.ReusableAnimator @@ -20,63 +19,90 @@ import org.eclipse.lsp4j.Diagnostic import org.eclipse.lsp4j.MessageType import java.io.IOException - -class ProBKernel @Inject constructor(private val injector : Injector, val classicalBFactory : ClassicalBFactory, +/** + * Represents the interface to communicate with prob kernel + * Is called via injector + * @see ProBKernelManager + */ +class ProBKernel @Inject constructor(private val injector : Injector, + val classicalBFactory : ClassicalBFactory, private val animationSelector: AnimationSelector, - private val animator : ReusableAnimator) { - + private val animator : ReusableAnimator, + private val communicator : CommunicatorInterface) { - val communicator = CommunicationCollector() - fun check(path : String, settings : ProBSettings) : Pair<List<Diagnostic>, List<Pair<String, MessageType>>>{ - communicator.log.clear() + /** + * Checks the given machine file; prepares all necessary object + * @param path the file to check + * @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>{ Communicator.sendDebugMessage("Unload old machine", MessageType.Info) unloadMachine() + + //TODO Rules factory val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(path.substringAfterLast("."))) - val warningListener = MyWarningListener() + val warningListener = WarningListener() animator.addWarningListener(warningListener) val parseErrors = mutableListOf<Diagnostic>() Communicator.sendDebugMessage("Load new machine", MessageType.Info) - loadMachine( + + val strictProblems = loadMachine( { stateSpace : StateSpace -> try { - val extractedModel = factory.extract(path) - val stateSpaceWithSettings = extractedModel.load(prepareAdditionalSettings(settings)) - extractedModel.loadIntoStateSpace(stateSpaceWithSettings) + factory.extract(path).loadIntoStateSpace(stateSpace) } catch (e: IOException) { - // throw RuntimeException(e) communicator.sendDebugMessage("IOException ${e.message}", MessageType.Info) } catch (e: ModelTranslationError) { communicator.sendDebugMessage("ModelTranslationError ${e.message}", MessageType.Info) - - // throw RuntimeException(e) }catch (e : ProBError){ parseErrors.addAll(convertErrorItems(e.errors)) } Trace(stateSpace) }, settings) - return Pair(listOf(warningListener.getWarnings(), parseErrors).flatten(), communicator.log) + communicator.sendDebugMessage("returning from kernel", MessageType.Info) + return listOf(warningListener.getWarnings(), parseErrors).flatten() } + /** + * Does the main work + * @param newTraceCreator a anonymous function dealing with the state space + * @param settings the settings to be applied + */ private fun loadMachine(newTraceCreator :java.util.function.Function<StateSpace, Trace>, settings: ProBSettings){ val newStateSpace = animator.createStateSpace() + newStateSpace.changePreferences(prepareAdditionalSettings(settings)) try { + communicator.sendDebugMessage("changing animation", MessageType.Info) animationSelector.changeCurrentAnimation(newTraceCreator.apply(newStateSpace)) + communicator.sendDebugMessage("executing optional steps", MessageType.Info) executeAdditionalOptions(settings) + newStateSpace.performExtendedStaticChecks() //TODO move to additional options + communicator.sendDebugMessage("returning...", MessageType.Info) + } catch (e: RuntimeException) { newStateSpace.kill() throw e } } + + /** + * executes additional commands, which are defined as separate command, all others are executed at + * @see prepareAdditionalSettings + * @param settings the settings to be executed as command + */ private fun executeAdditionalOptions(settings : ProBSettings){ - // animator.createStateSpace() if(settings.wdChecks){ - animator.execute(CheckWellDefinednessCommand()) + communicator.sendDebugMessage("Doing WD checks", MessageType.Info) + animator.execute(CheckWellDefinednessCommand()) } - } + /** + * to clean up a machine + */ private fun unloadMachine() { val oldTrace = animationSelector.currentTrace if (oldTrace != null) { @@ -87,6 +113,11 @@ class ProBKernel @Inject constructor(private val injector : Injector, val classi } + /** + * prepares a map with additional settings + * @param proBSettings the settings to put in the map + * @return the settings map + */ private fun prepareAdditionalSettings(proBSettings: ProBSettings): MutableMap<String, String> { val settings = mutableMapOf<String, String>() if(proBSettings.performanceHints) { diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelConnector.kt b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelConnector.kt deleted file mode 100644 index 4027ccf4381db5dcb47f7f09ddfb765ffca10acc..0000000000000000000000000000000000000000 --- a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelConnector.kt +++ /dev/null @@ -1,87 +0,0 @@ -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 index 4b1b9fdb774b197332bd1a85ddb4e55f263ca44f..f18f925e359b4678c0678c31fa1bd627510db62a 100644 --- a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt +++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt @@ -1,96 +1,82 @@ package b.language.server.proBMangement.prob -import ProBKernel -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.dataStorage.Settings -import com.google.gson.Gson +import b.language.server.proBMangement.ProBInterface import com.google.inject.Guice import com.google.inject.Stage +import org.eclipse.lsp4j.Diagnostic import org.eclipse.lsp4j.MessageType -import org.zeromq.SocketType - -import org.zeromq.ZContext -import org.zeromq.ZMQ +import java.io.File import java.net.URI /** - * Creates the prob kernel access and maintaince a stady connection + * Creates the prob kernel access and maintenance */ -class ProBKernelManager : Thread() { - - private var active = true - private lateinit var kernel : ProBKernel - private var probHome = "" - private val communicator = CommunicationCollector() - +class ProBKernelManager(private val communicator : CommunicatorInterface) : ProBInterface { + private var kernel : ProBKernel + private var probHome = "DEFAULT" - 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()) + init{ + kernel = setup() } /** - * @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) - - + private fun setup() : ProBKernel { + val injector = Guice.createInjector(Stage.PRODUCTION, ProBKernelModule(communicator)) 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 } + + /** + * Checks if the given prob home matches - if not a knew prob kernel will be initialized + * @param probNewHome the potential new proB home + * @return changes was successful/no change at all + */ + private fun checkProBVersionSetting(probNewHome : String) : Boolean{ + return if(probNewHome != probHome) + { + if(File(probNewHome).exists()) { + System.setProperty("prob.home", "/home/sebastian/prob_prolog") + kernel = setup() + probHome = probNewHome + true + } else{ + false + } + }else{ + true + } + } + + + /** + * 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 + * + * @throws CouldNotFindProBHomeException the given path ist not "DEFAULT" and wrong + */ + override fun checkDocument(uri: String, settings: Settings): List<Diagnostic> { + val path = URI(uri).path + communicator.sendDebugMessage("try to use ${settings.probHome} as prob version", MessageType.Info) + val result = checkProBVersionSetting(settings.probHome) + if(!result){ + throw CouldNotFindProBHomeException("searched at ${settings.probHome} for prob but found nothing") + } + communicator.sendDebugMessage("success...", MessageType.Info) + communicator.sendDebugMessage("checking document", MessageType.Info) + return kernel.check(path, 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/ProBKernelModule.kt b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelModule.kt index 88b8286a32d3d5d2696ac64615652ff791ed3ca6..b66e683ebfddcbb4bde88b694f2ceb34f56dddf9 100644 --- a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelModule.kt +++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelModule.kt @@ -1,11 +1,13 @@ package b.language.server.proBMangement.prob +import b.language.server.communication.Communicator import b.language.server.communication.CommunicatorInterface import com.google.inject.AbstractModule import de.prob.MainModule -class ProBKernelModule() : AbstractModule() { +class ProBKernelModule(val communicator : CommunicatorInterface) : AbstractModule() { override fun configure() { install(MainModule()) + bind(CommunicatorInterface::class.java).toInstance(communicator) } } \ 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 deleted file mode 100644 index 0e48ca2587f5c74665034d0a4a205c9ee589c470..0000000000000000000000000000000000000000 --- a/src/main/kotlin/b/language/server/proBMangement/prob/Reply.kt +++ /dev/null @@ -1,7 +0,0 @@ -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 deleted file mode 100644 index 4bf4d78a5304185e28c728fbea3b2f6dd20289bd..0000000000000000000000000000000000000000 --- a/src/main/kotlin/b/language/server/proBMangement/prob/Request.kt +++ /dev/null @@ -1,5 +0,0 @@ -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 deleted file mode 100644 index bcadcb2c7cf81d29de5066e95f99a3b1a4722a82..0000000000000000000000000000000000000000 --- a/src/main/kotlin/b/language/server/proBMangement/prob/ServerConnection.kt +++ /dev/null @@ -1,9 +0,0 @@ -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/prob/Util.kt b/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt index 83fb00974c7befb909f3e04264cf35c8b4bb9fa6..d0d3c444c4bca463f4ae6fdb52f767e3f4189960 100644 --- a/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt +++ b/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt @@ -9,7 +9,7 @@ import org.eclipse.lsp4j.Range fun convertErrorItems(errorItems : List<ErrorItem>) : List<Diagnostic>{ return errorItems.toList().map { errorItem -> errorItem.locations.map { location -> - Diagnostic(Range(Position(location.startLine, location.startColumn), Position(location.endLine, location.endColumn)), + Diagnostic(Range(Position(location.startLine-1, location.startColumn), Position(location.endLine-1, location.endColumn)), errorItem.message, getErrorItemType(errorItem), location.filename) diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/MyWarningListener.kt b/src/main/kotlin/b/language/server/proBMangement/prob/WarningListener.kt similarity index 82% rename from src/main/kotlin/b/language/server/proBMangement/prob/MyWarningListener.kt rename to src/main/kotlin/b/language/server/proBMangement/prob/WarningListener.kt index 676130b347a2ef972d33fd4e3a0598e892f7511a..8c51998438a95c2d8888658365a15d0fa97c8646 100644 --- a/src/main/kotlin/b/language/server/proBMangement/prob/MyWarningListener.kt +++ b/src/main/kotlin/b/language/server/proBMangement/prob/WarningListener.kt @@ -5,8 +5,10 @@ import de.prob.animator.domainobjects.ErrorItem import org.eclipse.lsp4j.Diagnostic import org.eclipse.lsp4j.DiagnosticSeverity - -class MyWarningListener : IWarningListener { +/** + * Custom collector to collect warnings from prob kernel + */ +class WarningListener : IWarningListener { private val warningList : ArrayList<ErrorItem> = arrayListOf() override fun warningsOccurred(warnings: MutableList<ErrorItem>?) { warningList.addAll(warnings!!.toList()) diff --git a/src/test/kotlin/b/language/server/ProBCommandLineTest.kt b/src/test/kotlin/b/language/server/ProBCommandLineTest.kt index 06bec3e31542f2c19c5b103dcea1cd3785042fcf..6784d0370572727f95553f87b778bd8e85de1284 100644 --- a/src/test/kotlin/b/language/server/ProBCommandLineTest.kt +++ b/src/test/kotlin/b/language/server/ProBCommandLineTest.kt @@ -1,18 +1,5 @@ package b.language.server -import b.language.server.dataStorage.Position -import b.language.server.dataStorage.Problem -import b.language.server.dataStorage.Settings -import com.google.gson.Gson -import org.eclipse.lsp4j.Diagnostic -import org.eclipse.lsp4j.DiagnosticSeverity -import org.eclipse.lsp4j.Range -import kotlin.test.Test -import org.junit.jupiter.api.io.TempDir -import java.io.File -import kotlin.test.assertEquals -import kotlin.test.assertTrue - class ProBCommandLineTest{ /* @Test