diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml index 3825ef30c7..c7f51fa081 100644 --- a/gradle/libs.versions.toml +++ b/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" } diff --git a/keyext.api/build.gradle.kts b/keyext.api/build.gradle.kts index b4c668779c..2b461dc61f 100644 --- a/keyext.api/build.gradle.kts +++ b/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) diff --git a/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java b/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java index 68bee186ce..a88df53f4d 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java @@ -164,12 +164,12 @@ public CompletableFuture 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); } }); diff --git a/keyext.api/src/main/java/org/keyproject/key/api/TermActionUtil.java b/keyext.api/src/main/java/org/keyproject/key/api/TermActionUtil.java index a5def30d5b..45ef0dfa81 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/TermActionUtil.java +++ b/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 removeRewrites( ImmutableList list) { - ImmutableList result = ImmutableSLList.nil(); + ImmutableList result = ImmutableList.nil(); for (TacletApp tacletApp : list) { Taclet taclet = tacletApp.taclet(); result = (taclet instanceof RewriteTaclet ? result : result.prepend(tacletApp)); diff --git a/keyext.web/build.gradle.kts b/keyext.web/build.gradle.kts new file mode 100644 index 0000000000..c083e39f32 --- /dev/null +++ b/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) +} \ No newline at end of file diff --git a/keyext.web/src/main/java/org/key_project/key/webui/JsonRpcWebSocketEndpoint.java b/keyext.web/src/main/java/org/key_project/key/webui/JsonRpcWebSocketEndpoint.java new file mode 100644 index 0000000000..295979c3dd --- /dev/null +++ b/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() + .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(); + } +} diff --git a/keyext.web/src/main/java/org/key_project/key/webui/WebUi.java b/keyext.web/src/main/java/org/key_project/key/webui/WebUi.java new file mode 100644 index 0000000000..95baadd1e5 --- /dev/null +++ b/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(); + } +} diff --git a/keyext.web/src/main/resources/static/favicon.png b/keyext.web/src/main/resources/static/favicon.png new file mode 100644 index 0000000000..825b9e65af Binary files /dev/null and b/keyext.web/src/main/resources/static/favicon.png differ diff --git a/keyext.web/src/main/resources/static/index.html b/keyext.web/src/main/resources/static/index.html new file mode 100644 index 0000000000..6faba62c8e --- /dev/null +++ b/keyext.web/src/main/resources/static/index.html @@ -0,0 +1,52 @@ + + + + + + + + KeY-τ + + + + + + + + + + + + + + + +
+ +
+ + + + diff --git a/settings.gradle.kts b/settings.gradle.kts index ac0d126294..ff873a57c3 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.web") \ No newline at end of file