From 2a466665844729e9d467d0fbe8327cb8401b2881 Mon Sep 17 00:00:00 2001
From: SeeBasTStick <sebastian.stock@hhu.de>
Date: Sun, 18 Oct 2020 15:33:06 +0200
Subject: [PATCH] fixed heavy bug concerning errors without span info would not
shown as result
---
src/main/kotlin/b/language/server/App.kt | 2 +-
.../server/proBMangement/prob/ProBKernel.kt | 42 +++++++++++++------
.../proBMangement/prob/ProBKernelManager.kt | 2 +-
.../server/proBMangement/prob/Util.kt | 15 +++++--
.../proBMangement/prob/WarningListener.kt | 9 ++--
5 files changed, 47 insertions(+), 23 deletions(-)
diff --git a/src/main/kotlin/b/language/server/App.kt b/src/main/kotlin/b/language/server/App.kt
index 3e34983..e86d1da 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 3812518..6447f33 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 3f2a06d..5d6a7aa 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 1d699a1..2edd671 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 3095312..7df1aac 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
--
GitLab