add key-tau into one runnable thing

gradle/libs.versions.toml

@@ -11,6 +11,8 @@ therapi = "0.15.0"
 kotlin-gradle-plugin = "2.4.0"
 dokka = "2.2.0"
 spotless = "8.7.0"
+shadow = "9.4.1"
+jetty = "12.1.10"
 
 [libraries]
 kotlin-gradle-plugin = { module = "org.jetbrains.kotlin:kotlin-gradle-plugin", version.ref = "kotlin-gradle-plugin" }
@@ -30,3 +32,8 @@ therapi-runtime-javadoc-scribe = { module = "com.github.therapi:therapi-runtime-
 therapi-runtime-javadoc = { module = "com.github.therapi:therapi-runtime-javadoc", version.ref = "therapi" }
 clickt = { module = "com.github.ajalt.clikt:clikt", version = "5.1.0" }
 vanniktech-maven = { module = "com.vanniktech.maven.publish:com.vanniktech.maven.publish.gradle.plugin", version = "0.37.0" }
+jetty-server = { module = "org.eclipse.jetty:jetty-server", version.ref = "jetty" }
+jetty-ee11-websocket-jakarta-server = { module = "org.eclipse.jetty.ee11.websocket:jetty-ee11-websocket-jakarta-server", version.ref = "jetty" }
+
+[plugins]
+shadow = { id = "com.gradleup.shadow", version.ref = "shadow" }

keyext.api/build.gradle.kts

@@ -17,9 +17,9 @@ dependencies {
     }
 
     api(libs.lsp4j.jsonrpc)
-    implementation(libs.lsp4j.websocket.jakarta)
-    implementation(libs.jetty.websocket.javax.server)
-    implementation(libs.picocli)
+    api(libs.lsp4j.websocket.jakarta)
+    api(libs.jetty.websocket.javax.server)
+    api(libs.picocli)
     implementation(libs.guava)
     annotationProcessor(libs.therapi.runtime.javadoc.scribe)
     api(libs.therapi.runtime.javadoc)

keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java

@@ -164,12 +164,12 @@ public CompletableFuture<MacroStatistic> script(ProofId proofId, String scriptLi
             var proof = data.find(proofId);
             var env = data.find(proofId.env());
             var script = ParsingFacade.parseScript(scriptLine);
-            var pe = new ProofScriptEngine(script);
+            var pe = new ProofScriptEngine(proof);
 
             try {
-                pe.execute((AbstractUserInterfaceControl) env.getProofControl(), proof);
+                pe.execute((AbstractUserInterfaceControl) env.getProofControl(), script);
                 return new MacroStatistic(proofId, scriptLine, -1, -1);
-            } catch (IOException | InterruptedException | ScriptException e) {
+            } catch (InterruptedException | ScriptException e) {
                 throw new RuntimeException(e);
             }
         });

keyext.api/src/main/java/org/keyproject/key/api/TermActionUtil.java

@@ -21,7 +21,6 @@
 import org.key_project.prover.proof.rulefilter.TacletFilter;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.reflection.ClassLoaderUtil;
 
 import org.jspecify.annotations.NonNull;
@@ -142,7 +141,7 @@ private int add(TermActionDesc ta) {
      */
     private static ImmutableList<TacletApp> removeRewrites(
             ImmutableList<TacletApp> list) {
-        ImmutableList<TacletApp> result = ImmutableSLList.nil();
+        ImmutableList<TacletApp> result = ImmutableList.nil();
         for (TacletApp tacletApp : list) {
             Taclet taclet = tacletApp.taclet();
             result = (taclet instanceof RewriteTaclet ? result : result.prepend(tacletApp));

keyext.web/build.gradle.kts

@@ -0,0 +1,17 @@
+plugins {
+    id("buildlogic.java-library-conventions")
+    application
+    alias(libs.plugins.shadow)
+}
+
+description = "A web interface for KeY"
+
+application {
+    mainClass.set("org.key_project.key.webui.WebUi")
+}
+
+dependencies {
+    implementation(project(":keyext.api"))
+    implementation(libs.jetty.server)
+    implementation(libs.jetty.ee11.websocket.jakarta.server)
+}

keyext.web/src/main/java/org/key_project/key/webui/JsonRpcWebSocketEndpoint.java

@@ -0,0 +1,56 @@
+package org.key_project.key.webui;
+
+import jakarta.websocket.OnClose;
+import jakarta.websocket.OnError;
+import jakarta.websocket.OnOpen;
+import jakarta.websocket.Session;
+import jakarta.websocket.server.ServerEndpoint;
+import org.eclipse.lsp4j.websocket.jakarta.WebSocketLauncherBuilder;
+import org.keyproject.key.api.KeyApiImpl;
+import org.keyproject.key.api.StartServer;
+import org.keyproject.key.api.remoteclient.ClientApi;
+
+import java.io.IOException;
+import java.io.PrintWriter;
+import java.util.concurrent.ExecutionException;
+import java.util.concurrent.ExecutorService;
+import java.util.concurrent.Executors;
+import java.util.concurrent.TimeUnit;
+
+/**
+ *
+ * @author Alexander Weigl
+ * @version 1 (11.06.26)
+ */
+@ServerEndpoint("/ws/jsonrpc")
+public class JsonRpcWebSocketEndpoint {
+    private static final ExecutorService threadPool = Executors.newCachedThreadPool();
+    private static final KeyApiImpl keyApi = new KeyApiImpl();
+
+    @OnOpen
+    public void onOpen(Session session) throws IOException, ExecutionException, InterruptedException {
+        session.setMaxIdleTimeout(TimeUnit.HOURS.toMillis(24));
+        var launcherBuilder = new WebSocketLauncherBuilder<ClientApi>()
+                .setSession(session)
+                .traceMessages(new PrintWriter(System.err))
+                .validateMessages(true);
+
+        launcherBuilder.configureGson(StartServer::configureJson);
+        launcherBuilder.setLocalService(keyApi);
+        launcherBuilder.setRemoteInterface(ClientApi.class);
+
+        final var clientApiLauncher = launcherBuilder.create();
+        keyApi.setClientApi(clientApiLauncher.getRemoteProxy());
+        //clientApiLauncher.startListening();
+    }
+
+    @OnClose
+    public void onClose(Session session) {
+
+    }
+
+    @OnError
+    public void onError(Session session, Throwable throwable) {
+        throwable.printStackTrace();
+    }
+}

keyext.web/src/main/java/org/key_project/key/webui/WebUi.java

@@ -0,0 +1,48 @@
+package org.key_project.key.webui;
+
+import org.eclipse.jetty.ee11.servlet.DefaultServlet;
+import org.eclipse.jetty.ee11.servlet.ServletContextHandler;
+import org.eclipse.jetty.ee11.websocket.jakarta.server.config.JakartaWebSocketServletContainerInitializer;
+import org.eclipse.jetty.server.Server;
+import org.eclipse.jetty.util.resource.Resource;
+import org.eclipse.jetty.util.resource.ResourceFactory;
+
+public class WebUi {
+    public static void main(String[] args) throws Exception {
+        startNetty();
+    }
+
+    private static void startNetty() throws Exception {
+        Server server = new Server(8080);
+        ServletContextHandler context = new ServletContextHandler();
+        context.setContextPath("/");
+
+        // Static files from classpath
+        ResourceFactory resourceFactory = ResourceFactory.of(context);
+        Resource staticResources = resourceFactory.newClassLoaderResource("static");
+        if (staticResources == null || !staticResources.exists()) {
+            throw new IllegalStateException("Classpath resource 'static' not found");
+        }
+        context.setBaseResource(staticResources);
+
+        // Enable Jakarta WebSocket
+        JakartaWebSocketServletContainerInitializer.configure(context, (servletContext, wsContainer) -> {
+            wsContainer.setDefaultMaxTextMessageBufferSize(128 * 1024);
+            wsContainer.addEndpoint(JsonRpcWebSocketEndpoint.class);
+        });
+
+        // Serve static files
+        context.addServlet(DefaultServlet.class, "/");
+        server.setHandler(context);
+        server.start();
+
+        System.out.println("Server running at http://localhost:8080");
+        System.out.println("WebSocket endpoint available at ws://localhost:8080/ws/jsonrpc");
+
+        var pb = new ProcessBuilder("google-chrome", "--app=http://localhost:8080")
+            .start();
+        System.out.println("You can use: google-chrome --app=http://localhost:8080");
+
+        server.join();
+    }
+}

keyext.web/src/main/resources/static/index.html

@@ -0,0 +1,52 @@
+<!doctype html>
+<html lang="en">
+
+<head>
+    <meta charset="utf-8" />
+    <link rel="icon" href="/favicon.png" />
+    <meta name="viewport" content="width=device-width, initial-scale=1" />
+    <title>KeY-τ</title>
+    <link href="/_app/immutable/entry/start.BtwCXLFx.js" rel="modulepreload">
+		<link href="/_app/immutable/chunks/CwrZi-qA.js" rel="modulepreload">
+		<link href="/_app/immutable/chunks/B8xKMZX0.js" rel="modulepreload">
+		<link href="/_app/immutable/chunks/DOHFA51K.js" rel="modulepreload">
+		<link href="/_app/immutable/entry/app.Ct5uxRNT.js" rel="modulepreload">
+		<link href="/_app/immutable/chunks/7wWjHvTU.js" rel="modulepreload">
+		<link href="/_app/immutable/chunks/o-yfdNR1.js" rel="modulepreload">
+		<link href="/_app/immutable/chunks/CzhP5laV.js" rel="modulepreload">
+		<link href="/_app/immutable/chunks/CoTS-PA8.js" rel="modulepreload">
+		<link href="/_app/immutable/nodes/0.D0Qjos9c.js" rel="modulepreload">
+		<link href="/_app/immutable/chunks/DcP_HY-I.js" rel="modulepreload">
+
+</head>
+
+<body data-sveltekit-preload-data="hover">
+    <div style="display: contents">
+			<script>
+				{
+
+					__sveltekit_iz9ql3 = {
+						base: ""
+					};
+
+					const element = document.currentScript.parentElement;
+
+					Promise.all([
+						import("/_app/immutable/entry/start.BtwCXLFx.js"),
+						import("/_app/immutable/entry/app.Ct5uxRNT.js")
+					]).then(([kit, app]) => {
+						kit.start(app, element);
+					});
+				}
+			</script>
+		</div>
+</body>
+<style>
+    body {
+        margin: 0;
+        height: 100vh;
+        width: 100vw;
+    }
+</style>
+
+</html>

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.web")