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

cleanup and todos

parent 908deba8
No related branches found
No related tags found
No related merge requests found
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())
......
......@@ -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{
......
......@@ -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()
......
......@@ -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))
}
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",
......
......@@ -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
*/
......
......@@ -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,14 +48,22 @@ 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 {
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))
}
......
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)
......
......@@ -5,6 +5,11 @@ 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>{
return errorItems.toList().map { errorItem ->
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment