diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml
index 689b48d7b9..4ed654d280 100644
--- a/.github/workflows/nightlydeploy.yml
+++ b/.github/workflows/nightlydeploy.yml
@@ -36,13 +36,15 @@ jobs:
uses: gradle/actions/setup-gradle@v6
- name: Generated Stubs, Documentation and Assemble
- run: ./gradlew --parallel :keyext.api.doc:run :dokkaGeneratePublicationHtml assemble
+ run: ./gradlew --parallel :keyext.api.doc:run
+ - run: ./gradlew --parallel :dokkaGeneratePublicationHtml assemble
+
+ - run: mv -v build/dokka/html/ out/dokka
- - run: mv out/* build/dokka/html/
- name: "Upload GitHub Pages artifact"
uses: actions/upload-pages-artifact@v5
with:
- path: build/dokka/html
+ path: out/
- name: Deploy to GitHub Pages
id: deployment
uses: actions/deploy-pages@v5
diff --git a/keyext.api.doc/src/main/resources/default.css b/doc/default.css
similarity index 89%
rename from keyext.api.doc/src/main/resources/default.css
rename to doc/default.css
index fa818b69cc..4140872abb 100644
--- a/keyext.api.doc/src/main/resources/default.css
+++ b/doc/default.css
@@ -57,10 +57,16 @@ body {
}
ul {
+ padding-left: 2ex;
+ }
+ ul.segments > li abbr {
+ font-size: 120%;
+ font-weight: bold;
}
li {
+ list-style: disc;
}
}
diff --git a/doc/index.md b/doc/index.md
new file mode 100644
index 0000000000..1491ff9298
--- /dev/null
+++ b/doc/index.md
@@ -0,0 +1,39 @@
+---
+title: "Index"
+---
+
+# key-rpc
+The JSON-RPC interface for the KeY theorem prover
+
+# Module sample
+Sample examples for Dokka Mermaid plugin.
+
+```mermaid
+pie title NETFLIX
+ "Time spent looking for movie" : 90
+ "Time spent watching it" : 10
+```
+
+# Package com.glureau.dokkamermaid.sample
+
+Package documentation can have its own mermaid diagrams.
+
+```mermaid
+mindmap
+ root((mindmap))
+ Origins
+ Long history
+ ::icon(fa fa-book)
+ Popularisation
+ British popular psychology author Tony Buzan
+ Research
+ On effectiveness
and features
+ On Automatic creation
+ Uses
+ Creative techniques
+ Strategic planning
+ Argument mapping
+ Tools
+ Pen and paper
+ Mermaid
+```
\ No newline at end of file
diff --git a/gradle/index.md b/gradle/index.md
index 285f0fb087..678d4382a0 100644
--- a/gradle/index.md
+++ b/gradle/index.md
@@ -1,35 +1,3 @@
# key-rpc
The JSON-RPC interface for the KeY theorem prover
-# Module sample
-Sample examples for Dokka Mermaid plugin.
-
-```mermaid
-pie title NETFLIX
- "Time spent looking for movie" : 90
- "Time spent watching it" : 10
-```
-
-# Package com.glureau.dokkamermaid.sample
-
-Package documentation can have its own mermaid diagrams.
-
-```mermaid
-mindmap
- root((mindmap))
- Origins
- Long history
- ::icon(fa fa-book)
- Popularisation
- British popular psychology author Tony Buzan
- Research
- On effectiveness
and features
- On Automatic creation
- Uses
- Creative techniques
- Strategic planning
- Argument mapping
- Tools
- Pen and paper
- Mermaid
-```
\ No newline at end of file
diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml
index a90b91ce49..c3b1e6e922 100644
--- a/gradle/libs.versions.toml
+++ b/gradle/libs.versions.toml
@@ -11,6 +11,7 @@ therapi = "0.15.0"
kotlin-gradle-plugin = "2.4.0"
dokka = "2.2.0"
spotless = "8.7.0"
+kotlinx-coroutines = "1.10.1"
[libraries]
kotlin-gradle-plugin = { module = "org.jetbrains.kotlin:kotlin-gradle-plugin", version.ref = "kotlin-gradle-plugin" }
@@ -28,3 +29,5 @@ guava = { module = "com.google.guava:guava", version.ref = "guava" }
therapi-runtime-javadoc-scribe = { module = "com.github.therapi:therapi-runtime-javadoc-scribe", version.ref = "therapi" }
therapi-runtime-javadoc = { module = "com.github.therapi:therapi-runtime-javadoc", version.ref = "therapi" }
clickt = { module = "com.github.ajalt.clikt:clikt", version = "5.1.0" }
+kotlinx-coroutines-core = { module = "org.jetbrains.kotlinx:kotlinx-coroutines-core", version.ref = "kotlinx-coroutines" }
+kotlinx-coroutines-js = { module = "org.jetbrains.kotlinx:kotlinx-coroutines-core-js", version.ref = "kotlinx-coroutines" }
diff --git a/keyext.api.doc/src/main/kotlin/org/key_project/key/api/doc/DocGen.kt b/keyext.api.doc/src/main/kotlin/org/key_project/key/api/doc/DocGen.kt
deleted file mode 100644
index 8e20821c44..0000000000
--- a/keyext.api.doc/src/main/kotlin/org/key_project/key/api/doc/DocGen.kt
+++ /dev/null
@@ -1,46 +0,0 @@
-package org.key_project.key.api.doc
-
-import java.util.function.Supplier
-
-/**
- * Generation of Markdown documentation.
- * # Module sample
- * Sample examples for Dokka Mermaid plugin.
- *
- * ```mermaid
- * pie title NETFLIX
- * "Time spent looking for movie" : 90
- * "Time spent watching it" : 10
- * ```
- *
- * # Package com.glureau.dokkamermaid.sample
- *
- * Package documentation can have its own mermaid diagrams.
- *
- * ```mermaid
- * mindmap
- * root((mindmap))
- * Origins
- * Long history
- * ::icon(fa fa-book)
- * Popularisation
- * British popular psychology author Tony Buzan
- * Research
- * On effectiveness
and features
- * On Automatic creation
- * Uses
- * Creative techniques
- * Strategic planning
- * Argument mapping
- * Tools
- * Pen and paper
- * Mermaid
- * ```
- *
- *
- * @author Alexander Weigl
- * @version 1 (29.10.23)
- */
-class DocGen(private val metamodel: Metamodel.KeyApi) : Supplier {
- override fun get() = HtmlDocs(metamodel).render()
-}
diff --git a/keyext.api.doc/src/main/kotlin/org/key_project/key/api/doc/HtmlDocs.kt b/keyext.api.doc/src/main/kotlin/org/key_project/key/api/doc/HtmlDocs.kt
deleted file mode 100644
index 2ace19b352..0000000000
--- a/keyext.api.doc/src/main/kotlin/org/key_project/key/api/doc/HtmlDocs.kt
+++ /dev/null
@@ -1,314 +0,0 @@
-package org.key_project.key.api.doc
-
-import de.uka.ilkd.key.util.KeYConstants
-import de.uka.ilkd.key.util.KeYResourceManager
-import kotlinx.html.*
-import kotlinx.html.stream.appendHTML
-import org.key_project.key.api.doc.Metamodel.EnumType
-import org.key_project.key.api.doc.Metamodel.ObjectType
-
-class HtmlDocs(
- metamodel: Metamodel.KeyApi,
-) {
- val segmentDocumentation: Map = metamodel.segmentDocumentation
- val types: List =
- metamodel.types.values
- .sortedBy { it.name }
- .toList()
- val endpoints: List = metamodel.endpoints.sortedBy { it.name }.toList()
- val endpointsBySegment: Map> =
- metamodel.endpoints
- .sortedBy { it.name }
- .groupBy { it.segment() }
- .toSortedMap()
-
- val date: String = java.util.Date().toString()
- private val version: String =
- KeYResourceManager.getManager().getVersion() +
- " (" + KeYConstants.INTERNAL_VERSION.substring(0, 8) + ")"
-
- fun render() =
- buildString(8096) {
- appendHTML(true).html {
- head {
- meta(charset = "utf-8")
- title { +"KeY API Documentation" }
- }
- body {
- style {
- +(javaClass.getResourceAsStream("/default.css")?.bufferedReader()?.readText() ?: "")
- }
- div {
- id = "main"
- nav {
- id = "nav"
- h1 { +"Documentation: KeY JSON-RPC API" }
- div {
- +"""Version: $version
- Date: $date}"""
- }
- h2 { +"Types" }
- ul {
- types.forEach { type ->
- li {
- a(href = "#${type.name}") { +type.name }
- }
- }
- }
-
- h2 { +"Procedures" }
- ul {
- endpointsBySegment.forEach { segname, seq ->
- li {
- abbr {
- title = segmentDocumentation[segname]?.text ?: "n/a"
- +segname
- }
- ul {
- seq.forEach { ep ->
- li {
- a(href = "#${ep.name}") { +ep.name }
- }
- }
- }
- }
- }
- }
- }
- }
-
- div {
- id = "content"
- // ── Base Definitions ─────────────────────────────────────────────────────
- h2 { +"Base Definitions" }
- p {
- +"This API builds upon and uses the same convention as the "
- a(href = "https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/") {
- +"Language Server Protocol"
- }
- +". In basic, the protocol builds upon a simple HTTP protocol with a JSON payload. A request message looks as"
- }
- div("highlight") {
- pre {
- +"""Content-Length: 80\r\n
-Content-Type: application/vscode-jsonrpc; charset=utf-8\r\n
-\r\n
-{
- "jsonrpc": "2.0",
- "id": 1,
- "method": "env/version",
- "params": {
- ...
- }
-}"""
- }
- }
- p {
- +"Header "
- code { +"Content-Type" }
- +" is optional. The "
- code { +"""\\r\\n""" }
- +" are mandatory. The field "
- code { +"id" }
- +" make the difference between a request or a notification. "
- +"Later do not result into a response. A response message contains the fields "
- code { +"result" }
- +" or "
- code { +"error" }
- +", depending on a normal or exceptional execution of the request."
- }
- p {
- +"The communication is always asynchronous and duplex. "
- +"Meaning you can send and receive messages at any time. "
- +"For synchronous calls, the client and server library need to implement a waiting mechanism."
- }
-
- // ── Types ────────────────────────────────────────────────────────────────
- h2 { +"Types" }
- div("data-type") {
- for (type in types) {
- val isEnum = type is EnumType
- val kind = if (isEnum) "enum" else "type"
-
- div {
- id = type.name
- classes = setOf("data-type", kind)
-
- h3 {
- +type.name
- +" "
- span("kind") { +" $kind" }
- }
-
- div("highlight") {
- span("k") { +kind }
- +" "
- span("kc") {
- a(href = "#${type.name}") { +type.name }
- }
- +" { "
- br()
-
- // Struct fields
- if (type is ObjectType) {
- type.fields.forEach { field ->
- div("entry field") {
- field.documentation?.let { doc ->
- div("cm") { +"/* ${doc.text} */" }
- }
- div {
- span("kc") {
- a(href = "#${type.name}") { +type.name }
- }
- +" "
- span("nv") { +field.name }
- +";"
- }
- }
- }
- }
- // Enum values
- if (type is EnumType) {
- type.values.sortedBy { it.value }?.forEach { value ->
- value.documentation?.let { doc ->
- +"/* ${doc.text} */"
- }
- +value.value
- }
- }
-
- +"}"
- }
-
- type.documentation?.let { doc ->
- div("documentation") {
- p { +doc.text }
- if (doc.others.isNotEmpty()) {
- ul {
- doc.others.forEach { entry ->
- li {
- strong { +"${entry.name}:" }
- +" ${entry.value}"
- }
- }
- }
- }
- }
-
- if (type is ObjectType) {
- type.jsonExample()?.let { example ->
- div {
- details {
- summary { +"Example" }
- code("highlight") {
- style = "white-space: pre"
- +example
- }
- }
- }
- }
- }
- }
- }
- }
- }
-
- // ── Endpoints ────────────────────────────────────────────────────────────
- h2 {
- id = "endpoints"
- +"Endpoints"
- }
-
- div("endpoints") {
- val grouped = endpoints.groupBy { it.segment() }
-
- for ((segment, endpoints) in grouped) {
- h3 {
- id = segment
- +"Segment: $segment"
- }
-
- segmentDocumentation[segment]?.let { doc ->
- div("documentation") {
- p { +doc.text }
- if (doc.others.isNotEmpty()) {
- ul {
- doc.others.forEach { entry ->
- li {
- strong { +"${entry.name}:" }
- +" ${entry.value}"
- }
- }
- }
- }
- }
- }
-
- endpoints.sortedBy { it.name }.forEach { ep ->
-
- val kindClass = if (ep.isAsync) "async" else "sync"
- val direction =
- when {
- ep.sender == "Server" && ep.isAsync -> "server ~~> client"
- ep.sender == "Server" && !ep.isAsync -> "server --> client"
- ep.sender == "Client" && !ep.isAsync -> "client --> server"
- else -> "client ~~> server"
- }
-
- div {
- id = ep.name
- classes = setOf("endpoint", kindClass, ep.sender)
-
- h4 {
- if (ep.isAsync) {
- span("async") { +"Notification:" }
- } else {
- span("sync") { +"Request:" }
- }
- +" ${ep.name} "
- span("direction") { +direction }
- }
-
- code("highlight") {
- +ep.name
- span("p") { +"(" }
- ep.args.forEachIndexed { index, arg ->
- span("kc") { a(href = "#${arg.type}") { +arg.type } }
- +" "
- span("nv") { +arg.name }
- if (index < ep.args.lastIndex) span("p") { +"," }
- }
- span("p") { +")" }
- if (ep is Metamodel.Request) {
- ep.returnType.let { ret ->
- span("p") { +":" }
- +" "
- span("kc") { a(href = "#${ret.name}") { +ret.name } }
- }
- }
- }
-
- ep.documentation?.let { doc ->
- div("documentation") {
- p { +doc.text }
- if (doc.others.isNotEmpty()) {
- ul {
- doc.others.forEach { entry ->
- li {
- strong { +"${entry.name}:" }
- +" ${entry.value}"
- }
- }
- }
- }
- }
- }
- }
- }
- }
- }
- }
- }
- }
- }
-}
diff --git a/keyext.api.doc/src/main/kotlin/org/key_project/key/api/doc/KotlinJsGenerator.kt b/keyext.api.doc/src/main/kotlin/org/key_project/key/api/doc/KotlinJsGenerator.kt
new file mode 100644
index 0000000000..58c8b3fe92
--- /dev/null
+++ b/keyext.api.doc/src/main/kotlin/org/key_project/key/api/doc/KotlinJsGenerator.kt
@@ -0,0 +1,225 @@
+package org.key_project.key.api.doc
+
+import java.util.function.Supplier
+
+/**
+ * Generator for Kotlin/JS programs based on a given meta model.
+ * Avoids JVM constructs as far as possible.
+ *
+ * @author Alexander Weigl
+ * @version 1 (2026)
+ */
+abstract class KotlinJsGenerator(protected val metamodel: Metamodel.KeyApi) : Supplier {
+ val BASE_PACKAGE = "org.key_project.key.api.client"
+ val PACKAGE = "$BASE_PACKAGE.stubs"
+
+ protected fun adKotlin(typeName: String): String = when (typeName) {
+ Metamodel.INT.name, "INT" -> "Int"
+ Metamodel.LONG.name, "LONG" -> "Long"
+ Metamodel.STRING.name, "STRING" -> "String"
+ Metamodel.BOOL.name, "BOOL" -> "Boolean"
+ Metamodel.DOUBLE.name, "DOUBLE" -> "Double"
+ else -> {
+ val t = findType(typeName)
+ adKotlin(t)
+ }
+ }
+
+ fun listType(t: String) = "List<$t>"
+ fun eitherType(a: String, b: String) = "Either<$a,$b>"
+
+ fun adKotlin(t: Metamodel.Type): String = when (t) {
+ is Metamodel.ListType -> listType(adKotlin(t.componentType))
+ is Metamodel.EitherType -> eitherType(adKotlin(t.a), adKotlin(t.b))
+ Metamodel.INT -> "Int"
+ Metamodel.LONG -> "Long"
+ Metamodel.STRING -> "String"
+ Metamodel.BOOL -> "Boolean"
+ Metamodel.DOUBLE -> "Double"
+ is Metamodel.EnumType,
+ is Metamodel.ObjectType -> t.name
+ }
+
+ fun findType(typeName: String?): Metamodel.Type = this.metamodel.types.values
+ .firstOrNull {
+ if (it is Metamodel.ListType) {
+ it.componentType.name == typeName
+ } else {
+ it.name == typeName
+ }
+ } ?: Metamodel.ObjectType("Any", "Any", listOf(), null)
+
+ protected fun escapeKdoc(text: String): String {
+ return text.replace("*/", "* /").replace("/*", "/ *").replace("\n", "\n * ")
+ }
+
+ /**
+ * Generates Kotlin/JS API server stubs for remote calls.
+ */
+ class KotlinJsApiGenServer(metamodel: Metamodel.KeyApi) : KotlinJsGenerator(metamodel) {
+ override fun get(): String {
+ val sorted = metamodel.endpoints.asSequence()
+ .filter { it is Metamodel.ServerRequest || it is Metamodel.ServerNotification }
+ .sortedBy { it.name }
+ .groupBy { it.segment() }
+ .toSortedMap()
+
+ val sb = StringBuilder()
+ sb.appendLine("package $PACKAGE")
+ sb.appendLine()
+ sb.appendLine("import $BASE_PACKAGE.*")
+ sb.appendLine()
+ sb.appendLine("/** Remote API client for KeY server communication. */")
+ sb.appendLine("class KeyRemote(private val rpcLayer: RPCLayer) {")
+ sb.appendLine()
+
+ sorted.forEach { (name, endpoints) ->
+ val cname = "Segment${name.replaceFirstChar { it.uppercase() }}"
+ sb.appendLine(" val $name: $cname = $cname()")
+ sb.appendLine()
+ }
+
+ sorted.forEach { (name, endpoints) ->
+ val cname = "Segment${name.replaceFirstChar { it.uppercase() }}"
+ sb.appendLine(" inner class $cname {")
+
+ metamodel.segmentDocumentation[name]?.let { doc ->
+ sb.appendLine(" /** ${escapeKdoc(doc.text)} */")
+ }
+
+ endpoints.forEach { endpoint ->
+ sb.append(generateServerMethod(endpoint))
+ }
+ sb.appendLine(" }")
+ sb.appendLine()
+ }
+
+ sb.appendLine("}")
+ return sb.toString()
+ }
+
+ private fun generateServerMethod(endpoint: Metamodel.Endpoint): String {
+ val sb = StringBuilder()
+
+ endpoint.documentation?.let { doc ->
+ sb.appendLine(" /** ${escapeKdoc(doc.text)} */")
+ }
+
+ val methodName = endpoint.name.substringAfterLast("/")
+ val params = endpoint.args.joinToString(", ") { "${it.name}: ${adKotlin(it.type)}" }
+ val returnType = if (endpoint is Metamodel.ServerRequest) {
+ adKotlin(endpoint.returnType)
+ } else {
+ "Unit"
+ }
+
+ sb.appendLine(" suspend fun $methodName($params): $returnType {")
+ val args = endpoint.args.joinToString(", ") { it.name }
+ if (endpoint is Metamodel.ServerRequest) {
+ sb.appendLine(" return rpcLayer.callSync(\"${endpoint.name}\", $args)")
+ } else {
+ sb.appendLine(" rpcLayer.callAsync(\"${endpoint.name}\", $args)")
+ }
+ sb.appendLine(" }")
+ return sb.toString()
+ }
+ }
+
+ /**
+ * Generates Kotlin/JS client interface for local implementation.
+ */
+ class KotlinJsApiGenClient(metamodel: Metamodel.KeyApi) : KotlinJsGenerator(metamodel) {
+ override fun get(): String = buildString {
+ appendLine("package $PACKAGE")
+ appendLine()
+ appendLine("import $BASE_PACKAGE.*")
+ appendLine("import kotlinx.coroutines.*")
+ appendLine()
+ appendLine("/** Client interface for implementing local KeY functionality. */")
+ appendLine("interface KeyClient {")
+
+ metamodel.endpoints.asSequence()
+ .filter { it is Metamodel.ClientRequest || it is Metamodel.ClientNotification }
+ .sortedBy { it.name }
+ .forEach { endpoint ->
+ append(generateClientMethod(endpoint))
+ }
+
+ appendLine("}")
+ appendLine()
+ }
+
+ private fun generateClientMethod(endpoint: Metamodel.Endpoint): String = buildString {
+ endpoint.documentation?.let { doc ->
+ appendLine(" /** ${escapeKdoc(doc.text)} */")
+ }
+
+ val methodName = endpoint.name.substringAfterLast("/")
+ val params = endpoint.args.joinToString(", ") { "${it.name}: ${adKotlin(it.type)}" }
+
+ if (endpoint is Metamodel.ClientRequest) {
+ appendLine(" suspend fun $methodName($params): ${adKotlin(endpoint.returnType)}")
+ } else {
+ appendLine(" suspend fun $methodName($params)")
+ }
+ appendLine()
+ }
+ }
+
+ /**
+ * Generates Kotlin/JS data classes from the metamodel.
+ * Uses kotlinx.serialization for JSON support.
+ */
+ class KotlinJsDataGen(metamodel: Metamodel.KeyApi) : KotlinJsGenerator(metamodel) {
+ override fun get(): String = buildString {
+ appendLine("package $PACKAGE")
+ appendLine()
+ appendLine("import $BASE_PACKAGE.*")
+ appendLine("import kotlinx.serialization.*")
+
+ metamodel.types.values.forEach { type ->
+ append(printType(type))
+ }
+
+ appendLine(" val TYPE_REGISTRY: Map = mapOf(")
+ val typeEntries = metamodel.types.values.map {
+ " \"${it.identifier?.replace("$", "\\\$")}\" to \"${it.name}\""
+ }.joinToString(",\n")
+ appendLine(typeEntries)
+ appendLine(" )")
+ appendLine()
+ }
+
+ private fun printType(type: Metamodel.Type): String = buildString {
+ when (type) {
+ is Metamodel.ObjectType -> {
+ appendLine(" @Serializable")
+ appendLine(" data class ${type.name}(")
+
+ val fields = type.fields.map { field ->
+ val fieldType = adKotlin(field.type)
+ " val ${field.name}: $fieldType"
+ }.joinToString(",\n")
+
+ appendLine(fields)
+ appendLine(" )")
+ appendLine()
+ }
+
+ is Metamodel.EnumType -> {
+ appendLine(" @Serializable")
+ appendLine(" enum class ${type.name} {")
+
+ val values = type.values.joinToString(",\n") { constant ->
+ " ${constant.value}"
+ }
+ appendLine(values)
+ appendLine(" }")
+ appendLine()
+ }
+
+ else -> {}
+ }
+ }
+ }
+}
diff --git a/keyext.api.doc/src/main/kotlin/org/key_project/key/api/doc/Main.kt b/keyext.api.doc/src/main/kotlin/org/key_project/key/api/doc/Main.kt
index de265be5f6..8bc63d507c 100644
--- a/keyext.api.doc/src/main/kotlin/org/key_project/key/api/doc/Main.kt
+++ b/keyext.api.doc/src/main/kotlin/org/key_project/key/api/doc/Main.kt
@@ -5,15 +5,13 @@ import com.github.ajalt.clikt.core.main
import com.github.ajalt.clikt.parameters.options.default
import com.github.ajalt.clikt.parameters.options.option
import com.github.ajalt.clikt.parameters.types.path
-import com.github.javaparser.utils.SourceRoot
import kotlinx.serialization.json.Json
import org.key_project.key.api.doc.Metamodel.KeyApi
import java.io.IOException
import java.nio.file.Files
import java.nio.file.Path
import java.nio.file.Paths
-import kotlin.io.path.createDirectories
-import kotlin.io.path.writeText
+import kotlin.io.path.*
/**
* @author Alexander Weigl
@@ -36,6 +34,9 @@ class Main : CliktCommand(name = "gendoc") {
private val outputWeb: Path by option("--output-web", help = "Output folder")
.path().default(Paths.get("../out"))
+ private val outputKotlinJs: Path by option("--output-kotlin-js", help = "Output folder for Kotlin/JS")
+ .path().default(Paths.get("../keyext.api.ktclient/src/commonMain/kotlin/org/key_project/key/api/client/stubs/"))
+
override fun run() {
val metadata = ExtractMetaData()
metadata.run()
@@ -49,7 +50,9 @@ class Main : CliktCommand(name = "gendoc") {
prettyPrint = true
}.encodeToString(it)
}
- runGenerator(metadata.api, "api.meta.html", outputWeb) { DocGen(it).get() }
+
+ generatePages(metadata.api, outputWeb)
+
runGenerator(metadata.api, "keydata.py", outputPython) { PythonGenerator.PyDataGen(it).get() }
runGenerator(metadata.api, "server.py", outputPython) { PythonGenerator.PyApiGen(it).get() }
@@ -59,7 +62,7 @@ class Main : CliktCommand(name = "gendoc") {
JavaGenerator.JavaApiGenClient(metadata.api),
JavaGenerator.JavaDataGen(metadata.api)
)
- cus.asSequence().map{it.get()}.forEach {
+ cus.asSequence().map { it.get() }.forEach {
val resolve = outputJava.resolve(it.packageDeclaration()?.nameAsString?.replace('.', '/') ?: "")
resolve.createDirectories()
it.setStorage(resolve.resolve(it.types.first().nameAsString + ".java"))
@@ -67,6 +70,48 @@ class Main : CliktCommand(name = "gendoc") {
it.toString()
)
}
+
+ // Kotlin/JS
+ Files.createDirectories(outputKotlinJs)
+ val kotlinJsGenerators = listOf(
+ KotlinJsGenerator.KotlinJsApiGenServer(metadata.api) to "KeyRemote.kt",
+ KotlinJsGenerator.KotlinJsApiGenClient(metadata.api) to "KeyClient.kt",
+ KotlinJsGenerator.KotlinJsDataGen(metadata.api) to "ApiModel.kt"
+ )
+ kotlinJsGenerators.forEach { (gen, fileName) ->
+ val content = gen.get()
+ Files.writeString(outputKotlinJs.resolve(fileName), content)
+ }
+ }
+
+ /// Poor man's static site generator
+ private fun generatePages(metadata: KeyApi, outputWeb: Path) {
+ val base = Paths.get("../doc")
+ val resources = base.walk().toList()
+
+ // copy non-markdown files
+ resources.filter { it.nameWithoutExtension != "md" }
+ .forEach { copyResources(it, base, outputWeb) }
+
+ val dokkaLink = Link("/dokka/index.html", "API", 11000)
+ val keyLink = Link("https://keyproject.github.io/key-docs/", "KeY Documentation", 10000)
+ val bookLink = Link("https://key-project.org/thebook2", "KeY Book", 10001)
+
+ // generate html pages
+ val pages = (listOf(ReferencePageResource(), dokkaLink, keyLink, bookLink) +
+ resources.filter { it.extension == "md" }.map { MdPageResource(it) })
+ .sortedBy { it.order }
+
+ pages.forEach {
+ val target = outputWeb / it.relativeHtmlPath
+ it.write(target, metadata, pages)
+ }
+ }
+
+ private fun copyResources(source: Path, base: Path, targetFolder: Path) {
+ val target = targetFolder / (source.relativeTo(base))
+ target.deleteIfExists()
+ source.copyTo(target)
}
private fun runGenerator(keyApi: KeyApi, target: String, folder: Path, api: (KeyApi) -> String) {
diff --git a/keyext.api.doc/src/main/kotlin/org/key_project/key/api/doc/ReferencePage.kt b/keyext.api.doc/src/main/kotlin/org/key_project/key/api/doc/ReferencePage.kt
new file mode 100644
index 0000000000..46895c0b78
--- /dev/null
+++ b/keyext.api.doc/src/main/kotlin/org/key_project/key/api/doc/ReferencePage.kt
@@ -0,0 +1,447 @@
+package org.key_project.key.api.doc
+
+import de.uka.ilkd.key.util.KeYConstants
+import de.uka.ilkd.key.util.KeYResourceManager
+import kotlinx.html.*
+import kotlinx.html.stream.appendHTML
+import org.intellij.markdown.flavours.space.SFMFlavourDescriptor
+import org.intellij.markdown.html.HtmlGenerator
+import org.intellij.markdown.parser.MarkdownParser
+import org.key_project.key.api.doc.Metamodel.EnumType
+import org.key_project.key.api.doc.Metamodel.ObjectType
+import java.nio.file.Path
+import kotlin.io.path.nameWithoutExtension
+import kotlin.io.path.readText
+import kotlin.io.path.writeText
+
+internal val RE_METADATA = "^--- *$(.*?)^--- *$".toRegex(setOf(RegexOption.MULTILINE, RegexOption.DOT_MATCHES_ALL))
+
+interface PageResource {
+ fun write(target: Path, metamodel: Metamodel.KeyApi, pages: List)
+ val relativeHtmlPath: String
+ val title: String
+ val order: Int
+}
+
+data class Link(
+ override val relativeHtmlPath: String,
+ override val title: String,
+ override val order: Int
+) : PageResource {
+ override fun write(
+ target: Path,
+ metamodel: Metamodel.KeyApi,
+ pages: List
+ ) {
+ // Nothing to be done
+ }
+}
+
+private const val REFERENCE_HTML = "reference.html"
+
+class ReferencePageResource() : PageResource {
+ override fun write(target: Path, metamodel: Metamodel.KeyApi, pages: List) =
+ target.writeText(ReferencePage(metamodel, pages).render())
+
+ override val relativeHtmlPath = REFERENCE_HTML
+ override val title = "API Reference"
+ override val order: Int
+ get() = 99999
+}
+
+data class MdPageResource(val path: Path) : PageResource {
+ private val content by lazy { path.readText() }
+
+ val metadata by lazy {
+ meta.trim(' ', '-', '\n').splitToSequence('\n')
+ .map {
+ val (a, b) = it.split(':', limit = 2)
+ a.trim() to b.trim('"', ' ')
+ }.associate { it }
+ }
+
+ val meta by lazy {
+ RE_METADATA.find(content)?.run {
+ groupValues[1]
+ } ?: ""
+ }
+
+ val text by lazy {
+ RE_METADATA.find(content)?.run {
+ content.substring(range.last + 1)
+ } ?: content
+ }
+
+ val nameWithoutExtension = path.nameWithoutExtension
+ override val relativeHtmlPath = nameWithoutExtension + ".html"
+ override val title: String
+ get() = metadata["title"] ?: nameWithoutExtension
+ override val order: Int
+ get() = metadata["menuOrder"]?.toInt() ?: 0
+
+ override fun write(
+ target: Path,
+ metamodel: Metamodel.KeyApi,
+ pages: List
+ ) {
+ val flavour = SFMFlavourDescriptor() // Markdown + Github + Jetbrains
+ val parsedTree = MarkdownParser(flavour).buildMarkdownTreeFromString(text)
+ val html = HtmlGenerator(text, parsedTree, flavour).generateHtml()
+ target.writeText(MarkdownPage(html, metamodel, pages).render())
+ }
+}
+
+
+abstract class BasePage(
+ metamodel: Metamodel.KeyApi,
+ val pages: List,
+ val pageTitle: String = "KeY API Documentation"
+) {
+ val segmentDocumentation: Map = metamodel.segmentDocumentation
+ val types: List =
+ metamodel.types.values
+ .sortedBy { it.name }
+ .toList()
+ val endpoints: List = metamodel.endpoints.sortedBy { it.name }.toList()
+ val endpointsBySegment: Map> =
+ metamodel.endpoints
+ .sortedBy { it.name }
+ .groupBy { it.segment() }
+ .toSortedMap()
+
+ val date: String = java.util.Date().toString()
+ private val version: String =
+ KeYResourceManager.getManager().getVersion() +
+ " (" + KeYConstants.INTERNAL_VERSION.substring(0, 8) + ")"
+
+ fun render() =
+ buildString(1024 * 1024) {
+ appendHTML(true).html {
+ head {
+ meta(charset = "utf-8")
+ title { +pageTitle }
+ link("default.css", rel = "stylesheet")
+ link("custom.css", rel = "stylesheet")
+ }
+ body {
+ div {
+ id = "main"
+ nav()
+
+ div {
+ id = "content"
+ content()
+ }
+ }
+ }
+ }
+ }
+
+ protected abstract fun DIV.content()
+
+ protected open fun DIV.nav() {
+ nav {
+ id = "nav"
+ h1 { +"Documentation: KeY JSON-RPC API" }
+ navMetaData()
+ navPages()
+ navTypes()
+ navProcedures()
+ }
+ }
+
+ protected open fun NAV.navPages() {
+ h2 { +"Pages" }
+ ul {
+ pages.forEach {
+ li {
+ a(it.relativeHtmlPath) { +it.title }
+ }
+ }
+ }
+ }
+
+ protected open fun NAV.navProcedures() {
+ h2 { +"Procedures" }
+ ul("segments") {
+ endpointsBySegment.forEach { (segname, seq) ->
+ li {
+ a(href = "${REFERENCE_HTML}#${segname}") { +segname }
+ ul {
+ seq.forEach { ep ->
+ li {
+ a(href = "${REFERENCE_HTML}#${ep.name}") { +ep.name }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+
+ protected open fun NAV.navTypes() {
+ h2 { +"Types" }
+ ul {
+ types.forEach { type ->
+ li {
+ a(href = "${REFERENCE_HTML}#${type.name}") { +type.name }
+ }
+ }
+ }
+ }
+
+ protected open fun NAV.navMetaData() {
+ div {
+ +"""Version: $version
+ Date: $date}"""
+ }
+ }
+
+}
+
+class MarkdownPage(val html: String, metamodel: Metamodel.KeyApi, pages: List) :
+ BasePage(metamodel, pages) {
+ override fun DIV.content() {
+ unsafe { +html }
+ script {
+ type = "module"
+ +"""
+ import mermaid from 'https://cdn.jsdelivr.net/npm/mermaid@11/dist/mermaid.esm.min.mjs';
+ mermaid.initialize({ startOnLoad: true });
+ mermaid.run({ querySelector: '.language-mermaid' });
+ """
+ }
+ }
+}
+
+class ReferencePage(metamodel: Metamodel.KeyApi, pages: List) : BasePage(metamodel, pages) {
+ override fun DIV.content() {
+ h2 { +"Base Definitions" }
+ p {
+ +"This API builds upon and uses the same convention as the "
+ a(href = "https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/") {
+ +"Language Server Protocol"
+ }
+ +". In basic, the protocol builds upon a simple HTTP protocol with a JSON payload. A request message looks as"
+ }
+ div("highlight") {
+ pre {
+ +"""Content-Length: 80\r\n
+ Content-Type: application/vscode-jsonrpc; charset=utf-8\r\n
+ \r\n
+ {
+ "jsonrpc": "2.0",
+ "id": 1,
+ "method": "env/version",
+ "params": {
+ ...
+ }
+ }"""
+ }
+ }
+ p {
+ +"Header "
+ code { +"Content-Type" }
+ +" is optional. The "
+ code { +"""\\r\\n""" }
+ +" are mandatory. The field "
+ code { +"id" }
+ +" make the difference between a request or a notification. "
+ +"Later do not result into a response. A response message contains the fields "
+ code { +"result" }
+ +" or "
+ code { +"error" }
+ +", depending on a normal or exceptional execution of the request."
+ }
+ p {
+ +"The communication is always asynchronous and duplex. "
+ +"Meaning you can send and receive messages at any time. "
+ +"For synchronous calls, the client and server library need to implement a waiting mechanism."
+ }
+
+ // ── Types ────────────────────────────────────────────────────────────────
+ h2 { +"Types" }
+ div("data-type") {
+ for (type in types) {
+ val isEnum = type is EnumType
+ val kind = if (isEnum) "enum" else "type"
+
+ div {
+ id = type.name
+ classes = setOf("data-type", kind)
+
+ h3 {
+ +type.name
+ +" "
+ span("kind") { +" $kind" }
+ }
+
+ div("highlight") {
+ span("k") { +kind }
+ +" "
+ span("kc") {
+ a(href = "#${type.name}") { +type.name }
+ }
+ +" { "
+ br()
+
+ // Struct fields
+ if (type is ObjectType) {
+ type.fields.forEach { field ->
+ div("entry field") {
+ field.documentation?.let { doc ->
+ div("cm") { +"/* ${doc.text} */" }
+ }
+ div {
+ span("kc") {
+ a(href = "#${type.name}") { +type.name }
+ }
+ +" "
+ span("nv") { +field.name }
+ +";"
+ }
+ }
+ }
+ }
+ // Enum values
+ if (type is EnumType) {
+ type.values.sortedBy { it.value }.forEach { value ->
+ value.documentation?.let { doc ->
+ +"/* ${doc.text} */"
+ }
+ +value.value
+ }
+ }
+
+ +"}"
+ }
+
+ type.documentation?.let { doc ->
+ div("documentation") {
+ p { +doc.text }
+ if (doc.others.isNotEmpty()) {
+ ul {
+ doc.others.forEach { entry ->
+ li {
+ strong { +"${entry.name}:" }
+ +" ${entry.value}"
+ }
+ }
+ }
+ }
+ }
+
+ if (type is ObjectType) {
+ type.jsonExample()?.let { example ->
+ div {
+ details {
+ summary { +"Example" }
+ code("highlight") {
+ style = "white-space: pre"
+ +example
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+
+ // ── Endpoints ────────────────────────────────────────────────────────────
+ h2 {
+ id = "endpoints"
+ +"Endpoints"
+ }
+
+ div("endpoints") {
+ val grouped = endpoints.groupBy { it.segment() }
+
+ for ((segment, endpoints) in grouped) {
+ h3 {
+ id = segment
+ +"Segment: $segment"
+ }
+
+ segmentDocumentation[segment]?.let { doc ->
+ div("documentation") {
+ p { +doc.text }
+ if (doc.others.isNotEmpty()) {
+ ul {
+ doc.others.forEach { entry ->
+ li {
+ strong { +"${entry.name}:" }
+ +" ${entry.value}"
+ }
+ }
+ }
+ }
+ }
+ }
+
+ endpoints.sortedBy { it.name }.forEach { ep ->
+
+ val kindClass = if (ep.isAsync) "async" else "sync"
+ val direction =
+ when {
+ ep.sender == "Server" && ep.isAsync -> "server ~~> client"
+ ep.sender == "Server" && !ep.isAsync -> "server --> client"
+ ep.sender == "Client" && !ep.isAsync -> "client --> server"
+ else -> "client ~~> server"
+ }
+
+ div {
+ id = ep.name
+ classes = setOf("endpoint", kindClass, ep.sender)
+
+ h4 {
+ if (ep.isAsync) {
+ span("async") { +"Notification:" }
+ } else {
+ span("sync") { +"Request:" }
+ }
+ +" ${ep.name} "
+ span("direction") { +direction }
+ }
+
+ code("highlight") {
+ +ep.name
+ span("p") { +"(" }
+ ep.args.forEachIndexed { index, arg ->
+ span("kc") { a(href = "#${arg.type}") { +arg.type } }
+ +" "
+ span("nv") { +arg.name }
+ if (index < ep.args.lastIndex) span("p") { +"," }
+ }
+ span("p") { +")" }
+ if (ep is Metamodel.Request) {
+ ep.returnType.let { ret ->
+ span("p") { +":" }
+ +" "
+ span("kc") { a(href = "#${ret.name}") { +ret.name } }
+ }
+ }
+ }
+
+ ep.documentation?.let { doc ->
+ div("documentation") {
+ p { +doc.text }
+ if (doc.others.isNotEmpty()) {
+ ul {
+ doc.others.forEach { entry ->
+ li {
+ strong { +"${entry.name}:" }
+ +" ${entry.value}"
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+}
diff --git a/keyext.api.ktclient/build.gradle.kts b/keyext.api.ktclient/build.gradle.kts
new file mode 100644
index 0000000000..a21f6ca661
--- /dev/null
+++ b/keyext.api.ktclient/build.gradle.kts
@@ -0,0 +1,45 @@
+plugins {
+ id("com.diffplug.spotless")
+ id("org.jetbrains.dokka")
+ id("org.jetbrains.kotlin.multiplatform")
+ kotlin("plugin.serialization") version "2.4.0"
+}
+
+repositories{mavenCentral()}
+
+kotlin {
+ jvm("desktop")
+ js() {
+ browser()
+ nodejs()
+ }
+
+ // --- Source Sets ---
+ sourceSets {
+ commonMain.dependencies {
+ implementation("org.jetbrains.kotlinx:kotlinx-serialization-json:1.11.0")
+ //implementation(libs.ktor.client.core)
+ implementation(libs.kotlinx.coroutines.core)
+ }
+
+ jsMain.dependencies {
+ implementation(libs.kotlinx.coroutines.js)
+ }
+
+ /*
+ androidMain.dependencies {
+ }
+
+ iosMain.dependencies {
+ implementation(libs.ktor.client.darwin)
+ }
+ */
+ val desktopMain by getting {
+ dependencies {
+ //implementation(libs.ktor.client.cio)
+ }
+ }
+ }
+}
+
+//sourceSets.main.get().kotlin.srcDir("src/gen/kotlin")
\ No newline at end of file
diff --git a/keyext.api.ktclient/src/commonMain/kotlin/Test.kt b/keyext.api.ktclient/src/commonMain/kotlin/Test.kt
new file mode 100644
index 0000000000..5d7617030e
--- /dev/null
+++ b/keyext.api.ktclient/src/commonMain/kotlin/Test.kt
@@ -0,0 +1,5 @@
+class Test {
+ fun test() : String {
+ return "test"
+ }
+}
\ No newline at end of file
diff --git a/keyext.api.ktclient/src/commonMain/kotlin/org/key_project/key/api/client/Either.kt b/keyext.api.ktclient/src/commonMain/kotlin/org/key_project/key/api/client/Either.kt
new file mode 100644
index 0000000000..82686187af
--- /dev/null
+++ b/keyext.api.ktclient/src/commonMain/kotlin/org/key_project/key/api/client/Either.kt
@@ -0,0 +1,129 @@
+package org.key_project.key.api.client
+
+/**
+ * Represents a value of one of two possible types, A or B.
+ * Conventionally, Left is used for error/failure cases and Right for success cases.
+ *
+ * @author Alexander Weigl
+ * @version 1 (22.06.26)
+ */
+sealed class Either {
+
+ /** Returns true if this is a Left, false otherwise. */
+ abstract fun isLeft(): Boolean
+
+ /** Returns true if this is a Right, false otherwise. */
+ abstract fun isRight(): Boolean
+
+ /** Returns the value if this is a Left, throws NoSuchElementException if this is a Right. */
+ abstract fun getLeft(): A
+
+ /** Returns the value if this is a Right, throws NoSuchElementException if this is a Left. */
+ abstract fun getRight(): B
+
+ /** Returns the value if this is a Left, or the default value if this is a Right. */
+ abstract fun getLeftOrNull(): A?
+
+ /** Returns the value if this is a Right, or the default value if this is a Left. */
+ abstract fun getRightOrNull(): B?
+
+ abstract fun getLeftOrElse(default: @UnsafeVariance A): A
+ abstract fun getRightOrElse(default: @UnsafeVariance B): B
+
+ /**
+ * Applies [fnL] if this is a Left, or [fnR] if this is a Right.
+ * This is the canonical way to extract a value of type C from an Either.
+ */
+ abstract fun fold(fnL: (A) -> C, fnR: (B) -> C): C
+
+ /**
+ * Maps the Right value using the given function.
+ * If this is a Left, returns the same Left unchanged.
+ */
+ abstract fun map(fn: (B) -> C): Either
+
+ /**
+ * Maps the Left value using the given function.
+ * If this is a Right, returns the same Right unchanged.
+ */
+ abstract fun mapLeft(fn: (A) -> C): Either
+
+ /**
+ * Flatmaps the Right value using the given function.
+ * If this is a Left, returns the same Left unchanged.
+ */
+ abstract fun flatMap(fn: (B) -> Either<@UnsafeVariance A, C>): Either
+
+ /**
+ * Returns this Either if it's a Left, or the result of calling [default] if it's a Right.
+ */
+ abstract fun leftOrElse(default: () -> @UnsafeVariance A): A
+
+ /**
+ * Returns this Either if it's a Right, or the result of calling [default] if it's a Left.
+ */
+ abstract fun rightOrElse(default: () -> @UnsafeVariance B): B
+
+ companion object {
+ /** Creates a Left containing the given value. */
+ fun left(value: A): Either = Left(value)
+
+ /** Creates a Right containing the given value. */
+ fun right(value: B): Either = Right(value)
+ }
+}
+
+/**
+ * Represents the Left side of an Either.
+ */
+class Left(private val value: A) : Either() {
+ override fun isLeft(): Boolean = true
+ override fun isRight(): Boolean = false
+ override fun getLeft(): A = value
+ override fun getRight(): B = throw NoSuchElementException("Cannot get Right value from Left")
+ override fun getLeftOrNull() = value
+ override fun getRightOrNull() = null
+ override fun getLeftOrElse(default: @UnsafeVariance A): A = value
+ override fun getRightOrElse(default: @UnsafeVariance B): B = default
+
+ override fun fold(fnL: (A) -> C, fnR: (B) -> C): C = fnL(value)
+
+ override fun map(fn: (B) -> C): Either = Either.left(value)
+ override fun mapLeft(fn: (A) -> C): Either = Either.left(fn(value))
+ override fun flatMap(fn: (B) -> Either<@UnsafeVariance A, C>): Either = Either.left(value)
+
+ override fun leftOrElse(default: () -> @UnsafeVariance A): A = value
+ override fun rightOrElse(default: () -> @UnsafeVariance B): B = default()
+
+ override fun equals(other: Any?): Boolean = other is Left<*, *> && other.value == value
+ override fun hashCode(): Int = value.hashCode()
+ override fun toString(): String = "Left($value)"
+}
+
+/**
+ * Represents the Right side of an Either.
+ */
+class Right(private val value: B) : Either() {
+ override fun isLeft(): Boolean = false
+ override fun isRight(): Boolean = true
+ override fun getLeft(): A = throw NoSuchElementException("Cannot get Left value from Right")
+ override fun getRight(): B = value
+ override fun getLeftOrElse(default: @UnsafeVariance A): A = default
+ override fun getRightOrElse(default: @UnsafeVariance B): B = value
+
+ override fun getLeftOrNull(): A? = null
+ override fun getRightOrNull(): B? = value
+
+ override fun fold(fnL: (A) -> C, fnR: (B) -> C): C = fnR(value)
+
+ override fun map(fn: (B) -> C): Either = Right(fn(value))
+ override fun mapLeft(fn: (A) -> C): Either = Right(value)
+ override fun flatMap(fn: (B) -> Either<@UnsafeVariance A, C>): Either = fn(value)
+
+ override fun leftOrElse(default: () -> @UnsafeVariance A): A = default()
+ override fun rightOrElse(default: () -> @UnsafeVariance B): B = value
+
+ override fun equals(other: Any?): Boolean = other is Right<*, *> && other.value == value
+ override fun hashCode(): Int = value.hashCode()
+ override fun toString(): String = "Right($value)"
+}
\ No newline at end of file
diff --git a/keyext.api.ktclient/src/commonMain/kotlin/org/key_project/key/api/client/RPCLayer.kt b/keyext.api.ktclient/src/commonMain/kotlin/org/key_project/key/api/client/RPCLayer.kt
new file mode 100644
index 0000000000..7b24260e85
--- /dev/null
+++ b/keyext.api.ktclient/src/commonMain/kotlin/org/key_project/key/api/client/RPCLayer.kt
@@ -0,0 +1,11 @@
+package org.key_project.key.api.client
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (22.06.26)
+ */
+expect class RPCLayer {
+ suspend inline fun callSync(methodName: String, vararg params: Any): T
+ inline fun callAsync(methodName: String, vararg params: Any)
+}
\ No newline at end of file
diff --git a/keyext.api.ktclient/src/desktopMain/kotlin/org/key_project/key/api/client/RPCLayer.desktop.kt b/keyext.api.ktclient/src/desktopMain/kotlin/org/key_project/key/api/client/RPCLayer.desktop.kt
new file mode 100644
index 0000000000..b5171c9234
--- /dev/null
+++ b/keyext.api.ktclient/src/desktopMain/kotlin/org/key_project/key/api/client/RPCLayer.desktop.kt
@@ -0,0 +1,10 @@
+package org.key_project.key.api.client
+
+actual class RPCLayer {
+ actual suspend inline fun callSync(methodName: String, vararg params: Any): T {
+ TODO("Not yet implemented")
+ }
+
+ actual inline fun callAsync(methodName: String, vararg params: Any) {
+ }
+}
\ No newline at end of file
diff --git a/keyext.api.ktclient/src/jsMain/kotlin/org/key_project/key/api/client/RPCLayer.js.kt b/keyext.api.ktclient/src/jsMain/kotlin/org/key_project/key/api/client/RPCLayer.js.kt
new file mode 100644
index 0000000000..3f4a933bfd
--- /dev/null
+++ b/keyext.api.ktclient/src/jsMain/kotlin/org/key_project/key/api/client/RPCLayer.js.kt
@@ -0,0 +1,242 @@
+package org.key_project.key.api.client
+
+import kotlinx.coroutines.*
+import kotlinx.coroutines.channels.Channel
+import org.w3c.dom.WebSocket
+import kotlin.coroutines.Continuation
+import kotlin.coroutines.resume
+import kotlin.coroutines.resumeWithException
+import kotlin.coroutines.suspendCoroutine
+import kotlin.js.Json
+import kotlin.js.json
+
+/**
+ * JSON-RPC 2.0 Layer implementation for JavaScript using WebSockets.
+ *
+ * @author Alexander Weigl
+ * @version 1 (22.06.26)
+ */
+actual class RPCLayer {
+ var websocket: WebSocket? = null
+ val pendingRequests = mutableMapOf()
+ private val notificationChannel = Channel(Channel.UNLIMITED)
+ var requestIdCounter = 0
+
+ /**
+ * Represents a pending request with its continuation.
+ */
+ data class RequestHandler(
+ val continuation: Continuation>,
+ val methodName: String
+ )
+
+ /**
+ * Connects to the JSON-RPC server via WebSocket.
+ * @param url The WebSocket URL of the RPC server
+ */
+ fun connect(url: String): Job = CoroutineScope(Dispatchers.Main).launch {
+ websocket = WebSocket(url).also { ws ->
+ ws.onopen = {
+ console.log("WebSocket connected to $url")
+ }
+ ws.onmessage = { event ->
+ handleIncomingMessage(event.data.toString())
+ }
+ ws.onerror = { error ->
+ console.error("WebSocket error: $error")
+ }
+ ws.onclose = { event ->
+ console.log("WebSocket closed: ${event.code} - ${event.reason}")
+ // Fail all pending requests
+ pendingRequests.values.forEach { handler ->
+ handler.continuation.resumeWithException(
+ RpcException("Connection closed", code = -1)
+ )
+ }
+ pendingRequests.clear()
+ }
+ }
+ }
+
+ /**
+ * Disconnects from the WebSocket server.
+ */
+ fun disconnect() {
+ websocket?.close()
+ websocket = null
+ }
+
+ private fun handleIncomingMessage(data: String) {
+ try {
+ val parsed = JSON.parse(data)
+
+ // Check if this is a response (has "id" field)
+ if (parsed.id != null && parsed.id != undefined) {
+ val id = parsed.id as Int
+ val handler = pendingRequests.remove(id)
+
+ if (handler != null) {
+ when {
+ parsed.error != null && parsed.error != undefined -> {
+ val error = parsed.error
+ val errorCode = error.code as? Int ?: -1
+ val errorMessage = error.message as? String ?: "Unknown error"
+ handler.continuation.resumeWithException(
+ RpcException(errorMessage, code = errorCode)
+ )
+ }
+
+ parsed.result != null && parsed.result != undefined -> {
+ handler.continuation.resume(Result.success(parsed.result))
+ }
+
+ else -> {
+ handler.continuation.resumeWithException(
+ RpcException("Invalid response format", code = -32600)
+ )
+ }
+ }
+ } else {
+ console.warn("Received response for unknown request id: $id")
+ }
+ } else {
+ // This is a notification
+ val method = parsed.method as? String ?: ""
+ val params = parsed.params
+ notificationChannel.trySend(JsonRpcNotification(method, params))
+ }
+ } catch (e: Exception) {
+ console.error("Failed to parse incoming message: $e")
+ }
+ }
+
+ actual suspend inline fun callSync(methodName: String, vararg params: Any): T {
+ val id = ++requestIdCounter
+
+ suspendCoroutine { continuation ->
+ // Build JSON-RPC request using js dynamic object
+ val request = buildJsonRpcRequest(methodName, params.toList(), id)
+ val jsonString = JSON.stringify(request)
+
+ pendingRequests[id] = RequestHandler(
+ continuation = continuation as Continuation>,
+ methodName = methodName
+ )
+
+ websocket?.send(jsonString) ?: continuation.resumeWithException(RpcException("Not connected to server"))
+ }
+ return waitFor(id)?.convertToType()
+ }
+
+ fun waitFor(id: Any): Json {
+ TODO("Not yet implemented")
+ }
+
+ actual inline fun callAsync(methodName: String, vararg params: Any) {
+ // No ID means notification (no response expected)
+ val request = buildJsonRpcRequest(methodName, params.toList(), null)
+ val jsonString = JSON.stringify(request)
+
+ websocket?.send(jsonString)
+ ?: throw RpcException("Not connected to server")
+ }
+
+ /**
+ * Builds a JSON-RPC 2.0 request object.
+ */
+ fun buildJsonRpcRequest(method: String, params: List, id: Int?): dynamic {
+ return json(
+ "jsonrpc" to "2.0",
+ "method" to method,
+ "params" to params.map { convertToJsonValue(it) }.toTypedArray(),
+ "id" to (id ?: undefined)
+ )
+ }
+
+ /**
+ * Converts a Kotlin/JS value to a JSON-compatible dynamic value.
+ */
+ private fun convertToJsonValue(value: Any?): dynamic {
+ return when (value) {
+ null -> null
+ is String -> value
+ is Number -> value
+ is Boolean -> value
+ is Enum<*> -> value.name
+ is Map<*, *> -> jsObjectFromMap(value)
+ is List<*> -> value.map { convertToJsonValue(it) }.toTypedArray()
+ is Array<*> -> value.map { convertToJsonValue(it) }.toTypedArray()
+ else -> value.toString()
+ }
+ }
+
+ /**
+ * Creates a JS object from a Kotlin map.
+ */
+ private fun jsObjectFromMap(map: Map<*, *>): dynamic {
+ val obj = js("{}")
+ map.forEach { (key, value) ->
+ if (key != null) {
+ obj[key.toString()] = convertToJsonValue(value)
+ }
+ }
+ return obj
+ }
+
+ /**
+ * Converts a dynamic JS result to the expected Kotlin type.
+ */
+ @Suppress("UNCHECKED_CAST")
+ private inline fun convertToType(result: dynamic): T {
+ return when {
+ result === null || result == undefined -> null as T
+ result is Boolean -> result as T
+ result is Number -> {
+ when (T::class) {
+ Int::class -> result.toInt() as T
+ Long::class -> result.toLong() as T
+ Double::class -> result.toDouble() as T
+ Float::class -> result.toFloat() as T
+ Short::class -> result.toShort() as T
+ Byte::class -> result.toByte() as T
+ else -> result as T
+ }
+ }
+
+ result is String -> {
+ when (T::class) {
+ String::class -> result as T
+ Int::class -> result.toInt() as T
+ Long::class -> result.toLong() as T
+ Double::class -> result.toDouble() as T
+ else -> result as T
+ }
+ }
+
+ else -> result as T
+ }
+ }
+
+ /**
+ * Checks if the WebSocket connection is open.
+ */
+ fun isConnected(): Boolean = websocket?.readyState == WebSocket.OPEN
+
+ /**
+ * Returns a flow of incoming notifications.
+ */
+ fun notifications() = notificationChannel.receiveAsFlow()
+}
+
+/**
+ * Represents an incoming JSON-RPC notification.
+ */
+private data class JsonRpcNotification(
+ val method: String,
+ val params: dynamic
+)
+
+/**
+ * RPC Exception carrying error information from the server.
+ */
+class RpcException(message: String, val code: Int = -1) : Exception(message)
\ No newline at end of file
diff --git a/settings.gradle.kts b/settings.gradle.kts
index ac0d126294..d127c7e040 100644
--- a/settings.gradle.kts
+++ b/settings.gradle.kts
@@ -4,3 +4,4 @@ plugins {
rootProject.name = "key-rpc"
include("keyext.api.app", "keyext.api", "keyext.api.doc", "keyext.api.client")
+include("keyext.api.ktclient")