diff --git a/src/main/kotlin/b/language/server/App.kt b/src/main/kotlin/b/language/server/App.kt
index 3e34983c1d6ac095609619917bf17e43da716a28..e86d1daef477dbc04b24022e9d5b8ed887bd4838 100644
--- a/src/main/kotlin/b/language/server/App.kt
+++ b/src/main/kotlin/b/language/server/App.kt
@@ -10,7 +10,7 @@ import java.util.concurrent.Future
fun main() {
println("opening connection and waiting ...")
- val socket = ServerSocket(55556)
+ 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/proBMangement/prob/ProBKernel.kt b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
index 3812518fb94c6176b866c73bf37c949d91d3cfd6..6447f330d5e87814e5567cfaa32feb8ddbe3923f 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernel.kt
@@ -16,6 +16,7 @@ import de.prob.scripting.ModelTranslationError
import de.prob.statespace.AnimationSelector
import de.prob.statespace.StateSpace
import de.prob.statespace.Trace
+import kotlinx.coroutines.flow.flowViaChannel
import org.eclipse.lsp4j.Diagnostic
import org.eclipse.lsp4j.MessageType
import java.io.IOException
@@ -44,29 +45,30 @@ class ProBKernel @Inject constructor(private val injector : Injector,
val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(path.substringAfterLast(".")))
- val informationListener = InformationListener()
+ val informationListener = InformationListener(path)
animator.addWarningListener(informationListener)
- val parseErrors = mutableListOf<Diagnostic>()
Communicator.sendDebugMessage("loading new machine", MessageType.Info)
+ val errors = mutableListOf<ErrorItem>()
val strictProblems = loadMachine(
- { stateSpace : StateSpace ->
+ {
+ stateSpace : StateSpace ->
try {
factory.extract(path).loadIntoStateSpace(stateSpace)
} catch (e: IOException) {
communicator.sendDebugMessage("IOException ${e.message}", MessageType.Info)
} catch (e: ModelTranslationError) {
communicator.sendDebugMessage("ModelTranslationError ${e.message}", MessageType.Info)
- }catch (e : ProBError){
- parseErrors.addAll(convertErrorItems(e.errors))
+ } catch (e : ProBError){
+ errors.addAll(e.errors)
}
Trace(stateSpace)
- }, settings)
+ }, settings, path)
- communicator.sendDebugMessage("returning from kernel", MessageType.Info)
+ communicator.sendDebugMessage("returning from kernel problems are ${strictProblems.toString()}", MessageType.Info)
- return listOf(informationListener.getInformation(), parseErrors, strictProblems).flatten()
+ return listOf(informationListener.getInformation(), strictProblems, convertErrorItems(errors, path)).flatten()
}
/**
@@ -74,28 +76,37 @@ 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): List<Diagnostic> {
+ private fun loadMachine(newTraceCreator :java.util.function.Function<StateSpace, Trace>, settings: ProBSettings,
+ path : String): List<Diagnostic> {
+ communicator.sendDebugMessage("creating new state space", MessageType.Info)
+
val newStateSpace = animator.createStateSpace()
+ communicator.sendDebugMessage("setting preferences", MessageType.Info)
newStateSpace.changePreferences(prepareAdditionalSettings(settings))
- val resultLint = mutableListOf<ErrorItem>() // see java doc of prepareAdditionalSettings
+ val errors = mutableListOf<ErrorItem>()
try {
communicator.sendDebugMessage("changing animation", MessageType.Info)
animationSelector.changeCurrentAnimation(newTraceCreator.apply(newStateSpace))
+ communicator.sendDebugMessage("done", MessageType.Info)
+
communicator.sendDebugMessage("executing optional steps", MessageType.Info)
executeAdditionalOptions(settings)
if (settings.strictChecks) {
- resultLint.addAll(newStateSpace.performExtendedStaticChecks())
+ errors.addAll(newStateSpace.performExtendedStaticChecks())
}
communicator.sendDebugMessage("finished evaluation", MessageType.Info)
- } catch (e: RuntimeException) {
+ }catch (e: RuntimeException) {
+ communicator.sendDebugMessage("something bad happened, statespace was killed", MessageType.Warning)
newStateSpace.kill()
throw e
}
- return convertErrorItems(resultLint)
+ communicator.sendDebugMessage("processing errors", MessageType.Info)
+
+ return convertErrorItems(errors, path)
}
@@ -135,9 +146,14 @@ class ProBKernel @Inject constructor(private val injector : Injector,
if(proBSettings.performanceHints) {
settings["STRICT_CLASH_CHECKING"] = "TRUE"
settings["TYPE_CHECK_DEFINITIONS"] = "TRUE"
+ }else{
+ settings["STRICT_CLASH_CHECKING"] = "TRUE"
+ settings["TYPE_CHECK_DEFINITIONS"] = "TRUE"
}
if (proBSettings.strictChecks) {
settings["PERFORMANCE_INFO"] = "TRUE"
+ }else{
+ settings["PERFORMANCE_INFO"] = "TRUE"
}
return settings
}
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 3f2a06dfe8058cf671785b4b42f603bb87d2aebd..5d6a7aa11336d2c3cd3ca2b6ff476b6f280b12e4 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/ProBKernelManager.kt
@@ -49,7 +49,7 @@ class ProBKernelManager(private val communicator : CommunicatorInterface) : ProB
return if(probNewHome != probHome)
{
if(probNewHome == "DEFAULT"){ //Use default prob
- System.setProperty("prob.home", "DEFAULT")
+ System.setProperty("prob.home", "null")
kernel = setup()
probHome = probNewHome
true
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 1d699a147b3ece53f96b3ad8a0616bb3e6079d08..2edd6719ca3874cab2d365ed8f9050b54d12aede 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/Util.kt
@@ -6,8 +6,8 @@ import org.eclipse.lsp4j.DiagnosticSeverity
import org.eclipse.lsp4j.Position
import org.eclipse.lsp4j.Range
-fun convertErrorItems(errorItems: List<ErrorItem>) : List<Diagnostic>{
- return errorItems.toList().map { errorItem ->
+fun convertErrorItems(errorItems: List<ErrorItem>, currentLoadedFile : String) : List<Diagnostic>{
+ return errorItems.map { errorItem ->
errorItem.locations.map { location ->
Diagnostic(Range(
Position(location.startLine - 1, location.startColumn),
@@ -15,6 +15,13 @@ fun convertErrorItems(errorItems: List<ErrorItem>) : List<Diagnostic>{
errorItem.message,
getErrorItemType(errorItem.type),
location.filename)
+ }.ifEmpty { //Fallback when errors from prob do not have position infos
+ listOf(Diagnostic(Range(
+ Position(0,0),
+ Position(0,0)),
+ errorItem.message,
+ getErrorItemType(errorItem.type),
+ currentLoadedFile))
}
}.flatten()
}
@@ -30,9 +37,9 @@ fun getErrorItemType(errorItem: ErrorItem.Type) : DiagnosticSeverity{
ErrorItem.Type.INTERNAL_ERROR -> {
DiagnosticSeverity.Error
}
- ErrorItem.Type.MESSAGE -> {
+ /* ErrorItem.Type.MESSAGE -> {
DiagnosticSeverity.Information
- }
+ }*/
else -> {
DiagnosticSeverity.Error
}
diff --git a/src/main/kotlin/b/language/server/proBMangement/prob/WarningListener.kt b/src/main/kotlin/b/language/server/proBMangement/prob/WarningListener.kt
index 3095312d88db9cc62ee027a794f395c2b23fa9c9..7df1aac275b4086287523067fdcbc56357b6f4a5 100644
--- a/src/main/kotlin/b/language/server/proBMangement/prob/WarningListener.kt
+++ b/src/main/kotlin/b/language/server/proBMangement/prob/WarningListener.kt
@@ -1,20 +1,21 @@
package b.language.server.proBMangement.prob
-import de.prob.animator.IInformationListener
+import de.prob.animator.IWarningListener
import de.prob.animator.domainobjects.ErrorItem
import org.eclipse.lsp4j.Diagnostic
-import org.eclipse.lsp4j.DiagnosticSeverity
/**
* Custom collector to collect warnings from prob kernel
*/
-class InformationListener : IInformationListener {
+class InformationListener(val fallbackPath : String) : IWarningListener {
private val warningList : ArrayList<ErrorItem> = arrayListOf()
+
+
override fun warningsOccurred(warnings: MutableList<ErrorItem>?) {
warningList.addAll(warnings!!.toList())
}
fun getInformation() : List<Diagnostic>{
- return convertErrorItems(warningList)
+ return convertErrorItems(warningList, fallbackPath)
}
}
\ No newline at end of file