diff --git a/src/main/kotlin/b/language/server/App.kt b/src/main/kotlin/b/language/server/App.kt
index 52445468b15d8c43025d9c057a1b029b1805fe03..e86d1daef477dbc04b24022e9d5b8ed887bd4838 100644
--- a/src/main/kotlin/b/language/server/App.kt
+++ b/src/main/kotlin/b/language/server/App.kt
@@ -1,20 +1,16 @@
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.*
-import java.net.InetAddress
import java.net.ServerSocket
-import java.net.Socket
-import java.nio.charset.StandardCharsets
import java.util.concurrent.Future
fun main() {
println("opening connection and waiting ...")
- val socket = ServerSocket(5555)
+ val socket = ServerSocket(55555)
val channel = socket.accept()
println("accepted connection from ${channel.inetAddress}")
startServer(channel.getInputStream(), channel.getOutputStream())
diff --git a/src/main/kotlin/b/language/server/BWorkspaceService.kt b/src/main/kotlin/b/language/server/BWorkspaceService.kt
index 86952c373a3124505e161356b45e5c8de4fd5af7..6ed6d36fb5b84f20ff3321132083b81a23e119d6 100644
--- a/src/main/kotlin/b/language/server/BWorkspaceService.kt
+++ b/src/main/kotlin/b/language/server/BWorkspaceService.kt
@@ -8,13 +8,13 @@ import org.eclipse.lsp4j.MessageType
import org.eclipse.lsp4j.services.WorkspaceService
-class BWorkspaceService(private val server: Server) : WorkspaceService {
+class BWorkspaceService(private val server: Server, val communicator: Communicator) : 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?) {
- Communicator.sendDebugMessage("----------changed watched files", MessageType.Info)
+ communicator.sendDebugMessage("----------changed watched files", MessageType.Info)
// Not needed
}
@@ -24,7 +24,7 @@ class BWorkspaceService(private val server: Server) : WorkspaceService {
* configuration settings.
*/
override fun didChangeConfiguration(params: DidChangeConfigurationParams?) {
- Communicator.sendDebugMessage("received change in configuration settings", MessageType.Info)
+ communicator.sendDebugMessage("received change in configuration settings", MessageType.Info)
if(server.configurationAbility) {
server.documentSettings.clear()
}else{
diff --git a/src/main/kotlin/b/language/server/Server.kt b/src/main/kotlin/b/language/server/Server.kt
index 554624e40ede0a8db3459d5e9cdfebbb5226a2b9..1f751b120b8fb90dbbab7c38d3f5217cc9893501 100644
--- a/src/main/kotlin/b/language/server/Server.kt
+++ b/src/main/kotlin/b/language/server/Server.kt
@@ -14,7 +14,7 @@ import kotlin.system.exitProcess
class Server : LanguageServer{
private val textDocumentService : TextDocumentService = BDocumentService(this, Communicator, ProBKernelManager(Communicator))
- private val bWorkspaceService : WorkspaceService = BWorkspaceService(this)
+ private val bWorkspaceService : WorkspaceService = BWorkspaceService(this, Communicator)
private lateinit var languageClient : LanguageClient
var globalSettings : Settings = Settings()
val documentSettings : HashMap<String, CompletableFuture<Settings>> = HashMap()
diff --git a/src/main/kotlin/b/language/server/Util.kt b/src/main/kotlin/b/language/server/Util.kt
index 18cee9e6ef858402b4f238d4d948d1e40f29d5ec..ce0811270e1ee8d1be53e1d0143ea62401f92db0 100644
--- a/src/main/kotlin/b/language/server/Util.kt
+++ b/src/main/kotlin/b/language/server/Util.kt
@@ -4,7 +4,6 @@ import b.language.server.dataStorage.Settings
import com.google.gson.Gson
import com.google.gson.JsonObject
-import java.io.File
/**
@@ -21,3 +20,5 @@ fun castJsonToSetting(json : JsonObject) : Settings {
Gson().fromJson(json.get("debugMode"), Boolean::class.java))
}
+
+
diff --git a/src/main/kotlin/b/language/server/dataStorage/Settings.kt b/src/main/kotlin/b/language/server/dataStorage/Settings.kt
index 50b5117c6b7131fab64445a1446dcd0ae1daffa7..40708a60950e5603a7d112f26b9dfd53afd867f0 100644
--- a/src/main/kotlin/b/language/server/dataStorage/Settings.kt
+++ b/src/main/kotlin/b/language/server/dataStorage/Settings.kt
@@ -1,6 +1,5 @@
package b.language.server.dataStorage
-import java.io.File
data class Settings(val strictChecks : Boolean = true, val wdChecks : Boolean = true,
val performanceHints : Boolean = true , val probHome : String = "DEFAULT",
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 966642bdb6a6d0ab92d6102bf84dd0516826c60a..6eb1e55814e20ad4824510dae70d91dfce5d8c53 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
@@ -4,10 +4,12 @@ package b.language.server.proBMangement.prob
import b.language.server.communication.Communicator
import b.language.server.communication.CommunicatorInterface
import b.language.server.dataStorage.ProBSettings
+import com.google.gson.Gson
import com.google.inject.Inject
import com.google.inject.Injector
import de.prob.animator.ReusableAnimator
import de.prob.animator.command.CheckWellDefinednessCommand
+import de.prob.animator.domainobjects.ErrorItem
import de.prob.exception.ProBError
import de.prob.scripting.ClassicalBFactory
import de.prob.scripting.FactoryProvider
@@ -17,7 +19,10 @@ import de.prob.statespace.StateSpace
import de.prob.statespace.Trace
import org.eclipse.lsp4j.Diagnostic
import org.eclipse.lsp4j.MessageType
+import org.ietf.jgss.GSSContext
+import java.io.File
import java.io.IOException
+import java.nio.charset.Charset
/**
* Represents the interface to communicate with prob kernel
@@ -41,12 +46,13 @@ class ProBKernel @Inject constructor(private val injector : Injector,
Communicator.sendDebugMessage("Unload old machine", MessageType.Info)
unloadMachine()
- //TODO Rules factory
val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(path.substringAfterLast(".")))
+
val warningListener = WarningListener()
animator.addWarningListener(warningListener)
val parseErrors = mutableListOf<Diagnostic>()
- Communicator.sendDebugMessage("Load new machine", MessageType.Info)
+
+ Communicator.sendDebugMessage("loading new machine", MessageType.Info)
val strictProblems = loadMachine(
{ stateSpace : StateSpace ->
@@ -61,8 +67,10 @@ class ProBKernel @Inject constructor(private val injector : Injector,
}
Trace(stateSpace)
}, settings)
+
communicator.sendDebugMessage("returning from kernel", MessageType.Info)
- return listOf(warningListener.getWarnings(), parseErrors).flatten()
+
+ return listOf(warningListener.getWarnings(), parseErrors, strictProblems).flatten()
}
/**
@@ -70,21 +78,28 @@ class ProBKernel @Inject constructor(private val injector : Injector,
* @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){
+ private fun loadMachine(newTraceCreator :java.util.function.Function<StateSpace, Trace>, settings: ProBSettings): List<Diagnostic> {
val newStateSpace = animator.createStateSpace()
newStateSpace.changePreferences(prepareAdditionalSettings(settings))
+ val resultLint = mutableListOf<ErrorItem>() // see java doc of prepareAdditionalSettings
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
+
+ if (settings.strictChecks) {
+ resultLint.addAll(newStateSpace.performExtendedStaticChecks())
+ }
+
communicator.sendDebugMessage("returning...", MessageType.Info)
} catch (e: RuntimeException) {
newStateSpace.kill()
throw e
}
+
+ return convertErrorItems(resultLint)
}
@@ -115,6 +130,7 @@ class ProBKernel @Inject constructor(private val injector : Injector,
/**
* prepares a map with additional settings
+ * note that the -lint option is an extra call to the state space and must be performed elsewhere
* @param proBSettings the settings to put in the map
* @return the settings map
*/
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 f18f925e359b4678c0678c31fa1bd627510db62a..4370b32694c801cc064bb1f1e13147bc42b18bc3 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt
@@ -10,6 +10,8 @@ import org.eclipse.lsp4j.Diagnostic
import org.eclipse.lsp4j.MessageType
import java.io.File
import java.net.URI
+import java.nio.file.Files
+import java.nio.file.Path
/**
* Creates the prob kernel access and maintenance
@@ -46,13 +48,21 @@ class ProBKernelManager(private val communicator : CommunicatorInterface) : ProB
private fun checkProBVersionSetting(probNewHome : String) : Boolean{
return if(probNewHome != probHome)
{
- if(File(probNewHome).exists()) {
- System.setProperty("prob.home", "/home/sebastian/prob_prolog")
+ if(probNewHome == "DEFAULT"){ //Use default prob
+ System.setProperty("prob.home", "null")
kernel = setup()
probHome = probNewHome
true
- } else{
- false
+ }
+ else {
+ if (File(probNewHome).exists()) { // Use custom prob
+ System.setProperty("prob.home", probNewHome)
+ kernel = setup()
+ probHome = probNewHome
+ true
+ } else {
+ false
+ }
}
}else{
true
@@ -70,12 +80,15 @@ class ProBKernelManager(private val communicator : CommunicatorInterface) : ProB
*/
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)
+
+ Files.exists(Path.of(URI(uri)))
+ communicator.sendDebugMessage("try to use ${settings.probHome} as prob version instead of ${System.getProperty("prob.home")}", 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))
}
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 b66e683ebfddcbb4bde88b694f2ceb34f56dddf9..25465911a116652a3a391224b3e8aac7e766e4b5 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,10 @@
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(val communicator : CommunicatorInterface) : AbstractModule() {
+class ProBKernelModule(private val communicator : CommunicatorInterface) : AbstractModule() {
override fun configure() {
install(MainModule())
bind(CommunicatorInterface::class.java).toInstance(communicator)
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 d0d3c444c4bca463f4ae6fdb52f767e3f4189960..fa1a55be050f898427f6a8ef51754a7f5818bad9 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt
@@ -5,11 +5,16 @@ import org.eclipse.lsp4j.Diagnostic
import org.eclipse.lsp4j.DiagnosticSeverity
import org.eclipse.lsp4j.Position
import org.eclipse.lsp4j.Range
+import java.io.BufferedWriter
+import java.io.File
+import java.io.FileOutputStream
+import java.io.OutputStreamWriter
-fun convertErrorItems(errorItems : List<ErrorItem>) : List<Diagnostic>{
+
+fun convertErrorItems(errorItems: List<ErrorItem>) : List<Diagnostic>{
return errorItems.toList().map { errorItem ->
errorItem.locations.map { location ->
- Diagnostic(Range(Position(location.startLine-1, location.startColumn), Position(location.endLine-1, location.endColumn)),
+ Diagnostic(Range(Position(location.startLine - 1, location.startColumn), Position(location.endLine - 1, location.endColumn)),
errorItem.message,
getErrorItemType(errorItem),
location.filename)
@@ -17,7 +22,7 @@ fun convertErrorItems(errorItems : List<ErrorItem>) : List<Diagnostic>{
}.flatten()
}
-fun getErrorItemType(errorItem : ErrorItem) : DiagnosticSeverity{
+fun getErrorItemType(errorItem: ErrorItem) : DiagnosticSeverity{
return when(errorItem.type){
ErrorItem.Type.ERROR -> {
DiagnosticSeverity.Error