33 files changed, 2104 insertions, 0 deletions

diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/CacheControlFilter.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/CacheControlFilter.java
new file mode 100644
index 00000000..b13ae95d
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/CacheControlFilter.java
@@ -0,0 +1,52 @@
+package tools.refinery.language.web;
+
+import java.io.IOException;
+import java.time.Duration;
+import java.util.regex.Pattern;
+
+import org.eclipse.jetty.http.HttpHeader;
+
+import jakarta.servlet.Filter;
+import jakarta.servlet.FilterChain;
+import jakarta.servlet.FilterConfig;
+import jakarta.servlet.ServletException;
+import jakarta.servlet.ServletRequest;
+import jakarta.servlet.ServletResponse;
+import jakarta.servlet.http.HttpServletRequest;
+import jakarta.servlet.http.HttpServletResponse;
+
+public class CacheControlFilter implements Filter {
+        private static final Pattern CACHE_URI_PATTERN = Pattern.compile(".*\\.(css|gif|js|map|png|svg|woff2)");
+
+        private static final Duration EXPIRY = Duration.ofDays(365);
+
+        private static final String CACHE_CONTROL_CACHE_VALUE = "public, max-age: " + EXPIRY.toSeconds() + ", immutable";
+
+        private static final String CACHE_CONTROL_NO_CACHE_VALUE = "no-cache, no-store, max-age: 0, must-revalidate";
+
+        @Override
+        public void init(FilterConfig filterConfig) throws ServletException {
+                // Nothing to initialize.
+        }
+
+        @Override
+        public void doFilter(ServletRequest request, ServletResponse response, FilterChain chain)
+                        throws IOException, ServletException {
+                if (request instanceof HttpServletRequest httpRequest && response instanceof HttpServletResponse httpResponse) {
+                        if (CACHE_URI_PATTERN.matcher(httpRequest.getRequestURI()).matches()) {
+                                httpResponse.setHeader(HttpHeader.CACHE_CONTROL.asString(), CACHE_CONTROL_CACHE_VALUE);
+                                httpResponse.setDateHeader(HttpHeader.EXPIRES.asString(),
+                                                System.currentTimeMillis() + EXPIRY.toMillis());
+                        } else {
+                                httpResponse.setHeader(HttpHeader.CACHE_CONTROL.asString(), CACHE_CONTROL_NO_CACHE_VALUE);
+                                httpResponse.setDateHeader(HttpHeader.EXPIRES.asString(), 0);
+                        }
+                }
+                chain.doFilter(request, response);
+        }
+
+        @Override
+        public void destroy() {
+                // Nothing to dispose.
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/ProblemWebModule.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/ProblemWebModule.java
new file mode 100644
index 00000000..ec55036f
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/ProblemWebModule.java
@@ -0,0 +1,35 @@
+/*
+ * generated by Xtext 2.25.0
+ */
+package tools.refinery.language.web;
+
+import org.eclipse.xtext.web.server.XtextServiceDispatcher;
+import org.eclipse.xtext.web.server.model.IWebDocumentProvider;
+import org.eclipse.xtext.web.server.model.XtextWebDocumentAccess;
+import org.eclipse.xtext.web.server.occurrences.OccurrencesService;
+
+import tools.refinery.language.web.occurrences.ProblemOccurrencesService;
+import tools.refinery.language.web.xtext.server.push.PushServiceDispatcher;
+import tools.refinery.language.web.xtext.server.push.PushWebDocumentAccess;
+import tools.refinery.language.web.xtext.server.push.PushWebDocumentProvider;
+
+/**
+ * Use this class to register additional components to be used within the web application.
+ */
+public class ProblemWebModule extends AbstractProblemWebModule {
+        public Class<? extends IWebDocumentProvider> bindIWebDocumentProvider() {
+                return PushWebDocumentProvider.class;
+        }
+        
+        public Class<? extends XtextWebDocumentAccess> bindXtextWebDocumentAccess() {
+                return PushWebDocumentAccess.class;
+        }
+        
+        public Class<? extends XtextServiceDispatcher> bindXtextServiceDispatcher() {
+                return PushServiceDispatcher.class;
+        }
+        
+        public Class<? extends OccurrencesService> bindOccurrencesService() {
+                return ProblemOccurrencesService.class;
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/ProblemWebSetup.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/ProblemWebSetup.java
new file mode 100644
index 00000000..4738bc80
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/ProblemWebSetup.java
@@ -0,0 +1,25 @@
+/*
+ * generated by Xtext 2.25.0
+ */
+package tools.refinery.language.web;
+
+import org.eclipse.xtext.util.Modules2;
+
+import com.google.inject.Guice;
+import com.google.inject.Injector;
+
+import tools.refinery.language.ProblemRuntimeModule;
+import tools.refinery.language.ProblemStandaloneSetup;
+import tools.refinery.language.ide.ProblemIdeModule;
+
+/**
+ * Initialization support for running Xtext languages in web applications.
+ */
+public class ProblemWebSetup extends ProblemStandaloneSetup {
+        
+        @Override
+        public Injector createInjector() {
+                return Guice.createInjector(Modules2.mixin(new ProblemRuntimeModule(), new ProblemIdeModule(), new ProblemWebModule()));
+        }
+        
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/ProblemWebSocketServlet.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/ProblemWebSocketServlet.java
new file mode 100644
index 00000000..df67b521
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/ProblemWebSocketServlet.java
@@ -0,0 +1,29 @@
+package tools.refinery.language.web;
+
+import org.eclipse.xtext.util.DisposableRegistry;
+
+import jakarta.servlet.ServletException;
+import tools.refinery.language.web.xtext.servlet.XtextWebSocketServlet;
+
+public class ProblemWebSocketServlet extends XtextWebSocketServlet {
+
+        private static final long serialVersionUID = -7040955470384797008L;
+
+        private transient DisposableRegistry disposableRegistry;
+
+        @Override
+        public void init() throws ServletException {
+                super.init();
+                var injector = new ProblemWebSetup().createInjectorAndDoEMFRegistration();
+                this.disposableRegistry = injector.getInstance(DisposableRegistry.class);
+        }
+
+        @Override
+        public void destroy() {
+                if (disposableRegistry != null) {
+                        disposableRegistry.dispose();
+                        disposableRegistry = null;
+                }
+                super.destroy();
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/ServerLauncher.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/ServerLauncher.java
new file mode 100644
index 00000000..ffd903d0
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/ServerLauncher.java
@@ -0,0 +1,192 @@
+/*
+ * generated by Xtext 2.25.0
+ */
+package tools.refinery.language.web;
+
+import java.io.File;
+import java.io.IOException;
+import java.net.InetSocketAddress;
+import java.net.URI;
+import java.net.URISyntaxException;
+import java.util.EnumSet;
+import java.util.Optional;
+import java.util.Set;
+
+import org.eclipse.jetty.server.Server;
+import org.eclipse.jetty.server.session.SessionHandler;
+import org.eclipse.jetty.servlet.DefaultServlet;
+import org.eclipse.jetty.servlet.ServletContextHandler;
+import org.eclipse.jetty.servlet.ServletHolder;
+import org.eclipse.jetty.util.resource.Resource;
+import org.eclipse.jetty.websocket.server.config.JettyWebSocketServletContainerInitializer;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import jakarta.servlet.DispatcherType;
+import jakarta.servlet.SessionTrackingMode;
+import tools.refinery.language.web.xtext.servlet.XtextWebSocketServlet;
+
+public class ServerLauncher {
+        public static final String DEFAULT_LISTEN_ADDRESS = "localhost";
+
+        public static final int DEFAULT_LISTEN_PORT = 1312;
+
+        public static final int DEFAULT_PUBLIC_PORT = 443;
+
+        public static final int HTTP_DEFAULT_PORT = 80;
+
+        public static final int HTTPS_DEFAULT_PORT = 443;
+        
+        public static final String ALLOWED_ORIGINS_SEPARATOR = ";";
+
+        private static final Logger LOG = LoggerFactory.getLogger(ServerLauncher.class);
+
+        private final Server server;
+
+        public ServerLauncher(InetSocketAddress bindAddress, Resource baseResource, Optional<String[]> allowedOrigins) {
+                server = new Server(bindAddress);
+                var handler = new ServletContextHandler();
+                addSessionHandler(handler);
+                addProblemServlet(handler, allowedOrigins);
+                if (baseResource != null) {
+                        handler.setBaseResource(baseResource);
+                        handler.setWelcomeFiles(new String[] { "index.html" });
+                        addDefaultServlet(handler);
+                }
+                handler.addFilter(CacheControlFilter.class, "/*", EnumSet.of(DispatcherType.REQUEST));
+                server.setHandler(handler);
+        }
+
+        private void addSessionHandler(ServletContextHandler handler) {
+                var sessionHandler = new SessionHandler();
+                sessionHandler.setSessionTrackingModes(Set.of(SessionTrackingMode.COOKIE));
+                handler.setSessionHandler(sessionHandler);
+        }
+
+        private void addProblemServlet(ServletContextHandler handler, Optional<String[]> allowedOrigins) {
+                var problemServletHolder = new ServletHolder(ProblemWebSocketServlet.class);
+                if (allowedOrigins.isEmpty()) {
+                        LOG.warn("All WebSocket origins are allowed! This setting should not be used in production!");
+                } else {
+                        var allowedOriginsString = String.join(XtextWebSocketServlet.ALLOWED_ORIGINS_SEPARATOR,
+                                        allowedOrigins.get());
+                        problemServletHolder.setInitParameter(XtextWebSocketServlet.ALLOWED_ORIGINS_INIT_PARAM,
+                                        allowedOriginsString);
+                }
+                handler.addServlet(problemServletHolder, "/xtext-service");
+                JettyWebSocketServletContainerInitializer.configure(handler, null);
+        }
+
+        private void addDefaultServlet(ServletContextHandler handler) {
+                var defaultServletHolder = new ServletHolder(DefaultServlet.class);
+                var isWindows = System.getProperty("os.name").toLowerCase().contains("win");
+                // Avoid file locking on Windows: https://stackoverflow.com/a/4985717
+                // See also the related Jetty ticket:
+                // https://github.com/eclipse/jetty.project/issues/2925
+                defaultServletHolder.setInitParameter("useFileMappedBuffer", isWindows ? "false" : "true");
+                handler.addServlet(defaultServletHolder, "/");
+        }
+
+        public void start() throws Exception {
+                server.start();
+                LOG.info("Server started on {}", server.getURI());
+                server.join();
+        }
+
+        public static void main(String[] args) {
+                try {
+                        var bindAddress = getBindAddress();
+                        var baseResource = getBaseResource();
+                        var allowedOrigins = getAllowedOrigins();
+                        var serverLauncher = new ServerLauncher(bindAddress, baseResource, allowedOrigins);
+                        serverLauncher.start();
+                } catch (Exception exception) {
+                        LOG.error("Fatal server error", exception);
+                        System.exit(1);
+                }
+        }
+
+        private static String getListenAddress() {
+                var listenAddress = System.getenv("LISTEN_ADDRESS");
+                if (listenAddress == null) {
+                        return DEFAULT_LISTEN_ADDRESS;
+                }
+                return listenAddress;
+        }
+
+        private static int getListenPort() {
+                var portStr = System.getenv("LISTEN_PORT");
+                if (portStr != null) {
+                        return Integer.parseInt(portStr);
+                }
+                return DEFAULT_LISTEN_PORT;
+        }
+
+        private static InetSocketAddress getBindAddress() {
+                var listenAddress = getListenAddress();
+                var listenPort = getListenPort();
+                return new InetSocketAddress(listenAddress, listenPort);
+        }
+
+        private static Resource getBaseResource() throws IOException, URISyntaxException {
+                var baseResourceOverride = System.getenv("BASE_RESOURCE");
+                if (baseResourceOverride != null) {
+                        // If a user override is provided, use it.
+                        return Resource.newResource(baseResourceOverride);
+                }
+                var indexUrlInJar = ServerLauncher.class.getResource("/webapp/index.html");
+                if (indexUrlInJar != null) {
+                        // If the app is packaged in the jar, serve it.
+                        var webRootUri = URI.create(indexUrlInJar.toURI().toASCIIString().replaceFirst("/index.html$", "/"));
+                        return Resource.newResource(webRootUri);
+                }
+                // Look for unpacked production artifacts (convenience for running from IDE).
+                var unpackedResourcePathComponents = new String[] { System.getProperty("user.dir"), "build", "webpack",
+                                "production" };
+                var unpackedResourceDir = new File(String.join(File.separator, unpackedResourcePathComponents));
+                if (unpackedResourceDir.isDirectory()) {
+                        return Resource.newResource(unpackedResourceDir);
+                }
+                // Fall back to just serving a 404.
+                return null;
+        }
+
+        private static String getPublicHost() {
+                var publicHost = System.getenv("PUBLIC_HOST");
+                if (publicHost != null) {
+                        return publicHost.toLowerCase();
+                }
+                return null;
+        }
+
+        private static int getPublicPort() {
+                var portStr = System.getenv("PUBLIC_PORT");
+                if (portStr != null) {
+                        return Integer.parseInt(portStr);
+                }
+                return DEFAULT_LISTEN_PORT;
+        }
+
+        private static Optional<String[]> getAllowedOrigins() {
+                var allowedOrigins = System.getenv("ALLOWED_ORIGINS");
+                if (allowedOrigins != null) {
+                        return Optional.of(allowedOrigins.split(ALLOWED_ORIGINS_SEPARATOR));
+                }
+                return getAllowedOriginsFromPublicHostAndPort();
+        }
+
+        private static Optional<String[]> getAllowedOriginsFromPublicHostAndPort() {
+                var publicHost = getPublicHost();
+                if (publicHost == null) {
+                        return Optional.empty();
+                }
+                int publicPort = getPublicPort();
+                var scheme = publicPort == HTTPS_DEFAULT_PORT ? "https" : "http";
+                var urlWithPort = String.format("%s://%s:%d", scheme, publicHost, publicPort);
+                if (publicPort == HTTPS_DEFAULT_PORT || publicPort == HTTP_DEFAULT_PORT) {
+                        var urlWithoutPort = String.format("%s://%s", scheme, publicHost);
+                        return Optional.of(new String[] { urlWithPort, urlWithoutPort });
+                }
+                return Optional.of(new String[] { urlWithPort });
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/occurrences/ProblemOccurrencesService.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/occurrences/ProblemOccurrencesService.java
new file mode 100644
index 00000000..d32bbb54
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/occurrences/ProblemOccurrencesService.java
@@ -0,0 +1,16 @@
+package tools.refinery.language.web.occurrences;
+
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.xtext.web.server.occurrences.OccurrencesService;
+
+import com.google.inject.Singleton;
+
+import tools.refinery.language.model.problem.NamedElement;
+
+@Singleton
+public class ProblemOccurrencesService extends OccurrencesService {
+        @Override
+        protected boolean filter(EObject element) {
+                return super.filter(element) && element instanceof NamedElement;
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/PongResult.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/PongResult.java
new file mode 100644
index 00000000..fe510f51
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/PongResult.java
@@ -0,0 +1,44 @@
+package tools.refinery.language.web.xtext.server;
+
+import java.util.Objects;
+
+import org.eclipse.xtext.web.server.IServiceResult;
+
+public class PongResult implements IServiceResult {
+        private String pong;
+
+        public PongResult(String pong) {
+                super();
+                this.pong = pong;
+        }
+
+        public String getPong() {
+                return pong;
+        }
+
+        public void setPong(String pong) {
+                this.pong = pong;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(pong);
+        }
+
+        @Override
+        public boolean equals(Object obj) {
+                if (this == obj)
+                        return true;
+                if (obj == null)
+                        return false;
+                if (getClass() != obj.getClass())
+                        return false;
+                PongResult other = (PongResult) obj;
+                return Objects.equals(pong, other.pong);
+        }
+
+        @Override
+        public String toString() {
+                return "PongResult [pong=" + pong + "]";
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/ResponseHandler.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/ResponseHandler.java
new file mode 100644
index 00000000..2a85afe3
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/ResponseHandler.java
@@ -0,0 +1,8 @@
+package tools.refinery.language.web.xtext.server;
+
+import tools.refinery.language.web.xtext.server.message.XtextWebResponse;
+
+@FunctionalInterface
+public interface ResponseHandler {
+        void onResponse(XtextWebResponse response) throws ResponseHandlerException;
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/ResponseHandlerException.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/ResponseHandlerException.java
new file mode 100644
index 00000000..34fcb546
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/ResponseHandlerException.java
@@ -0,0 +1,14 @@
+package tools.refinery.language.web.xtext.server;
+
+public class ResponseHandlerException extends Exception {
+
+        private static final long serialVersionUID = 3589866922420268164L;
+
+        public ResponseHandlerException(String message, Throwable cause) {
+                super(message, cause);
+        }
+
+        public ResponseHandlerException(String message) {
+                super(message);
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/SubscribingServiceContext.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/SubscribingServiceContext.java
new file mode 100644
index 00000000..78e00a9e
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/SubscribingServiceContext.java
@@ -0,0 +1,26 @@
+package tools.refinery.language.web.xtext.server;
+
+import java.util.Set;
+
+import org.eclipse.xtext.web.server.IServiceContext;
+import org.eclipse.xtext.web.server.ISession;
+
+import tools.refinery.language.web.xtext.server.push.PrecomputationListener;
+
+public record SubscribingServiceContext(IServiceContext delegate, PrecomputationListener subscriber)
+                implements IServiceContext {
+        @Override
+        public Set<String> getParameterKeys() {
+                return delegate.getParameterKeys();
+        }
+
+        @Override
+        public String getParameter(String key) {
+                return delegate.getParameter(key);
+        }
+
+        @Override
+        public ISession getSession() {
+                return delegate.getSession();
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/TransactionExecutor.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/TransactionExecutor.java
new file mode 100644
index 00000000..0b417b06
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/TransactionExecutor.java
@@ -0,0 +1,180 @@
+package tools.refinery.language.web.xtext.server;
+
+import java.lang.ref.WeakReference;
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
+import org.eclipse.emf.common.util.URI;
+import org.eclipse.xtext.resource.IResourceServiceProvider;
+import org.eclipse.xtext.util.IDisposable;
+import org.eclipse.xtext.web.server.IServiceContext;
+import org.eclipse.xtext.web.server.IServiceResult;
+import org.eclipse.xtext.web.server.ISession;
+import org.eclipse.xtext.web.server.InvalidRequestException;
+import org.eclipse.xtext.web.server.InvalidRequestException.UnknownLanguageException;
+import org.eclipse.xtext.web.server.XtextServiceDispatcher;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import com.google.common.base.Strings;
+import com.google.inject.Injector;
+
+import tools.refinery.language.web.xtext.server.message.XtextWebErrorKind;
+import tools.refinery.language.web.xtext.server.message.XtextWebErrorResponse;
+import tools.refinery.language.web.xtext.server.message.XtextWebOkResponse;
+import tools.refinery.language.web.xtext.server.message.XtextWebPushMessage;
+import tools.refinery.language.web.xtext.server.message.XtextWebRequest;
+import tools.refinery.language.web.xtext.server.push.PrecomputationListener;
+import tools.refinery.language.web.xtext.server.push.PushWebDocument;
+import tools.refinery.language.web.xtext.servlet.SimpleServiceContext;
+
+public class TransactionExecutor implements IDisposable, PrecomputationListener {
+        private static final Logger LOG = LoggerFactory.getLogger(TransactionExecutor.class);
+
+        private final ISession session;
+
+        private final IResourceServiceProvider.Registry resourceServiceProviderRegistry;
+
+        private final Map<String, WeakReference<PushWebDocument>> subscriptions = new HashMap<>();
+
+        private ResponseHandler responseHandler;
+
+        private Object callPendingLock = new Object();
+
+        private boolean callPending;
+
+        private List<XtextWebPushMessage> pendingPushMessages = new ArrayList<>();
+
+        public TransactionExecutor(ISession session, IResourceServiceProvider.Registry resourceServiceProviderRegistry) {
+                this.session = session;
+                this.resourceServiceProviderRegistry = resourceServiceProviderRegistry;
+        }
+
+        public void setResponseHandler(ResponseHandler responseHandler) {
+                this.responseHandler = responseHandler;
+        }
+
+        public void handleRequest(XtextWebRequest request) throws ResponseHandlerException {
+                var serviceContext = new SimpleServiceContext(session, request.getRequestData());
+                var ping = serviceContext.getParameter("ping");
+                if (ping != null) {
+                        responseHandler.onResponse(new XtextWebOkResponse(request, new PongResult(ping)));
+                        return;
+                }
+                synchronized (callPendingLock) {
+                        if (callPending) {
+                                LOG.error("Reentrant request detected");
+                        }
+                        if (!pendingPushMessages.isEmpty()) {
+                                LOG.error("{} push messages got stuck without a pending request", pendingPushMessages.size());
+                        }
+                        callPending = true;
+                }
+                try {
+                        var injector = getInjector(serviceContext);
+                        var serviceDispatcher = injector.getInstance(XtextServiceDispatcher.class);
+                        var service = serviceDispatcher.getService(new SubscribingServiceContext(serviceContext, this));
+                        var serviceResult = service.getService().apply();
+                        responseHandler.onResponse(new XtextWebOkResponse(request, serviceResult));
+                } catch (InvalidRequestException e) {
+                        responseHandler.onResponse(new XtextWebErrorResponse(request, XtextWebErrorKind.REQUEST_ERROR, e));
+                } catch (RuntimeException e) {
+                        responseHandler.onResponse(new XtextWebErrorResponse(request, XtextWebErrorKind.SERVER_ERROR, e));
+                } finally {
+                        synchronized (callPendingLock) {
+                                for (var message : pendingPushMessages) {
+                                        try {
+                                                responseHandler.onResponse(message);
+                                        } catch (ResponseHandlerException | RuntimeException e) {
+                                                LOG.error("Error while flushing push message", e);
+                                        }
+                                }
+                                pendingPushMessages.clear();
+                                callPending = false;
+                        }
+                }
+        }
+
+        @Override
+        public void onPrecomputedServiceResult(String resourceId, String stateId, String serviceName,
+                        IServiceResult serviceResult) throws ResponseHandlerException {
+                var message = new XtextWebPushMessage(resourceId, stateId, serviceName, serviceResult);
+                synchronized (callPendingLock) {
+                        // If we're currently responding to a call we must delay any push messages until
+                        // the reply is sent, because push messages relating to the new state id must be
+                        // sent after the response with the new state id so that the client knows about
+                        // the new state when it receives the push message.
+                        if (callPending) {
+                                pendingPushMessages.add(message);
+                        } else {
+                                responseHandler.onResponse(message);
+                        }
+                }
+        }
+
+        @Override
+        public void onSubscribeToPrecomputationEvents(String resourceId, PushWebDocument document) {
+                PushWebDocument previousDocument = null;
+                var previousSubscription = subscriptions.get(resourceId);
+                if (previousSubscription != null) {
+                        previousDocument = previousSubscription.get();
+                }
+                if (previousDocument == document) {
+                        return;
+                }
+                if (previousDocument != null) {
+                        previousDocument.removePrecomputationListener(this);
+                }
+                subscriptions.put(resourceId, new WeakReference<>(document));
+        }
+
+        /**
+         * Get the injector to satisfy the request in the {@code serviceContext}.
+         * 
+         * Based on {@link org.eclipse.xtext.web.servlet.XtextServlet#getInjector}.
+         * 
+         * @param serviceContext the Xtext service context of the request
+         * @return the injector for the Xtext language in the request
+         * @throws UnknownLanguageException if the Xtext language cannot be determined
+         */
+        protected Injector getInjector(IServiceContext context) {
+                IResourceServiceProvider resourceServiceProvider = null;
+                var resourceName = context.getParameter("resource");
+                if (resourceName == null) {
+                        resourceName = "";
+                }
+                var emfURI = URI.createURI(resourceName);
+                var contentType = context.getParameter("contentType");
+                if (Strings.isNullOrEmpty(contentType)) {
+                        resourceServiceProvider = resourceServiceProviderRegistry.getResourceServiceProvider(emfURI);
+                        if (resourceServiceProvider == null) {
+                                if (emfURI.toString().isEmpty()) {
+                                        throw new UnknownLanguageException(
+                                                        "Unable to identify the Xtext language: missing parameter 'resource' or 'contentType'.");
+                                } else {
+                                        throw new UnknownLanguageException(
+                                                        "Unable to identify the Xtext language for resource " + emfURI + ".");
+                                }
+                        }
+                } else {
+                        resourceServiceProvider = resourceServiceProviderRegistry.getResourceServiceProvider(emfURI, contentType);
+                        if (resourceServiceProvider == null) {
+                                throw new UnknownLanguageException(
+                                                "Unable to identify the Xtext language for contentType " + contentType + ".");
+                        }
+                }
+                return resourceServiceProvider.get(Injector.class);
+        }
+
+        @Override
+        public void dispose() {
+                for (var subscription : subscriptions.values()) {
+                        var document = subscription.get();
+                        if (document != null) {
+                                document.removePrecomputationListener(this);
+                        }
+                }
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebErrorKind.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebErrorKind.java
new file mode 100644
index 00000000..f74bae74
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebErrorKind.java
@@ -0,0 +1,11 @@
+package tools.refinery.language.web.xtext.server.message;
+
+import com.google.gson.annotations.SerializedName;
+
+public enum XtextWebErrorKind {
+        @SerializedName("request")
+        REQUEST_ERROR,
+
+        @SerializedName("server")
+        SERVER_ERROR,
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebErrorResponse.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebErrorResponse.java
new file mode 100644
index 00000000..01d78c31
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebErrorResponse.java
@@ -0,0 +1,79 @@
+package tools.refinery.language.web.xtext.server.message;
+
+import java.util.Objects;
+
+import com.google.gson.annotations.SerializedName;
+
+public final class XtextWebErrorResponse implements XtextWebResponse {
+        private String id;
+
+        @SerializedName("error")
+        private XtextWebErrorKind errorKind;
+
+        @SerializedName("message")
+        private String errorMessage;
+
+        public XtextWebErrorResponse(String id, XtextWebErrorKind errorKind, String errorMessage) {
+                super();
+                this.id = id;
+                this.errorKind = errorKind;
+                this.errorMessage = errorMessage;
+        }
+
+        public XtextWebErrorResponse(XtextWebRequest request, XtextWebErrorKind errorKind,
+                        String errorMessage) {
+                this(request.getId(), errorKind, errorMessage);
+        }
+
+        public XtextWebErrorResponse(XtextWebRequest request, XtextWebErrorKind errorKind, Throwable t) {
+                this(request, errorKind, t.getMessage());
+        }
+
+        public String getId() {
+                return id;
+        }
+
+        public void setId(String id) {
+                this.id = id;
+        }
+
+        public XtextWebErrorKind getErrorKind() {
+                return errorKind;
+        }
+
+        public void setErrorKind(XtextWebErrorKind errorKind) {
+                this.errorKind = errorKind;
+        }
+
+        public String getErrorMessage() {
+                return errorMessage;
+        }
+
+        public void setErrorMessage(String errorMessage) {
+                this.errorMessage = errorMessage;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(errorKind, errorMessage, id);
+        }
+
+        @Override
+        public boolean equals(Object obj) {
+                if (this == obj)
+                        return true;
+                if (obj == null)
+                        return false;
+                if (getClass() != obj.getClass())
+                        return false;
+                XtextWebErrorResponse other = (XtextWebErrorResponse) obj;
+                return errorKind == other.errorKind && Objects.equals(errorMessage, other.errorMessage)
+                                && Objects.equals(id, other.id);
+        }
+
+        @Override
+        public String toString() {
+                return "XtextWebSocketErrorResponse [id=" + id + ", errorKind=" + errorKind + ", errorMessage=" + errorMessage
+                                + "]";
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebOkResponse.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebOkResponse.java
new file mode 100644
index 00000000..8af27247
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebOkResponse.java
@@ -0,0 +1,72 @@
+package tools.refinery.language.web.xtext.server.message;
+
+import java.util.Objects;
+
+import org.eclipse.xtext.web.server.IServiceResult;
+import org.eclipse.xtext.web.server.IUnwrappableServiceResult;
+
+import com.google.gson.annotations.SerializedName;
+
+public final class XtextWebOkResponse implements XtextWebResponse {
+        private String id;
+
+        @SerializedName("response")
+        private Object responseData;
+
+        public XtextWebOkResponse(String id, Object responseData) {
+                super();
+                this.id = id;
+                this.responseData = responseData;
+        }
+
+        public XtextWebOkResponse(XtextWebRequest request, IServiceResult result) {
+                this(request.getId(), maybeUnwrap(result));
+        }
+
+        public String getId() {
+                return id;
+        }
+
+        public void setId(String id) {
+                this.id = id;
+        }
+
+        public Object getResponseData() {
+                return responseData;
+        }
+
+        public void setResponseData(Object responseData) {
+                this.responseData = responseData;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(id, responseData);
+        }
+
+        @Override
+        public boolean equals(Object obj) {
+                if (this == obj)
+                        return true;
+                if (obj == null)
+                        return false;
+                if (getClass() != obj.getClass())
+                        return false;
+                XtextWebOkResponse other = (XtextWebOkResponse) obj;
+                return Objects.equals(id, other.id) && Objects.equals(responseData, other.responseData);
+        }
+
+        @Override
+        public String toString() {
+                return "XtextWebSocketOkResponse [id=" + id + ", responseData=" + responseData + "]";
+        }
+
+        private static Object maybeUnwrap(IServiceResult result) {
+                if (result instanceof IUnwrappableServiceResult unwrappableServiceResult
+                                && unwrappableServiceResult.getContent() != null) {
+                        return unwrappableServiceResult.getContent();
+                } else {
+                        return result;
+                }
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebPushMessage.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebPushMessage.java
new file mode 100644
index 00000000..c9432e1c
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebPushMessage.java
@@ -0,0 +1,81 @@
+package tools.refinery.language.web.xtext.server.message;
+
+import java.util.Objects;
+
+import com.google.gson.annotations.SerializedName;
+
+public final class XtextWebPushMessage implements XtextWebResponse {    
+        @SerializedName("resource")
+        private String resourceId;
+        
+        private String stateId;
+        
+        private String service;
+        
+        @SerializedName("push")
+        private Object pushData;
+
+        public XtextWebPushMessage(String resourceId, String stateId, String service, Object pushData) {
+                super();
+                this.resourceId = resourceId;
+                this.stateId = stateId;
+                this.service = service;
+                this.pushData = pushData;
+        }
+
+        public String getResourceId() {
+                return resourceId;
+        }
+
+        public void setResourceId(String resourceId) {
+                this.resourceId = resourceId;
+        }
+
+        public String getStateId() {
+                return stateId;
+        }
+
+        public void setStateId(String stateId) {
+                this.stateId = stateId;
+        }
+
+        public String getService() {
+                return service;
+        }
+
+        public void setService(String service) {
+                this.service = service;
+        }
+
+        public Object getPushData() {
+                return pushData;
+        }
+
+        public void setPushData(Object pushData) {
+                this.pushData = pushData;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(pushData, resourceId, service, stateId);
+        }
+
+        @Override
+        public boolean equals(Object obj) {
+                if (this == obj)
+                        return true;
+                if (obj == null)
+                        return false;
+                if (getClass() != obj.getClass())
+                        return false;
+                XtextWebPushMessage other = (XtextWebPushMessage) obj;
+                return Objects.equals(pushData, other.pushData) && Objects.equals(resourceId, other.resourceId)
+                                && Objects.equals(service, other.service) && Objects.equals(stateId, other.stateId);
+        }
+
+        @Override
+        public String toString() {
+                return "XtextWebPushMessage [resourceId=" + resourceId + ", stateId=" + stateId + ", service=" + service
+                                + ", pushData=" + pushData + "]";
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebRequest.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebRequest.java
new file mode 100644
index 00000000..959749f8
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebRequest.java
@@ -0,0 +1,57 @@
+package tools.refinery.language.web.xtext.server.message;
+
+import java.util.Map;
+import java.util.Objects;
+
+import com.google.gson.annotations.SerializedName;
+
+public class XtextWebRequest {
+        private String id;
+
+        @SerializedName("request")
+        private Map<String, String> requestData;
+
+        public XtextWebRequest(String id, Map<String, String> requestData) {
+                super();
+                this.id = id;
+                this.requestData = requestData;
+        }
+
+        public String getId() {
+                return id;
+        }
+
+        public void setId(String id) {
+                this.id = id;
+        }
+
+        public Map<String, String> getRequestData() {
+                return requestData;
+        }
+
+        public void setRequestData(Map<String, String> requestData) {
+                this.requestData = requestData;
+        }
+
+        @Override
+        public int hashCode() {
+                return Objects.hash(id, requestData);
+        }
+
+        @Override
+        public boolean equals(Object obj) {
+                if (this == obj)
+                        return true;
+                if (obj == null)
+                        return false;
+                if (getClass() != obj.getClass())
+                        return false;
+                XtextWebRequest other = (XtextWebRequest) obj;
+                return Objects.equals(id, other.id) && Objects.equals(requestData, other.requestData);
+        }
+
+        @Override
+        public String toString() {
+                return "XtextWebSocketRequest [id=" + id + ", requestData=" + requestData + "]";
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebResponse.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebResponse.java
new file mode 100644
index 00000000..3bd13047
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/message/XtextWebResponse.java
@@ -0,0 +1,4 @@
+package tools.refinery.language.web.xtext.server.message;
+
+public sealed interface XtextWebResponse permits XtextWebOkResponse,XtextWebErrorResponse,XtextWebPushMessage {
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PrecomputationListener.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PrecomputationListener.java
new file mode 100644
index 00000000..79a284db
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PrecomputationListener.java
@@ -0,0 +1,15 @@
+package tools.refinery.language.web.xtext.server.push;
+
+import org.eclipse.xtext.web.server.IServiceResult;
+
+import tools.refinery.language.web.xtext.server.ResponseHandlerException;
+
+@FunctionalInterface
+public interface PrecomputationListener {
+        void onPrecomputedServiceResult(String resourceId, String stateId, String serviceName, IServiceResult serviceResult)
+                        throws ResponseHandlerException;
+
+        default void onSubscribeToPrecomputationEvents(String resourceId, PushWebDocument document) {
+                // Nothing to handle by default.
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushServiceDispatcher.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushServiceDispatcher.java
new file mode 100644
index 00000000..c7b8108d
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushServiceDispatcher.java
@@ -0,0 +1,23 @@
+package tools.refinery.language.web.xtext.server.push;
+
+import org.eclipse.xtext.web.server.IServiceContext;
+import org.eclipse.xtext.web.server.XtextServiceDispatcher;
+import org.eclipse.xtext.web.server.model.XtextWebDocument;
+
+import com.google.inject.Singleton;
+
+import tools.refinery.language.web.xtext.server.SubscribingServiceContext;
+
+@Singleton
+public class PushServiceDispatcher extends XtextServiceDispatcher {
+
+        @Override
+        protected XtextWebDocument getFullTextDocument(String fullText, String resourceId, IServiceContext context) {
+                var document = super.getFullTextDocument(fullText, resourceId, context);
+                if (document instanceof PushWebDocument pushWebDocument
+                                && context instanceof SubscribingServiceContext subscribingContext) {
+                        pushWebDocument.addPrecomputationListener(subscribingContext.subscriber());
+                }
+                return document;
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocument.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocument.java
new file mode 100644
index 00000000..906b9e30
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocument.java
@@ -0,0 +1,89 @@
+package tools.refinery.language.web.xtext.server.push;
+
+import java.util.ArrayList;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+
+import org.eclipse.xtext.util.CancelIndicator;
+import org.eclipse.xtext.web.server.IServiceResult;
+import org.eclipse.xtext.web.server.model.AbstractCachedService;
+import org.eclipse.xtext.web.server.model.DocumentSynchronizer;
+import org.eclipse.xtext.web.server.model.XtextWebDocument;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import com.google.common.collect.ImmutableList;
+
+import tools.refinery.language.web.xtext.server.ResponseHandlerException;
+
+public class PushWebDocument extends XtextWebDocument {
+        private static final Logger LOG = LoggerFactory.getLogger(PushWebDocument.class);
+
+        private final List<PrecomputationListener> precomputationListeners = new ArrayList<>();
+
+        private final Map<Class<?>, IServiceResult> precomputedServices = new HashMap<>();
+
+        public PushWebDocument(String resourceId, DocumentSynchronizer synchronizer) {
+                super(resourceId, synchronizer);
+                if (resourceId == null) {
+                        throw new IllegalArgumentException("resourceId must not be null");
+                }
+        }
+
+        public boolean addPrecomputationListener(PrecomputationListener listener) {
+                synchronized (precomputationListeners) {
+                        if (precomputationListeners.contains(listener)) {
+                                return false;
+                        }
+                        precomputationListeners.add(listener);
+                        listener.onSubscribeToPrecomputationEvents(getResourceId(), this);
+                        return true;
+                }
+        }
+
+        public boolean removePrecomputationListener(PrecomputationListener listener) {
+                synchronized (precomputationListeners) {
+                        return precomputationListeners.remove(listener);
+                }
+        }
+
+        public <T extends IServiceResult> void precomputeServiceResult(AbstractCachedService<T> service, String serviceName,
+                        CancelIndicator cancelIndicator, boolean logCacheMiss) {
+                var result = getCachedServiceResult(service, cancelIndicator, logCacheMiss);
+                if (result == null) {
+                        LOG.error("{} service returned null result", serviceName);
+                        return;
+                }
+                var serviceClass = service.getClass();
+                var previousResult = precomputedServices.get(serviceClass);
+                if (previousResult != null && previousResult.equals(result)) {
+                        return;
+                }
+                precomputedServices.put(serviceClass, result);
+                notifyPrecomputationListeners(serviceName, result);
+        }
+
+        private <T extends IServiceResult> void notifyPrecomputationListeners(String serviceName, T result) {
+                var resourceId = getResourceId();
+                var stateId = getStateId();
+                List<PrecomputationListener> copyOfListeners;
+                synchronized (precomputationListeners) {
+                        copyOfListeners = ImmutableList.copyOf(precomputationListeners);
+                }
+                var toRemove = new ArrayList<PrecomputationListener>();
+                for (var listener : copyOfListeners) {
+                        try {
+                                listener.onPrecomputedServiceResult(resourceId, stateId, serviceName, result);
+                        } catch (ResponseHandlerException e) {
+                                LOG.error("Delivering precomputation push message failed", e);
+                                toRemove.add(listener);
+                        }
+                }
+                if (!toRemove.isEmpty()) {
+                        synchronized (precomputationListeners) {
+                                precomputationListeners.removeAll(toRemove);
+                        }
+                }
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocumentAccess.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocumentAccess.java
new file mode 100644
index 00000000..b3666a86
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocumentAccess.java
@@ -0,0 +1,68 @@
+package tools.refinery.language.web.xtext.server.push;
+
+import org.eclipse.xtext.service.OperationCanceledManager;
+import org.eclipse.xtext.util.CancelIndicator;
+import org.eclipse.xtext.util.concurrent.CancelableUnitOfWork;
+import org.eclipse.xtext.web.server.IServiceResult;
+import org.eclipse.xtext.web.server.model.AbstractCachedService;
+import org.eclipse.xtext.web.server.model.IXtextWebDocument;
+import org.eclipse.xtext.web.server.model.PrecomputedServiceRegistry;
+import org.eclipse.xtext.web.server.model.XtextWebDocument;
+import org.eclipse.xtext.web.server.model.XtextWebDocumentAccess;
+import org.eclipse.xtext.web.server.syntaxcoloring.HighlightingService;
+import org.eclipse.xtext.web.server.validation.ValidationService;
+
+import com.google.inject.Inject;
+
+public class PushWebDocumentAccess extends XtextWebDocumentAccess {
+
+        @Inject
+        private PrecomputedServiceRegistry preComputedServiceRegistry;
+
+        @Inject
+        private OperationCanceledManager operationCanceledManager;
+
+        private PushWebDocument pushDocument;
+
+        @Override
+        protected void init(XtextWebDocument document, String requiredStateId, boolean skipAsyncWork) {
+                super.init(document, requiredStateId, skipAsyncWork);
+                if (document instanceof PushWebDocument newPushDocument) {
+                        pushDocument = newPushDocument;
+                }
+        }
+
+        @Override
+        protected void performPrecomputation(CancelIndicator cancelIndicator) {
+                if (pushDocument == null) {
+                        super.performPrecomputation(cancelIndicator);
+                        return;
+                }
+                for (AbstractCachedService<? extends IServiceResult> service : preComputedServiceRegistry
+                                .getPrecomputedServices()) {
+                        operationCanceledManager.checkCanceled(cancelIndicator);
+                        precomputeServiceResult(service, false);
+                }
+        }
+        
+        protected <T extends IServiceResult> void precomputeServiceResult(AbstractCachedService<T> service, boolean logCacheMiss) {
+                var serviceName = getPrecomputedServiceName(service);
+                readOnly(new CancelableUnitOfWork<Void, IXtextWebDocument>() {
+                        @Override
+                        public java.lang.Void exec(IXtextWebDocument d, CancelIndicator cancelIndicator) throws Exception {
+                                pushDocument.precomputeServiceResult(service, serviceName, cancelIndicator, logCacheMiss);
+                                return null;
+                        }
+                });
+        }
+        
+        protected String getPrecomputedServiceName(AbstractCachedService<? extends IServiceResult> service) {
+                if (service instanceof ValidationService) {
+                        return "validate";
+                }
+                if (service instanceof HighlightingService) {
+                        return "highlight";
+                }
+                throw new IllegalArgumentException("Unknown precomputed service: " + service);
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocumentProvider.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocumentProvider.java
new file mode 100644
index 00000000..fc45f74a
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/server/push/PushWebDocumentProvider.java
@@ -0,0 +1,33 @@
+package tools.refinery.language.web.xtext.server.push;
+
+import org.eclipse.xtext.web.server.IServiceContext;
+import org.eclipse.xtext.web.server.model.DocumentSynchronizer;
+import org.eclipse.xtext.web.server.model.IWebDocumentProvider;
+import org.eclipse.xtext.web.server.model.XtextWebDocument;
+
+import com.google.inject.Inject;
+import com.google.inject.Provider;
+import com.google.inject.Singleton;
+
+/**
+ * Based on
+ * {@link org.eclipse.xtext.web.server.model.IWebDocumentProvider.DefaultImpl}.
+ * 
+ * @author Kristóf Marussy
+ */
+@Singleton
+public class PushWebDocumentProvider implements IWebDocumentProvider {
+        @Inject
+        private Provider<DocumentSynchronizer> synchronizerProvider;
+
+        @Override
+        public XtextWebDocument get(String resourceId, IServiceContext serviceContext) {
+                if (resourceId == null) {
+                        return new XtextWebDocument(resourceId, synchronizerProvider.get());
+                } else {
+                        // We only need to send push messages if a resourceId is specified.
+                        return new PushWebDocument(resourceId,
+                                        serviceContext.getSession().get(DocumentSynchronizer.class, () -> this.synchronizerProvider.get()));
+                }
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/SimpleServiceContext.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/SimpleServiceContext.java
new file mode 100644
index 00000000..43e37160
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/SimpleServiceContext.java
@@ -0,0 +1,26 @@
+package tools.refinery.language.web.xtext.servlet;
+
+import java.util.Map;
+import java.util.Set;
+
+import org.eclipse.xtext.web.server.IServiceContext;
+import org.eclipse.xtext.web.server.ISession;
+
+import com.google.common.collect.ImmutableSet;
+
+public record SimpleServiceContext(ISession session, Map<String, String> parameters) implements IServiceContext {
+        @Override
+        public Set<String> getParameterKeys() {
+                return ImmutableSet.copyOf(parameters.keySet());
+        }
+
+        @Override
+        public String getParameter(String key) {
+                return parameters.get(key);
+        }
+
+        @Override
+        public ISession getSession() {
+                return session;
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/SimpleSession.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/SimpleSession.java
new file mode 100644
index 00000000..09c055a2
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/SimpleSession.java
@@ -0,0 +1,35 @@
+package tools.refinery.language.web.xtext.servlet;
+
+import java.util.HashMap;
+import java.util.Map;
+
+import org.eclipse.xtext.web.server.ISession;
+import org.eclipse.xtext.xbase.lib.Functions.Function0;
+
+public class SimpleSession implements ISession {
+        private Map<Object, Object> map = new HashMap<>();
+
+        @Override
+        public <T> T get(Object key) {
+                @SuppressWarnings("unchecked")
+                var value = (T) map.get(key);
+                return value;
+        }
+
+        @Override
+        public <T> T get(Object key, Function0<? extends T> factory) {
+                @SuppressWarnings("unchecked")
+                var value = (T) map.computeIfAbsent(key, absentKey -> factory.apply());
+                return value;
+        }
+
+        @Override
+        public void put(Object key, Object value) {
+                map.put(key, value);
+        }
+
+        @Override
+        public void remove(Object key) {
+                map.remove(key);
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextStatusCode.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextStatusCode.java
new file mode 100644
index 00000000..0cd229e8
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextStatusCode.java
@@ -0,0 +1,9 @@
+package tools.refinery.language.web.xtext.servlet;
+
+public final class XtextStatusCode {
+        public static final int INVALID_JSON = 4007;
+
+        private XtextStatusCode() {
+                throw new IllegalStateException("This is a static utility class and should not be instantiated directly");
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextWebSocket.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextWebSocket.java
new file mode 100644
index 00000000..fd41f213
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextWebSocket.java
@@ -0,0 +1,133 @@
+package tools.refinery.language.web.xtext.servlet;
+
+import java.io.IOException;
+import java.io.Reader;
+
+import org.eclipse.jetty.websocket.api.Session;
+import org.eclipse.jetty.websocket.api.StatusCode;
+import org.eclipse.jetty.websocket.api.WriteCallback;
+import org.eclipse.jetty.websocket.api.annotations.OnWebSocketClose;
+import org.eclipse.jetty.websocket.api.annotations.OnWebSocketConnect;
+import org.eclipse.jetty.websocket.api.annotations.OnWebSocketError;
+import org.eclipse.jetty.websocket.api.annotations.OnWebSocketMessage;
+import org.eclipse.jetty.websocket.api.annotations.WebSocket;
+import org.eclipse.xtext.resource.IResourceServiceProvider;
+import org.eclipse.xtext.web.server.ISession;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import com.google.gson.Gson;
+import com.google.gson.JsonIOException;
+import com.google.gson.JsonParseException;
+
+import tools.refinery.language.web.xtext.server.ResponseHandler;
+import tools.refinery.language.web.xtext.server.ResponseHandlerException;
+import tools.refinery.language.web.xtext.server.TransactionExecutor;
+import tools.refinery.language.web.xtext.server.message.XtextWebRequest;
+import tools.refinery.language.web.xtext.server.message.XtextWebResponse;
+
+@WebSocket
+public class XtextWebSocket implements WriteCallback, ResponseHandler {
+        private static final Logger LOG = LoggerFactory.getLogger(XtextWebSocket.class);
+
+        private final Gson gson = new Gson();
+
+        private final TransactionExecutor executor;
+
+        private Session webSocketSession;
+
+        public XtextWebSocket(TransactionExecutor executor) {
+                this.executor = executor;
+                executor.setResponseHandler(this);
+        }
+
+        public XtextWebSocket(ISession session, IResourceServiceProvider.Registry resourceServiceProviderRegistry) {
+                this(new TransactionExecutor(session, resourceServiceProviderRegistry));
+        }
+
+        @OnWebSocketConnect
+        public void onConnect(Session webSocketSession) {
+                if (this.webSocketSession != null) {
+                        LOG.error("Websocket session onConnect when already connected");
+                        return;
+                }
+                LOG.debug("New websocket connection from {}", webSocketSession.getRemoteAddress());
+                this.webSocketSession = webSocketSession;
+        }
+
+        @OnWebSocketClose
+        public void onClose(int statusCode, String reason) {
+                executor.dispose();
+                if (webSocketSession == null) {
+                        return;
+                }
+                if (statusCode == StatusCode.NORMAL || statusCode == StatusCode.SHUTDOWN) {
+                        LOG.debug("{} closed connection normally: {}", webSocketSession.getRemoteAddress(), reason);
+                } else {
+                        LOG.warn("{} closed connection with status code {}: {}", webSocketSession.getRemoteAddress(), statusCode,
+                                        reason);
+                }
+                webSocketSession = null;
+        }
+
+        @OnWebSocketError
+        public void onError(Throwable error) {
+                if (webSocketSession == null) {
+                        return;
+                }
+                LOG.error("Internal websocket error in connection from" + webSocketSession.getRemoteAddress(), error);
+        }
+
+        @OnWebSocketMessage
+        public void onMessage(Reader reader) {
+                if (webSocketSession == null) {
+                        LOG.error("Trying to receive message when websocket is disconnected");
+                        return;
+                }
+                XtextWebRequest request;
+                try {
+                        request = gson.fromJson(reader, XtextWebRequest.class);
+                } catch (JsonIOException e) {
+                        LOG.error("Cannot read from websocket from" + webSocketSession.getRemoteAddress(), e);
+                        if (webSocketSession.isOpen()) {
+                                webSocketSession.close(StatusCode.SERVER_ERROR, "Cannot read payload");
+                        }
+                        return;
+                } catch (JsonParseException e) {
+                        LOG.warn("Malformed websocket request from" + webSocketSession.getRemoteAddress(), e);
+                        webSocketSession.close(XtextStatusCode.INVALID_JSON, "Invalid JSON payload");
+                        return;
+                }
+                try {
+                        executor.handleRequest(request);
+                } catch (ResponseHandlerException e) {
+                        LOG.warn("Cannot write websocket response", e);
+                        if (webSocketSession.isOpen()) {
+                                webSocketSession.close(StatusCode.SERVER_ERROR, "Cannot write response");
+                        }
+                }
+        }
+
+        @Override
+        public void onResponse(XtextWebResponse response) throws ResponseHandlerException {
+                if (webSocketSession == null) {
+                        throw new ResponseHandlerException("Trying to send message when websocket is disconnected");
+                }
+                var responseString = gson.toJson(response);
+                try {
+                        webSocketSession.getRemote().sendPartialString(responseString, true, this);
+                } catch (IOException e) {
+                        throw new ResponseHandlerException(
+                                        "Cannot initiaite async write to websocket " + webSocketSession.getRemoteAddress(), e);
+                }
+        }
+
+        @Override
+        public void writeFailed(Throwable x) {
+                if (webSocketSession == null) {
+                        LOG.error("Cannot complete async write to disconnected websocket", x);
+                        return;
+                }
+                LOG.warn("Cannot complete async write to websocket " + webSocketSession.getRemoteAddress(), x);
+        }
+}
diff --git a/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextWebSocketServlet.java b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextWebSocketServlet.java
new file mode 100644
index 00000000..942ca380
--- /dev/null
+++ b/subprojects/language-web/src/main/java/tools/refinery/language/web/xtext/servlet/XtextWebSocketServlet.java
@@ -0,0 +1,83 @@
+package tools.refinery.language.web.xtext.servlet;
+
+import java.io.IOException;
+import java.time.Duration;
+import java.util.Set;
+
+import org.eclipse.jetty.websocket.server.JettyServerUpgradeRequest;
+import org.eclipse.jetty.websocket.server.JettyServerUpgradeResponse;
+import org.eclipse.jetty.websocket.server.JettyWebSocketCreator;
+import org.eclipse.jetty.websocket.server.JettyWebSocketServlet;
+import org.eclipse.jetty.websocket.server.JettyWebSocketServletFactory;
+import org.eclipse.xtext.resource.IResourceServiceProvider;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import jakarta.servlet.ServletConfig;
+import jakarta.servlet.ServletException;
+
+public abstract class XtextWebSocketServlet extends JettyWebSocketServlet implements JettyWebSocketCreator {
+
+        private static final long serialVersionUID = -3772740838165122685L;
+
+        public static final String ALLOWED_ORIGINS_SEPARATOR = ";";
+
+        public static final String ALLOWED_ORIGINS_INIT_PARAM = "tools.refinery.language.web.xtext.XtextWebSocketServlet.allowedOrigin";
+
+        public static final String XTEXT_SUBPROTOCOL_V1 = "tools.refinery.language.web.xtext.v1";
+
+        /**
+         * Maximum message size should be large enough to upload a full model file.
+         */
+        private static final long MAX_FRAME_SIZE = 4L * 1024L * 1024L;
+
+        private static final Duration IDLE_TIMEOUT = Duration.ofSeconds(30);
+
+        private transient Logger log = LoggerFactory.getLogger(getClass());
+
+        private transient Set<String> allowedOrigins = null;
+
+        @Override
+        public void init(ServletConfig config) throws ServletException {
+                var allowedOriginsStr = config.getInitParameter(ALLOWED_ORIGINS_INIT_PARAM);
+                if (allowedOriginsStr == null) {
+                        log.warn("All WebSocket origins are allowed! This setting should not be used in production!");
+                } else {
+                        allowedOrigins = Set.of(allowedOriginsStr.split(ALLOWED_ORIGINS_SEPARATOR));
+                        log.info("Allowed origins: {}", allowedOrigins);
+                }
+                super.init(config);
+        }
+
+        @Override
+        protected void configure(JettyWebSocketServletFactory factory) {
+                factory.setMaxFrameSize(MAX_FRAME_SIZE);
+                factory.setIdleTimeout(IDLE_TIMEOUT);
+                factory.addMapping("/", this);
+        }
+
+        @Override
+        public Object createWebSocket(JettyServerUpgradeRequest req, JettyServerUpgradeResponse resp) {
+                if (allowedOrigins != null) {
+                        var origin = req.getOrigin();
+                        if (origin == null || !allowedOrigins.contains(origin.toLowerCase())) {
+                                log.error("Connection from {} from forbidden origin {}", req.getRemoteSocketAddress(), origin);
+                                try {
+                                        resp.sendForbidden("Origin not allowed");
+                                } catch (IOException e) {
+                                        log.error("Cannot send forbidden origin error", e);
+                                }
+                                return null;
+                        }
+                }
+                if (req.getSubProtocols().contains(XTEXT_SUBPROTOCOL_V1)) {
+                        resp.setAcceptedSubProtocol(XTEXT_SUBPROTOCOL_V1);
+                } else {
+                        log.error("None of the subprotocols {} offered by {} are supported", req.getSubProtocols(),
+                                        req.getRemoteSocketAddress());
+                        resp.setAcceptedSubProtocol(null);
+                }
+                var session = new SimpleSession();
+                return new XtextWebSocket(session, IResourceServiceProvider.Registry.INSTANCE);
+        }
+}
diff --git a/subprojects/language-web/src/test/java/tools/refinery/language/web/ProblemWebSocketServletIntegrationTest.java b/subprojects/language-web/src/test/java/tools/refinery/language/web/ProblemWebSocketServletIntegrationTest.java
new file mode 100644
index 00000000..a26ce040
--- /dev/null
+++ b/subprojects/language-web/src/test/java/tools/refinery/language/web/ProblemWebSocketServletIntegrationTest.java
@@ -0,0 +1,204 @@
+package tools.refinery.language.web;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.equalTo;
+import static org.hamcrest.Matchers.hasSize;
+import static org.hamcrest.Matchers.instanceOf;
+import static org.hamcrest.Matchers.startsWith;
+import static org.junit.jupiter.api.Assertions.assertThrows;
+
+import java.io.IOException;
+import java.net.InetSocketAddress;
+import java.net.URI;
+import java.util.concurrent.CompletableFuture;
+import java.util.concurrent.CompletionException;
+
+import org.eclipse.jetty.http.HttpHeader;
+import org.eclipse.jetty.http.HttpStatus;
+import org.eclipse.jetty.server.Server;
+import org.eclipse.jetty.servlet.ServletContextHandler;
+import org.eclipse.jetty.servlet.ServletHolder;
+import org.eclipse.jetty.websocket.api.Session;
+import org.eclipse.jetty.websocket.api.StatusCode;
+import org.eclipse.jetty.websocket.api.annotations.WebSocket;
+import org.eclipse.jetty.websocket.api.exceptions.UpgradeException;
+import org.eclipse.jetty.websocket.client.ClientUpgradeRequest;
+import org.eclipse.jetty.websocket.client.WebSocketClient;
+import org.eclipse.jetty.websocket.server.config.JettyWebSocketServletContainerInitializer;
+import org.eclipse.xtext.testing.GlobalRegistries;
+import org.eclipse.xtext.testing.GlobalRegistries.GlobalStateMemento;
+import org.junit.jupiter.api.AfterEach;
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+import org.junit.jupiter.params.ParameterizedTest;
+import org.junit.jupiter.params.provider.ValueSource;
+
+import tools.refinery.language.web.tests.WebSocketIntegrationTestClient;
+import tools.refinery.language.web.xtext.servlet.XtextStatusCode;
+import tools.refinery.language.web.xtext.servlet.XtextWebSocketServlet;
+
+class ProblemWebSocketServletIntegrationTest {
+        private static int SERVER_PORT = 28080;
+
+        private static String SERVLET_URI = "/xtext-service";
+
+        private GlobalStateMemento stateBeforeInjectorCreation;
+
+        private Server server;
+
+        private WebSocketClient client;
+
+        @BeforeEach
+        void beforeEach() throws Exception {
+                stateBeforeInjectorCreation = GlobalRegistries.makeCopyOfGlobalState();
+                client = new WebSocketClient();
+                client.start();
+        }
+
+        @AfterEach
+        void afterEach() throws Exception {
+                client.stop();
+                client = null;
+                if (server != null) {
+                        server.stop();
+                        server = null;
+                }
+                stateBeforeInjectorCreation.restoreGlobalState();
+                stateBeforeInjectorCreation = null;
+        }
+
+        @Test
+        void updateTest() {
+                startServer(null);
+                var clientSocket = new UpdateTestClient();
+                var session = connect(clientSocket, null, XtextWebSocketServlet.XTEXT_SUBPROTOCOL_V1);
+                assertThat(session.getUpgradeResponse().getAcceptedSubProtocol(),
+                                equalTo(XtextWebSocketServlet.XTEXT_SUBPROTOCOL_V1));
+                clientSocket.waitForTestResult();
+                assertThat(clientSocket.getCloseStatusCode(), equalTo(StatusCode.NORMAL));
+                var responses = clientSocket.getResponses();
+                assertThat(responses, hasSize(5));
+                assertThat(responses.get(0), equalTo("{\"id\":\"foo\",\"response\":{\"stateId\":\"-80000000\"}}"));
+                assertThat(responses.get(1), startsWith(
+                                "{\"resource\":\"test.problem\",\"stateId\":\"-80000000\",\"service\":\"highlight\",\"push\":{\"regions\":["));
+                assertThat(responses.get(2), equalTo(
+                                "{\"resource\":\"test.problem\",\"stateId\":\"-80000000\",\"service\":\"validate\",\"push\":{\"issues\":[]}}"));
+                assertThat(responses.get(3), equalTo("{\"id\":\"bar\",\"response\":{\"stateId\":\"-7fffffff\"}}"));
+                assertThat(responses.get(4), startsWith(
+                                "{\"resource\":\"test.problem\",\"stateId\":\"-7fffffff\",\"service\":\"highlight\",\"push\":{\"regions\":["));
+        }
+
+        @WebSocket
+        public static class UpdateTestClient extends WebSocketIntegrationTestClient {
+                @Override
+                protected void arrange(Session session, int responsesReceived) throws IOException {
+                        switch (responsesReceived) {
+                        case 0 -> session.getRemote().sendString(
+                                        "{\"id\":\"foo\",\"request\":{\"resource\":\"test.problem\",\"serviceType\":\"update\",\"fullText\":\"class Person.\n\"}}");
+                        case 3 -> session.getRemote().sendString(
+                                        "{\"id\":\"bar\",\"request\":{\"resource\":\"test.problem\",\"serviceType\":\"update\",\"requiredStateId\":\"-80000000\",\"deltaText\":\"indiv q.\nnode(q).\n\",\"deltaOffset\":\"0\",\"deltaReplaceLength\":\"0\"}}");
+                        case 5 -> session.close();
+                        }
+                }
+        }
+
+        @Test
+        void badSubProtocolTest() {
+                startServer(null);
+                var clientSocket = new CloseImmediatelyTestClient();
+                var session = connect(clientSocket, null, "<invalid sub-protocol>");
+                assertThat(session.getUpgradeResponse().getAcceptedSubProtocol(), equalTo(null));
+                clientSocket.waitForTestResult();
+                assertThat(clientSocket.getCloseStatusCode(), equalTo(StatusCode.NORMAL));
+        }
+
+        @WebSocket
+        public static class CloseImmediatelyTestClient extends WebSocketIntegrationTestClient {
+                @Override
+                protected void arrange(Session session, int responsesReceived) throws IOException {
+                        session.close();
+                }
+        }
+
+        @Test
+        void subProtocolNegotiationTest() {
+                startServer(null);
+                var clientSocket = new CloseImmediatelyTestClient();
+                var session = connect(clientSocket, null, "<invalid sub-protocol>", XtextWebSocketServlet.XTEXT_SUBPROTOCOL_V1);
+                assertThat(session.getUpgradeResponse().getAcceptedSubProtocol(),
+                                equalTo(XtextWebSocketServlet.XTEXT_SUBPROTOCOL_V1));
+                clientSocket.waitForTestResult();
+                assertThat(clientSocket.getCloseStatusCode(), equalTo(StatusCode.NORMAL));
+        }
+
+        @Test
+        void invalidJsonTest() {
+                startServer(null);
+                var clientSocket = new InvalidJsonTestClient();
+                connect(clientSocket, null, XtextWebSocketServlet.XTEXT_SUBPROTOCOL_V1);
+                clientSocket.waitForTestResult();
+                assertThat(clientSocket.getCloseStatusCode(), equalTo(XtextStatusCode.INVALID_JSON));
+        }
+
+        @WebSocket
+        public static class InvalidJsonTestClient extends WebSocketIntegrationTestClient {
+                @Override
+                protected void arrange(Session session, int responsesReceived) throws IOException {
+                        session.getRemote().sendString("<invalid json>");
+                }
+        }
+
+        @ParameterizedTest(name = "Origin: {0}")
+        @ValueSource(strings = { "https://refinery.example", "https://refinery.example:443", "HTTPS://REFINERY.EXAMPLE" })
+        void validOriginTest(String origin) {
+                startServer("https://refinery.example;https://refinery.example:443");
+                var clientSocket = new CloseImmediatelyTestClient();
+                connect(clientSocket, origin, XtextWebSocketServlet.XTEXT_SUBPROTOCOL_V1);
+                clientSocket.waitForTestResult();
+                assertThat(clientSocket.getCloseStatusCode(), equalTo(StatusCode.NORMAL));
+        }
+
+        @Test
+        void invalidOriginTest() {
+                startServer("https://refinery.example;https://refinery.example:443");
+                var clientSocket = new CloseImmediatelyTestClient();
+                var exception = assertThrows(CompletionException.class,
+                                () -> connect(clientSocket, "https://invalid.example", XtextWebSocketServlet.XTEXT_SUBPROTOCOL_V1));
+                var innerException = exception.getCause();
+                assertThat(innerException, instanceOf(UpgradeException.class));
+                assertThat(((UpgradeException) innerException).getResponseStatusCode(), equalTo(HttpStatus.FORBIDDEN_403));
+        }
+
+        private void startServer(String allowedOrigins) {
+                server = new Server(new InetSocketAddress(SERVER_PORT));
+                var handler = new ServletContextHandler();
+                var holder = new ServletHolder(ProblemWebSocketServlet.class);
+                if (allowedOrigins != null) {
+                        holder.setInitParameter(ProblemWebSocketServlet.ALLOWED_ORIGINS_INIT_PARAM, allowedOrigins);
+                }
+                handler.addServlet(holder, SERVLET_URI);
+                JettyWebSocketServletContainerInitializer.configure(handler, null);
+                server.setHandler(handler);
+                try {
+                        server.start();
+                } catch (Exception e) {
+                        throw new RuntimeException("Failed to start websocket server");
+                }
+        }
+
+        private Session connect(Object webSocketClient, String origin, String... subProtocols) {
+                var upgradeRequest = new ClientUpgradeRequest();
+                if (origin != null) {
+                        upgradeRequest.setHeader(HttpHeader.ORIGIN.name(), origin);
+                }
+                upgradeRequest.setSubProtocols(subProtocols);
+                CompletableFuture<Session> sessionFuture;
+                try {
+                        sessionFuture = client.connect(webSocketClient, URI.create("ws://localhost:" + SERVER_PORT + SERVLET_URI),
+                                        upgradeRequest);
+                } catch (IOException e) {
+                        throw new AssertionError("Unexpected exception while connection to websocket", e);
+                }
+                return sessionFuture.join();
+        }
+}
diff --git a/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/AwaitTerminationExecutorServiceProvider.java b/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/AwaitTerminationExecutorServiceProvider.java
new file mode 100644
index 00000000..b70d0ed5
--- /dev/null
+++ b/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/AwaitTerminationExecutorServiceProvider.java
@@ -0,0 +1,42 @@
+package tools.refinery.language.web.tests;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.concurrent.ExecutorService;
+
+import org.eclipse.xtext.ide.ExecutorServiceProvider;
+
+import com.google.inject.Singleton;
+
+@Singleton
+public class AwaitTerminationExecutorServiceProvider extends ExecutorServiceProvider {
+        private List<RestartableCachedThreadPool> servicesToShutDown = new ArrayList<>();
+
+        @Override
+        protected ExecutorService createInstance(String key) {
+                var instance = new RestartableCachedThreadPool();
+                synchronized (servicesToShutDown) {
+                        servicesToShutDown.add(instance);
+                }
+                return instance;
+        }
+
+        public void waitForAllTasksToFinish() {
+                synchronized (servicesToShutDown) {
+                        for (var executorService : servicesToShutDown) {
+                                executorService.waitForAllTasksToFinish();
+                        }
+                }
+        }
+
+        @Override
+        public void dispose() {
+                super.dispose();
+                synchronized (servicesToShutDown) {
+                        for (var executorService : servicesToShutDown) {
+                                executorService.waitForTermination();
+                        }
+                        servicesToShutDown.clear();
+                }
+        }
+}
diff --git a/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/ProblemWebInjectorProvider.java b/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/ProblemWebInjectorProvider.java
new file mode 100644
index 00000000..43c12faa
--- /dev/null
+++ b/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/ProblemWebInjectorProvider.java
@@ -0,0 +1,47 @@
+package tools.refinery.language.web.tests;
+
+import org.eclipse.xtext.ide.ExecutorServiceProvider;
+import org.eclipse.xtext.util.DisposableRegistry;
+import org.eclipse.xtext.util.Modules2;
+
+import com.google.inject.Guice;
+import com.google.inject.Injector;
+
+import tools.refinery.language.ide.ProblemIdeModule;
+import tools.refinery.language.tests.ProblemInjectorProvider;
+import tools.refinery.language.web.ProblemWebModule;
+import tools.refinery.language.web.ProblemWebSetup;
+
+public class ProblemWebInjectorProvider extends ProblemInjectorProvider {
+
+        protected Injector internalCreateInjector() {
+                return new ProblemWebSetup() {
+                        @Override
+                        public Injector createInjector() {
+                                return Guice.createInjector(
+                                                Modules2.mixin(createRuntimeModule(), new ProblemIdeModule(), createWebModule()));
+                        }
+                }.createInjectorAndDoEMFRegistration();
+        }
+
+        protected ProblemWebModule createWebModule() {
+                // Await termination of the executor service to avoid race conditions between
+                // the tasks in the service and the {@link
+                // org.eclipse.xtext.testing.extensions.InjectionExtension}.
+                return new ProblemWebModule() {
+                        @SuppressWarnings("unused")
+                        public Class<? extends ExecutorServiceProvider> bindExecutorServiceProvider() {
+                                return AwaitTerminationExecutorServiceProvider.class;
+                        }
+                };
+        }
+
+        @Override
+        public void restoreRegistry() {
+                // Also make sure to dispose any IDisposable instances (that may depend on the
+                // global state) created by Xtext before restoring the global state.
+                var disposableRegistry = getInjector().getInstance(DisposableRegistry.class);
+                disposableRegistry.dispose();
+                super.restoreRegistry();
+        }
+}
diff --git a/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/RestartableCachedThreadPool.java b/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/RestartableCachedThreadPool.java
new file mode 100644
index 00000000..1468273d
--- /dev/null
+++ b/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/RestartableCachedThreadPool.java
@@ -0,0 +1,109 @@
+package tools.refinery.language.web.tests;
+
+import java.util.Collection;
+import java.util.List;
+import java.util.concurrent.Callable;
+import java.util.concurrent.ExecutionException;
+import java.util.concurrent.ExecutorService;
+import java.util.concurrent.Executors;
+import java.util.concurrent.Future;
+import java.util.concurrent.TimeUnit;
+import java.util.concurrent.TimeoutException;
+
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+public class RestartableCachedThreadPool implements ExecutorService {
+        private static final Logger LOG = LoggerFactory.getLogger(RestartableCachedThreadPool.class);
+        
+        private ExecutorService delegate;
+
+        public RestartableCachedThreadPool() {
+                delegate = createExecutorService();
+        }
+        
+        public void waitForAllTasksToFinish() {
+                delegate.shutdown();
+                waitForTermination();
+                delegate = createExecutorService();
+        }
+        
+        public void waitForTermination() {
+                try {
+                        delegate.awaitTermination(1, TimeUnit.SECONDS);
+                } catch (InterruptedException e) {
+                        LOG.warn("Interrupted while waiting for delegate executor to stop", e);
+                }
+        }
+        
+        protected ExecutorService createExecutorService() {
+                return Executors.newCachedThreadPool();
+        }
+        
+        @Override
+        public boolean awaitTermination(long arg0, TimeUnit arg1) throws InterruptedException {
+                return delegate.awaitTermination(arg0, arg1);
+        }
+
+        @Override
+        public void execute(Runnable arg0) {
+                delegate.execute(arg0);
+        }
+
+        @Override
+        public <T> List<Future<T>> invokeAll(Collection<? extends Callable<T>> arg0, long arg1, TimeUnit arg2)
+                        throws InterruptedException {
+                return delegate.invokeAll(arg0, arg1, arg2);
+        }
+
+        @Override
+        public <T> List<Future<T>> invokeAll(Collection<? extends Callable<T>> arg0) throws InterruptedException {
+                return delegate.invokeAll(arg0);
+        }
+
+        @Override
+        public <T> T invokeAny(Collection<? extends Callable<T>> arg0, long arg1, TimeUnit arg2)
+                        throws InterruptedException, ExecutionException, TimeoutException {
+                return delegate.invokeAny(arg0, arg1, arg2);
+        }
+
+        @Override
+        public <T> T invokeAny(Collection<? extends Callable<T>> arg0) throws InterruptedException, ExecutionException {
+                return delegate.invokeAny(arg0);
+        }
+
+        @Override
+        public boolean isShutdown() {
+                return delegate.isShutdown();
+        }
+
+        @Override
+        public boolean isTerminated() {
+                return delegate.isTerminated();
+        }
+
+        @Override
+        public void shutdown() {
+                delegate.shutdown();
+        }
+
+        @Override
+        public List<Runnable> shutdownNow() {
+                return delegate.shutdownNow();
+        }
+
+        @Override
+        public <T> Future<T> submit(Callable<T> arg0) {
+                return delegate.submit(arg0);
+        }
+
+        @Override
+        public <T> Future<T> submit(Runnable arg0, T arg1) {
+                return delegate.submit(arg0, arg1);
+        }
+
+        @Override
+        public Future<?> submit(Runnable arg0) {
+                return delegate.submit(arg0);
+        }
+}
diff --git a/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/WebSocketIntegrationTestClient.java b/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/WebSocketIntegrationTestClient.java
new file mode 100644
index 00000000..49464d27
--- /dev/null
+++ b/subprojects/language-web/src/test/java/tools/refinery/language/web/tests/WebSocketIntegrationTestClient.java
@@ -0,0 +1,98 @@
+package tools.refinery.language.web.tests;
+
+import static org.junit.jupiter.api.Assertions.fail;
+
+import java.io.IOException;
+import java.time.Duration;
+import java.util.ArrayList;
+import java.util.List;
+
+import org.eclipse.jetty.websocket.api.Session;
+import org.eclipse.jetty.websocket.api.annotations.OnWebSocketClose;
+import org.eclipse.jetty.websocket.api.annotations.OnWebSocketConnect;
+import org.eclipse.jetty.websocket.api.annotations.OnWebSocketError;
+import org.eclipse.jetty.websocket.api.annotations.OnWebSocketMessage;
+
+public abstract class WebSocketIntegrationTestClient {
+        private static long TIMEOUT_MILLIS = Duration.ofSeconds(1).toMillis();
+        
+        private boolean finished = false;
+
+        private Object lock = new Object();
+
+        private Throwable error;
+
+        private int closeStatusCode;
+
+        private List<String> responses = new ArrayList<>();
+        
+        public int getCloseStatusCode() {
+                return closeStatusCode;
+        }
+        
+        public List<String> getResponses() {
+                return responses;
+        }
+
+        @OnWebSocketConnect
+        public void onConnect(Session session) {
+                arrangeAndCatchErrors(session);
+        }
+        
+        private void arrangeAndCatchErrors(Session session) {
+                try {
+                        arrange(session, responses.size());
+                } catch (Exception e) {
+                        finishedWithError(e);
+                }
+        }
+        
+        protected abstract void arrange(Session session, int responsesReceived) throws IOException; 
+
+        @OnWebSocketClose
+        public void onClose(int statusCode, String reason) {
+                closeStatusCode = statusCode;
+                testFinished();
+        }
+
+        @OnWebSocketError
+        public void onError(Throwable error) {
+                finishedWithError(error);
+        }
+
+        @OnWebSocketMessage
+        public void onMessage(Session session, String message) {
+                responses.add(message);
+                arrangeAndCatchErrors(session);
+        }
+
+        private void finishedWithError(Throwable t) {
+                error = t;
+                testFinished();
+        }
+
+        private void testFinished() {
+                synchronized (lock) {
+                        finished = true;
+                        lock.notify();
+                }
+        }
+
+        public void waitForTestResult() {
+                synchronized (lock) {
+                        if (!finished) {
+                                try {
+                                        lock.wait(TIMEOUT_MILLIS);
+                                } catch (InterruptedException e) {
+                                        fail("Unexpected InterruptedException", e);
+                                }
+                        }
+                }
+                if (!finished) {
+                        fail("Test still not finished after timeout");
+                }
+                if (error != null) {
+                        fail("Unexpected exception in websocket thread", error);
+                }
+        }
+}
diff --git a/subprojects/language-web/src/test/java/tools/refinery/language/web/xtext/servlet/TransactionExecutorTest.java b/subprojects/language-web/src/test/java/tools/refinery/language/web/xtext/servlet/TransactionExecutorTest.java
new file mode 100644
index 00000000..5b8fedba
--- /dev/null
+++ b/subprojects/language-web/src/test/java/tools/refinery/language/web/xtext/servlet/TransactionExecutorTest.java
@@ -0,0 +1,165 @@
+package tools.refinery.language.web.xtext.servlet;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.equalTo;
+import static org.hamcrest.Matchers.hasProperty;
+import static org.hamcrest.Matchers.instanceOf;
+import static org.mockito.Mockito.mock;
+import static org.mockito.Mockito.times;
+import static org.mockito.Mockito.verify;
+
+import java.util.List;
+import java.util.Map;
+
+import org.eclipse.emf.common.util.URI;
+import org.eclipse.xtext.resource.IResourceServiceProvider;
+import org.eclipse.xtext.testing.InjectWith;
+import org.eclipse.xtext.testing.extensions.InjectionExtension;
+import org.eclipse.xtext.web.server.model.DocumentStateResult;
+import org.eclipse.xtext.web.server.syntaxcoloring.HighlightingResult;
+import org.eclipse.xtext.web.server.validation.ValidationResult;
+import org.junit.jupiter.api.BeforeEach;
+import org.junit.jupiter.api.Test;
+import org.junit.jupiter.api.extension.ExtendWith;
+import org.mockito.ArgumentCaptor;
+import org.mockito.junit.jupiter.MockitoExtension;
+
+import com.google.inject.Inject;
+
+import tools.refinery.language.web.tests.AwaitTerminationExecutorServiceProvider;
+import tools.refinery.language.web.tests.ProblemWebInjectorProvider;
+import tools.refinery.language.web.xtext.server.ResponseHandler;
+import tools.refinery.language.web.xtext.server.ResponseHandlerException;
+import tools.refinery.language.web.xtext.server.TransactionExecutor;
+import tools.refinery.language.web.xtext.server.message.XtextWebOkResponse;
+import tools.refinery.language.web.xtext.server.message.XtextWebRequest;
+import tools.refinery.language.web.xtext.server.message.XtextWebResponse;
+
+@ExtendWith(MockitoExtension.class)
+@ExtendWith(InjectionExtension.class)
+@InjectWith(ProblemWebInjectorProvider.class)
+class TransactionExecutorTest {
+        private static final String RESOURCE_NAME = "test.problem";
+
+        private static final String PROBLEM_CONTENT_TYPE = "application/x-tools.refinery.problem";
+
+        private static final String TEST_PROBLEM = """
+                        class Person {
+                                Person[0..*] friend opposite friend
+                        }
+
+                        friend(a, b).
+                        """;
+
+        private static final Map<String, String> UPDATE_FULL_TEXT_PARAMS = Map.of("resource", RESOURCE_NAME, "serviceType",
+                        "update", "fullText", TEST_PROBLEM);
+
+        @Inject
+        private IResourceServiceProvider.Registry resourceServiceProviderRegistry;
+
+        @Inject
+        private AwaitTerminationExecutorServiceProvider executorServices;
+
+        private TransactionExecutor transactionExecutor;
+
+        @BeforeEach
+        void beforeEach() {
+                transactionExecutor = new TransactionExecutor(new SimpleSession(), resourceServiceProviderRegistry);
+        }
+
+        @Test
+        void updateFullTextTest() throws ResponseHandlerException {
+                var captor = newCaptor();
+                var stateId = updateFullText(captor);
+                assertThatPrecomputedMessagesAreReceived(stateId, captor.getAllValues());
+        }
+
+        @Test
+        void updateDeltaTextHighlightAndValidationChange() throws ResponseHandlerException {
+                var stateId = updateFullText();
+                var responseHandler = sendRequestAndWaitForAllResponses(
+                                new XtextWebRequest("bar", Map.of("resource", RESOURCE_NAME, "serviceType", "update", "requiredStateId",
+                                                stateId, "deltaText", "individual q.\nnode(q).\n<invalid text>\n", "deltaOffset", "0", "deltaReplaceLength", "0")));
+
+                var captor = newCaptor();
+                verify(responseHandler, times(3)).onResponse(captor.capture());
+                var newStateId = getStateId("bar", captor.getAllValues().get(0));
+                assertThatPrecomputedMessagesAreReceived(newStateId, captor.getAllValues());
+        }
+
+        @Test
+        void updateDeltaTextHighlightChangeOnly() throws ResponseHandlerException {
+                var stateId = updateFullText();
+                var responseHandler = sendRequestAndWaitForAllResponses(
+                                new XtextWebRequest("bar", Map.of("resource", RESOURCE_NAME, "serviceType", "update", "requiredStateId",
+                                                stateId, "deltaText", "indiv q.\nnode(q).\n", "deltaOffset", "0", "deltaReplaceLength", "0")));
+
+                var captor = newCaptor();
+                verify(responseHandler, times(2)).onResponse(captor.capture());
+                var newStateId = getStateId("bar", captor.getAllValues().get(0));
+                assertHighlightingResponse(newStateId, captor.getAllValues().get(1));
+        }
+
+        @Test
+        void fullTextWithoutResourceTest() throws ResponseHandlerException {
+                var resourceServiceProvider = resourceServiceProviderRegistry
+                                .getResourceServiceProvider(URI.createFileURI(RESOURCE_NAME));
+                resourceServiceProviderRegistry.getContentTypeToFactoryMap().put(PROBLEM_CONTENT_TYPE, resourceServiceProvider);
+                var responseHandler = sendRequestAndWaitForAllResponses(new XtextWebRequest("foo",
+                                Map.of("contentType", PROBLEM_CONTENT_TYPE, "fullText", TEST_PROBLEM, "serviceType", "validate")));
+
+                var captor = newCaptor();
+                verify(responseHandler).onResponse(captor.capture());
+                var response = captor.getValue();
+                assertThat(response, hasProperty("id", equalTo("foo")));
+                assertThat(response, hasProperty("responseData", instanceOf(ValidationResult.class)));
+        }
+
+        private ArgumentCaptor<XtextWebResponse> newCaptor() {
+                return ArgumentCaptor.forClass(XtextWebResponse.class);
+        }
+
+        private String updateFullText() throws ResponseHandlerException {
+                return updateFullText(newCaptor());
+        }
+
+        private String updateFullText(ArgumentCaptor<XtextWebResponse> captor) throws ResponseHandlerException {
+                var responseHandler = sendRequestAndWaitForAllResponses(new XtextWebRequest("foo", UPDATE_FULL_TEXT_PARAMS));
+
+                verify(responseHandler, times(3)).onResponse(captor.capture());
+                return getStateId("foo", captor.getAllValues().get(0));
+        }
+
+        private ResponseHandler sendRequestAndWaitForAllResponses(XtextWebRequest request) throws ResponseHandlerException {
+                var responseHandler = mock(ResponseHandler.class);
+                transactionExecutor.setResponseHandler(responseHandler);
+                transactionExecutor.handleRequest(request);
+                executorServices.waitForAllTasksToFinish();
+                return responseHandler;
+        }
+
+        private String getStateId(String requestId, XtextWebResponse okResponse) {
+                assertThat(okResponse, hasProperty("id", equalTo(requestId)));
+                assertThat(okResponse, hasProperty("responseData", instanceOf(DocumentStateResult.class)));
+                return ((DocumentStateResult) ((XtextWebOkResponse) okResponse).getResponseData()).getStateId();
+        }
+
+        private void assertThatPrecomputedMessagesAreReceived(String stateId, List<XtextWebResponse> responses) {
+                assertHighlightingResponse(stateId, responses.get(1));
+                assertValidationResponse(stateId, responses.get(2));
+        }
+
+        private void assertHighlightingResponse(String stateId, XtextWebResponse highlightingResponse) {
+                assertThat(highlightingResponse, hasProperty("resourceId", equalTo(RESOURCE_NAME)));
+                assertThat(highlightingResponse, hasProperty("stateId", equalTo(stateId)));
+                assertThat(highlightingResponse, hasProperty("service", equalTo("highlight")));
+                assertThat(highlightingResponse, hasProperty("pushData", instanceOf(HighlightingResult.class)));
+        }
+
+        private void assertValidationResponse(String stateId, XtextWebResponse validationResponse) {
+                assertThat(validationResponse, hasProperty("resourceId", equalTo(RESOURCE_NAME)));
+                assertThat(validationResponse, hasProperty("stateId", equalTo(stateId)));
+                assertThat(validationResponse, hasProperty("service", equalTo("validate")));
+                assertThat(validationResponse, hasProperty("pushData", instanceOf(ValidationResult.class)));
+        }
+}