added dynamic response, mainly translated existing vscode server to java

.gitignore

@@ -27,4 +27,4 @@ hs_err_pid*
 
 # Ignore Gradle build output directory
 build
-/.idea/
+/.idea/*

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"

src/main/kotlin/b/language/server/BDocumentService.kt

 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

src/main/kotlin/b/language/server/BWorkspaceService.kt

 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
+            }
+        }
     }
 }

src/main/kotlin/b/language/server/ProBInterface.kt

+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

src/main/kotlin/b/language/server/ProblemHandler.kt

+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

src/main/kotlin/b/language/server/Server.kt

 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

src/main/kotlin/b/language/server/Util.kt

+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

src/main/kotlin/b/language/server/dataStorage/Problem.kt

+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)
+

src/main/kotlin/b/language/server/dataStorage/Settings.kt

+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"))