From 00c5159470aebfba3d61ff2037d118f38b27707e Mon Sep 17 00:00:00 2001
From: SeeBasTStick <sebastian.stock@hhu.de>
Date: Tue, 21 Jul 2020 16:38:36 +0200
Subject: [PATCH] added dynamic response, mainly translated existing vscode
server to java
---
.gitignore | 2 +-
build.gradle.kts | 6 +-
.../b/language/server/BDocumentService.kt | 46 ++++++++---
.../b/language/server/BWorkspaceService.kt | 20 ++++-
.../kotlin/b/language/server/ProBInterface.kt | 82 +++++++++++++++++++
.../b/language/server/ProblemHandler.kt | 82 +++++++++++++++++++
src/main/kotlin/b/language/server/Server.kt | 50 +++++++++--
src/main/kotlin/b/language/server/Util.kt | 14 ++++
.../b/language/server/dataStorage/Problem.kt | 19 +++++
.../b/language/server/dataStorage/Settings.kt | 6 ++
10 files changed, 301 insertions(+), 26 deletions(-)
create mode 100644 src/main/kotlin/b/language/server/ProBInterface.kt
create mode 100644 src/main/kotlin/b/language/server/ProblemHandler.kt
create mode 100644 src/main/kotlin/b/language/server/Util.kt
create mode 100644 src/main/kotlin/b/language/server/dataStorage/Problem.kt
create mode 100644 src/main/kotlin/b/language/server/dataStorage/Settings.kt
diff --git a/.gitignore b/.gitignore
index 9460fd2..eac18f6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -27,4 +27,4 @@ hs_err_pid*
# Ignore Gradle build output directory
build
-/.idea/
+/.idea/*
diff --git a/build.gradle.kts b/build.gradle.kts
index 03f0b4e..e87b3b6 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -15,7 +15,6 @@ plugins {
repositories {
// Use jcenter for resolving dependencies.
- // You can declare any Maven/Ivy/file repository here.
jcenter()
}
@@ -26,15 +25,18 @@ dependencies {
// Use the Kotlin JDK 8 standard library.
implementation("org.jetbrains.kotlin:kotlin-stdlib-jdk8")
+ // eclipse lsp implementation
implementation("org.eclipse.lsp4j", "org.eclipse.lsp4j", "0.9.0")
+ // json converter
+ implementation("com.google.code.gson" ,"gson" ,"2.8.6")
+
// Use the Kotlin test library.
testImplementation("org.jetbrains.kotlin:kotlin-test")
// Use the Kotlin JUnit integration.
testImplementation("org.jetbrains.kotlin:kotlin-test-junit")
}
-
application {
// Define the main class for the application.
mainClassName = "b.language.server.AppKt"
diff --git a/src/main/kotlin/b/language/server/BDocumentService.kt b/src/main/kotlin/b/language/server/BDocumentService.kt
index a0dbf76..57534bc 100644
--- a/src/main/kotlin/b/language/server/BDocumentService.kt
+++ b/src/main/kotlin/b/language/server/BDocumentService.kt
@@ -1,14 +1,16 @@
package b.language.server
+import b.language.server.dataStorage.Problem
import org.eclipse.lsp4j.*
-import org.eclipse.lsp4j.jsonrpc.messages.Either
import org.eclipse.lsp4j.services.TextDocumentService
-import java.util.concurrent.CompletableFuture
+import java.io.File
+import java.net.URI
import java.util.concurrent.ConcurrentHashMap
class BDocumentService(private val server: Server) : TextDocumentService {
private val documents = ConcurrentHashMap<String, String>()
+ private val issueTracker : ConcurrentHashMap<String, ArrayList<String>> = ConcurrentHashMap()
/**
* The document open notification is sent from the client to the server to
@@ -29,8 +31,30 @@ class BDocumentService(private val server: Server) : TextDocumentService {
* Registration Options: TextDocumentSaveRegistrationOptions
*/
override fun didSave(params: DidSaveTextDocumentParams?) {
- println("Save")
- TODO("Not yet implemented")
+
+
+ val uri = URI(params!!.textDocument.uri)
+
+ val path = File(uri.path)
+
+ val errorPath = File(path.parent + "/tmp/_error.json")
+ val errorDict = File(path.parent + "/tmp")
+
+ val clientSettings = server.getDocumentSettings(params.textDocument.uri)
+
+ clientSettings.thenAccept{ setting ->
+ val probInterface = ProBInterface(setting.probHome, path, errorDict, errorPath, server = server)
+ probInterface.createFolder()
+ probInterface.performActionOnDocument()
+
+ val problemHandler = ProblemHandler()
+
+ val problemList: List<Problem> = problemHandler.readProblems(errorPath.absolutePath)
+ val diagnostics: List<Diagnostic> = problemHandler.transformProblems(problemList)
+
+ server.languageClient.publishDiagnostics(PublishDiagnosticsParams(params.textDocument.uri, diagnostics))
+ }
+
}
/**
@@ -42,7 +66,7 @@ class BDocumentService(private val server: Server) : TextDocumentService {
* Registration Options: TextDocumentRegistrationOptions
*/
override fun didClose(params: DidCloseTextDocumentParams?) {
- TODO("Not yet implemented")
+ server.documentSettings.remove(params!!.textDocument.uri)
}
/**
@@ -52,16 +76,16 @@ class BDocumentService(private val server: Server) : TextDocumentService {
* Registration Options: TextDocumentChangeRegistrationOptions
*/
override fun didChange(params: DidChangeTextDocumentParams?) {
-
- CompletableFuture.runAsync {
- val diagnostics : ArrayList<Diagnostic> =
- arrayListOf(Diagnostic(Range(Position(1,1), Position(1,1)), "Test", DiagnosticSeverity.Error, "Test"))
- server.languageClient.publishDiagnostics(PublishDiagnosticsParams(params?.textDocument?.uri, diagnostics))
- }
+ //Nothing
}
+
+
+
+
+
}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/BWorkspaceService.kt b/src/main/kotlin/b/language/server/BWorkspaceService.kt
index 2ae8540..70c5159 100644
--- a/src/main/kotlin/b/language/server/BWorkspaceService.kt
+++ b/src/main/kotlin/b/language/server/BWorkspaceService.kt
@@ -1,16 +1,20 @@
package b.language.server
+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.services.WorkspaceService
+import java.io.File
-class BWorkspaceService : 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.
*/
override fun didChangeWatchedFiles(params: DidChangeWatchedFilesParams?) {
- TODO("Not yet implemented")
+ // Not needed
}
/**
@@ -18,6 +22,14 @@ class BWorkspaceService : WorkspaceService {
* configuration settings.
*/
override fun didChangeConfiguration(params: DidChangeConfigurationParams?) {
- TODO("Not yet implemented")
+ if(server.configurationAbility) {
+ server.documentSettings.clear()
+ }else{
+ if (params!!.settings is JsonObject) {
+ val settings: JsonObject = params.settings as JsonObject
+ val documentSetting = castJsonToSetting(settings)
+ server.globalSettings = documentSetting
+ }
+ }
}
-}
\ No newline at end of file
+}
diff --git a/src/main/kotlin/b/language/server/ProBInterface.kt b/src/main/kotlin/b/language/server/ProBInterface.kt
new file mode 100644
index 0000000..745f176
--- /dev/null
+++ b/src/main/kotlin/b/language/server/ProBInterface.kt
@@ -0,0 +1,82 @@
+package b.language.server
+
+import org.eclipse.lsp4j.MessageParams
+import org.eclipse.lsp4j.MessageType
+import java.io.File
+import java.io.FileWriter
+import java.io.InputStream
+
+/**
+ * Interacts with ProB via Commandline
+ * @param probHome the target ProbCli
+ * @param fileToCheck the main machine to start evaluating
+ * @param errorDict the path to store errors
+ * @param wdActive is wd checks enabled?
+ * @param strictActive is strict enabled?
+ * @param performanceHintsActive are performance hints activated?
+ * @param server the server used to connect with
+ */
+class ProBInterface(probHome : File,
+ fileToCheck : File,
+ val errorDict : File,
+ val errorPath : File,
+ wdActive : Boolean = false,
+ strictActive : Boolean = false,
+ performanceHintsActive : Boolean = false,
+ private val server : Server){
+
+
+ private val configuration : String = " -p MAX_INITIALISATIONS 0 -version "
+ private val ndjson : String = " -p NDJSON_ERROR_LOG_FILE "
+ private val wd : String = if(wdActive){
+ " -wd-check -release_java_parser "
+ }else{
+ " "
+ }
+ private val strict : String = if(strictActive){
+ " -p STRICT_CLASH_CHECKING TRUE -p TYPE_CHECK_DEFINITIONS TRUE -lint "
+ }else{
+ " "
+ }
+ private val performanceHints : String = if(performanceHintsActive){
+ " -p PERFORMANCE_INFO TRUE "
+ }else{
+ " "
+ }
+
+ private val command : String
+
+ init {
+ command = probHome.path +
+ configuration +
+ performanceHints +
+ strict +
+ wd +
+ fileToCheck.absoluteFile +
+ ndjson +
+ errorPath.absoluteFile
+ }
+
+
+ fun createFolder() : Boolean{
+ errorDict.mkdirs()
+ FileWriter(errorPath, false).close()
+ return errorDict.mkdirs()
+ }
+
+ /**
+ * Executes the command and returns and sends an error message if something fails
+ */
+ fun performActionOnDocument() {
+ 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 outputAsString = String(output.readAllBytes())
+ if(!outputAsString.contains("ProB Command Line Interface")){
+ server.languageClient.showMessage(
+ MessageParams(MessageType.Error, "Something went wrong when calling probcli $command"))
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/ProblemHandler.kt b/src/main/kotlin/b/language/server/ProblemHandler.kt
new file mode 100644
index 0000000..da05b45
--- /dev/null
+++ b/src/main/kotlin/b/language/server/ProblemHandler.kt
@@ -0,0 +1,82 @@
+package b.language.server
+
+import b.language.server.dataStorage.Problem
+import com.google.gson.Gson
+import org.eclipse.lsp4j.Diagnostic
+import org.eclipse.lsp4j.DiagnosticSeverity
+import org.eclipse.lsp4j.Position
+import org.eclipse.lsp4j.Range
+import java.io.*
+
+
+
+/**
+ * Responsible for reading Errors from the corresponding JSON File and sending transforming them into a object
+ */
+class ProblemHandler {
+
+ /**
+ * 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!!)
+ }
+ }
+
+
+ return jsonStrings.toList().map { string -> Gson().fromJson(string, Problem::class.java) }
+ }
+
+ /**
+ * 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.character == -1 &&
+ problem.end.line == -1 && problem.end.character == -1)
+ {
+ Problem(problem.type,
+ problem.message,
+ problem.reason,
+ problem.file,
+ Position(1, 0),
+ Position(1, Integer.MAX_VALUE),
+ problem.version)
+ }
+ else{
+ problem
+ }
+ }
+ .map { problem -> Diagnostic(Range(problem.start, problem.end), problem.message,
+ when (problem.type) {
+ "error" -> {
+ DiagnosticSeverity.Error
+ }
+ "warning" -> {
+ DiagnosticSeverity.Warning
+ }
+ "information" -> {
+ DiagnosticSeverity.Information
+ }
+ else -> {
+ DiagnosticSeverity.Hint
+ }
+ },
+ problem.file,
+ "probcli v.${problem.version}")}
+ }
+
+}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/Server.kt b/src/main/kotlin/b/language/server/Server.kt
index 3e5e5b1..eab1196 100644
--- a/src/main/kotlin/b/language/server/Server.kt
+++ b/src/main/kotlin/b/language/server/Server.kt
@@ -1,11 +1,14 @@
package b.language.server
+import b.language.server.dataStorage.Settings
+import com.google.gson.JsonObject
import org.eclipse.lsp4j.*
import org.eclipse.lsp4j.services.LanguageClient
import org.eclipse.lsp4j.services.LanguageServer
import org.eclipse.lsp4j.services.TextDocumentService
import org.eclipse.lsp4j.services.WorkspaceService
import java.util.concurrent.CompletableFuture
+import kotlin.collections.HashMap
import kotlin.system.exitProcess
@@ -14,12 +17,13 @@ class Server : LanguageServer {
private val textDocumentService : TextDocumentService
private val bWorkspaceService : WorkspaceService
lateinit var languageClient : LanguageClient
-
-
+ var globalSettings : Settings = Settings()
+ val documentSettings : HashMap<String, CompletableFuture<Settings>> = HashMap()
+ var configurationAbility : Boolean = true;
init {
textDocumentService = BDocumentService(this)
- bWorkspaceService = BWorkspaceService()
+ bWorkspaceService = BWorkspaceService(this)
}
@@ -39,17 +43,18 @@ class Server : LanguageServer {
*/
override fun initialize(params: InitializeParams?): CompletableFuture<InitializeResult> {
val res = InitializeResult(ServerCapabilities())
- res.capabilities.setCodeActionProvider(true)
- res.capabilities.completionProvider = CompletionOptions()
- res.capabilities.definitionProvider = false
+ res.capabilities.setCodeActionProvider(false)
+// res.capabilities.definitionProvider = false
res.capabilities.hoverProvider = false
res.capabilities.referencesProvider = false
res.capabilities.setTextDocumentSync(TextDocumentSyncKind.Full)
res.capabilities.documentSymbolProvider = false
-
return CompletableFuture.supplyAsync { res }
}
+ override fun initialized(params: InitializedParams?) {
+ //languageClient.registerCapability(DidChangeConfigurationCapabilities())
+ }
/**
* The shutdown request is sent from the client to the server. It asks the
@@ -72,7 +77,7 @@ class Server : LanguageServer {
* A notification to ask the server to exit its process.
*/
override fun exit() {
- exitProcess(0);
+ exitProcess(0)
}
@@ -87,4 +92,33 @@ class Server : LanguageServer {
fun setRemoteProxy(remoteProxy: LanguageClient) {
this.languageClient = remoteProxy
}
+
+
+ /**
+ * 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
+ * @param uri the uri of the document requested
+ * @return settings of the document requested
+ */
+ fun getDocumentSettings(uri : String) : CompletableFuture<Settings> {
+ this.languageClient.showMessage(
+ MessageParams(MessageType.Log, "uri $uri " ))
+ if(!configurationAbility){
+ val returnValue = CompletableFuture<Settings>()
+ returnValue.complete(globalSettings)
+ return returnValue
+ }
+ // if client has configuration abilities
+ return if(documentSettings.containsKey(uri))
+ {
+ documentSettings[uri]!!
+ }else{
+ 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]!!
+ }
+ }
}
\ No newline at end of file
diff --git a/src/main/kotlin/b/language/server/Util.kt b/src/main/kotlin/b/language/server/Util.kt
new file mode 100644
index 0000000..9687ebd
--- /dev/null
+++ b/src/main/kotlin/b/language/server/Util.kt
@@ -0,0 +1,14 @@
+package b.language.server
+
+import b.language.server.dataStorage.Settings
+import com.google.gson.Gson
+import com.google.gson.JsonObject
+import java.io.File
+
+fun castJsonToSetting(json : JsonObject) : Settings {
+ return Settings(Gson().fromJson(json.get("maxNumberOfProblems"), Int::class.java),
+ 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)))
+}
\ 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
new file mode 100644
index 0000000..631fd69
--- /dev/null
+++ b/src/main/kotlin/b/language/server/dataStorage/Problem.kt
@@ -0,0 +1,19 @@
+package b.language.server.dataStorage
+
+import org.eclipse.lsp4j.Position
+
+/**
+ * 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
new file mode 100644
index 0000000..9a2ca6f
--- /dev/null
+++ b/src/main/kotlin/b/language/server/dataStorage/Settings.kt
@@ -0,0 +1,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("~/prob_prolog/probcli.sh"))
--
GitLab