Skip to content
Snippets Groups Projects
Commit a2f921f0 authored by SeeBasTStick's avatar SeeBasTStick
Browse files

added information from probKernel

parent d3629399
Branches
Tags
No related merge requests found
...@@ -8,3 +8,4 @@ ...@@ -8,3 +8,4 @@
*/ */
rootProject.name = "b-language-server" rootProject.name = "b-language-server"
includeBuild("../prob2_kernel/de.prob2.kernel")
\ No newline at end of file
...@@ -10,7 +10,7 @@ import java.util.concurrent.Future ...@@ -10,7 +10,7 @@ import java.util.concurrent.Future
fun main() { fun main() {
println("opening connection and waiting ...") println("opening connection and waiting ...")
val socket = ServerSocket(55555) val socket = ServerSocket(55556)
val channel = socket.accept() val channel = socket.accept()
println("accepted connection from ${channel.inetAddress}") println("accepted connection from ${channel.inetAddress}")
startServer(channel.getInputStream(), channel.getOutputStream()) startServer(channel.getInputStream(), channel.getOutputStream())
......
...@@ -55,7 +55,7 @@ class BDocumentService(private val server: Server, ...@@ -55,7 +55,7 @@ class BDocumentService(private val server: Server,
try{ try{
val diagnostics: List<Diagnostic> = proBInterface.checkDocument(currentUri, settings) val diagnostics: List<Diagnostic> = proBInterface.checkDocument(currentUri, settings)
communicator.sendDebugMessage("created diagnostics $diagnostics", MessageType.Info) communicator.sendDebugMessage("creating diagnostics $diagnostics", MessageType.Info)
communicator.publishDiagnostics(PublishDiagnosticsParams(currentUri, diagnostics)) communicator.publishDiagnostics(PublishDiagnosticsParams(currentUri, diagnostics))
val filesWithProblems = diagnostics.map { diagnostic -> diagnostic.source } val filesWithProblems = diagnostics.map { diagnostic -> diagnostic.source }
val invalidFiles = calculateToInvalidate(currentUri, filesWithProblems) val invalidFiles = calculateToInvalidate(currentUri, filesWithProblems)
......
...@@ -28,7 +28,7 @@ class Server : LanguageServer{ ...@@ -28,7 +28,7 @@ class Server : LanguageServer{
res.capabilities.textDocumentSync = Either.forLeft(TextDocumentSyncKind.Full) res.capabilities.textDocumentSync = Either.forLeft(TextDocumentSyncKind.Full)
res.capabilities.workspace = WorkspaceServerCapabilities(WorkspaceFoldersOptions()) res.capabilities.workspace = WorkspaceServerCapabilities(WorkspaceFoldersOptions())
res.capabilities.workspace.workspaceFolders.supported = true res.capabilities.workspace.workspaceFolders.supported = true
res.capabilities.completionProvider = CompletionOptions()
return CompletableFuture.supplyAsync { res } return CompletableFuture.supplyAsync { res }
} }
......
...@@ -4,7 +4,6 @@ package b.language.server.proBMangement.prob ...@@ -4,7 +4,6 @@ package b.language.server.proBMangement.prob
import b.language.server.communication.Communicator import b.language.server.communication.Communicator
import b.language.server.communication.CommunicatorInterface import b.language.server.communication.CommunicatorInterface
import b.language.server.dataStorage.ProBSettings import b.language.server.dataStorage.ProBSettings
import com.google.gson.Gson
import com.google.inject.Inject import com.google.inject.Inject
import com.google.inject.Injector import com.google.inject.Injector
import de.prob.animator.ReusableAnimator import de.prob.animator.ReusableAnimator
...@@ -19,10 +18,7 @@ import de.prob.statespace.StateSpace ...@@ -19,10 +18,7 @@ import de.prob.statespace.StateSpace
import de.prob.statespace.Trace import de.prob.statespace.Trace
import org.eclipse.lsp4j.Diagnostic import org.eclipse.lsp4j.Diagnostic
import org.eclipse.lsp4j.MessageType import org.eclipse.lsp4j.MessageType
import org.ietf.jgss.GSSContext
import java.io.File
import java.io.IOException import java.io.IOException
import java.nio.charset.Charset
/** /**
* Represents the interface to communicate with prob kernel * Represents the interface to communicate with prob kernel
...@@ -43,13 +39,13 @@ class ProBKernel @Inject constructor(private val injector : Injector, ...@@ -43,13 +39,13 @@ class ProBKernel @Inject constructor(private val injector : Injector,
* @return a list with the problems found * @return a list with the problems found
*/ */
fun check(path : String, settings : ProBSettings) : List<Diagnostic>{ fun check(path : String, settings : ProBSettings) : List<Diagnostic>{
Communicator.sendDebugMessage("Unload old machine", MessageType.Info) Communicator.sendDebugMessage("unloading old machine", MessageType.Info)
unloadMachine() unloadMachine()
val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(path.substringAfterLast("."))) val factory = injector.getInstance(FactoryProvider.factoryClassFromExtension(path.substringAfterLast(".")))
val warningListener = WarningListener() val informationListener = InformationListener()
animator.addWarningListener(warningListener) animator.addWarningListener(informationListener)
val parseErrors = mutableListOf<Diagnostic>() val parseErrors = mutableListOf<Diagnostic>()
Communicator.sendDebugMessage("loading new machine", MessageType.Info) Communicator.sendDebugMessage("loading new machine", MessageType.Info)
...@@ -70,7 +66,7 @@ class ProBKernel @Inject constructor(private val injector : Injector, ...@@ -70,7 +66,7 @@ class ProBKernel @Inject constructor(private val injector : Injector,
communicator.sendDebugMessage("returning from kernel", MessageType.Info) communicator.sendDebugMessage("returning from kernel", MessageType.Info)
return listOf(warningListener.getWarnings(), parseErrors, strictProblems).flatten() return listOf(informationListener.getInformation(), parseErrors, strictProblems).flatten()
} }
/** /**
...@@ -92,7 +88,7 @@ class ProBKernel @Inject constructor(private val injector : Injector, ...@@ -92,7 +88,7 @@ class ProBKernel @Inject constructor(private val injector : Injector,
resultLint.addAll(newStateSpace.performExtendedStaticChecks()) resultLint.addAll(newStateSpace.performExtendedStaticChecks())
} }
communicator.sendDebugMessage("returning...", MessageType.Info) communicator.sendDebugMessage("finished evaluation", MessageType.Info)
} catch (e: RuntimeException) { } catch (e: RuntimeException) {
newStateSpace.kill() newStateSpace.kill()
...@@ -110,7 +106,7 @@ class ProBKernel @Inject constructor(private val injector : Injector, ...@@ -110,7 +106,7 @@ class ProBKernel @Inject constructor(private val injector : Injector,
*/ */
private fun executeAdditionalOptions(settings : ProBSettings){ private fun executeAdditionalOptions(settings : ProBSettings){
if(settings.wdChecks){ if(settings.wdChecks){
communicator.sendDebugMessage("Doing WD checks", MessageType.Info) communicator.sendDebugMessage("doing WD checks", MessageType.Info)
animator.execute(CheckWellDefinednessCommand()) animator.execute(CheckWellDefinednessCommand())
} }
} }
......
...@@ -88,7 +88,8 @@ class ProBKernelManager(private val communicator : CommunicatorInterface) : ProB ...@@ -88,7 +88,8 @@ class ProBKernelManager(private val communicator : CommunicatorInterface) : ProB
System.getProperty("prob.home"), MessageType.Info) System.getProperty("prob.home"), MessageType.Info)
val result = checkProBVersionSetting(settings.probHome) val result = checkProBVersionSetting(settings.probHome)
if(!result){ if(!result){
throw CouldNotFindProBHomeException("searched at ${settings.probHome} for prob but found nothing") throw CouldNotFindProBHomeException("searched at ${settings.probHome} for prob but found nothing - make sure " +
"you point to the prob directory not to probcli.sh/probcli")
} }
communicator.sendDebugMessage("success!", MessageType.Info) communicator.sendDebugMessage("success!", MessageType.Info)
......
...@@ -30,6 +30,9 @@ fun getErrorItemType(errorItem: ErrorItem.Type) : DiagnosticSeverity{ ...@@ -30,6 +30,9 @@ fun getErrorItemType(errorItem: ErrorItem.Type) : DiagnosticSeverity{
ErrorItem.Type.INTERNAL_ERROR -> { ErrorItem.Type.INTERNAL_ERROR -> {
DiagnosticSeverity.Error DiagnosticSeverity.Error
} }
ErrorItem.Type.MESSAGE -> {
DiagnosticSeverity.Information
}
else -> { else -> {
DiagnosticSeverity.Error DiagnosticSeverity.Error
} }
......
package b.language.server.proBMangement.prob package b.language.server.proBMangement.prob
import de.prob.animator.IWarningListener import de.prob.animator.IInformationListener
import de.prob.animator.domainobjects.ErrorItem import de.prob.animator.domainobjects.ErrorItem
import org.eclipse.lsp4j.Diagnostic import org.eclipse.lsp4j.Diagnostic
import org.eclipse.lsp4j.DiagnosticSeverity import org.eclipse.lsp4j.DiagnosticSeverity
...@@ -8,13 +8,13 @@ import org.eclipse.lsp4j.DiagnosticSeverity ...@@ -8,13 +8,13 @@ import org.eclipse.lsp4j.DiagnosticSeverity
/** /**
* Custom collector to collect warnings from prob kernel * Custom collector to collect warnings from prob kernel
*/ */
class WarningListener : IWarningListener { class InformationListener : IInformationListener {
private val warningList : ArrayList<ErrorItem> = arrayListOf() private val warningList : ArrayList<ErrorItem> = arrayListOf()
override fun warningsOccurred(warnings: MutableList<ErrorItem>?) { override fun warningsOccurred(warnings: MutableList<ErrorItem>?) {
warningList.addAll(warnings!!.toList()) warningList.addAll(warnings!!.toList())
} }
fun getWarnings() : List<Diagnostic>{ fun getInformation() : List<Diagnostic>{
return convertErrorItems(warningList) return convertErrorItems(warningList)
} }
} }
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment