Merge pull request #13 from kris7t/xtext-formatter

Xtext formatter support

18 files changed, 753 insertions, 372 deletions

diff --git a/language-web/package.json b/language-web/package.json
index 3362a47a..54aad155 100644
--- a/language-web/package.json
+++ b/language-web/package.json
@@ -95,6 +95,7 @@
     "mobx-react-lite": "^3.2.1",
     "nanoid": "^3.1.30",
     "react": "^17.0.2",
-    "react-dom": "^17.0.2"
+    "react-dom": "^17.0.2",
+    "zod": "^3.11.6"
   }
 }
diff --git a/language-web/src/main/js/editor/EditorButtons.tsx b/language-web/src/main/js/editor/EditorButtons.tsx
index 09ce33dd..150aa00d 100644
--- a/language-web/src/main/js/editor/EditorButtons.tsx
+++ b/language-web/src/main/js/editor/EditorButtons.tsx
@@ -7,6 +7,7 @@ import ToggleButtonGroup from '@mui/material/ToggleButtonGroup';
 import CheckIcon from '@mui/icons-material/Check';
 import ErrorIcon from '@mui/icons-material/Error';
 import FormatListNumberedIcon from '@mui/icons-material/FormatListNumbered';
+import FormatPaint from '@mui/icons-material/FormatPaint';
 import InfoOutlinedIcon from '@mui/icons-material/InfoOutlined';
 import RedoIcon from '@mui/icons-material/Redo';
 import SearchIcon from '@mui/icons-material/Search';
@@ -47,7 +48,6 @@ export const EditorButtons = observer(() => {
           disabled={!editorStore.canUndo}
           onClick={() => editorStore.undo()}
           aria-label="Undo"
-          value="undo"
         >
           <UndoIcon fontSize="small" />
         </IconButton>
@@ -55,7 +55,6 @@ export const EditorButtons = observer(() => {
           disabled={!editorStore.canRedo}
           onClick={() => editorStore.redo()}
           aria-label="Redo"
-          value="redo"
         >
           <RedoIcon fontSize="small" />
         </IconButton>
@@ -88,6 +87,12 @@ export const EditorButtons = observer(() => {
           {getLintIcon(editorStore.highestDiagnosticLevel)}
         </ToggleButton>
       </ToggleButtonGroup>
+      <IconButton
+        onClick={() => editorStore.formatText()}
+        aria-label="Automatic format"
+      >
+        <FormatPaint fontSize="small" />
+      </IconButton>
     </Stack>
   );
 });
diff --git a/language-web/src/main/js/editor/EditorStore.ts b/language-web/src/main/js/editor/EditorStore.ts
index 059233f4..5760de28 100644
--- a/language-web/src/main/js/editor/EditorStore.ts
+++ b/language-web/src/main/js/editor/EditorStore.ts
@@ -115,6 +115,7 @@ export class EditorStore {
         lineNumbers(),
         foldGutter(),
         keymap.of([
+          { key: 'Mod-Shift-f', run: () => this.formatText() },
           ...closeBracketsKeymap,
           ...commentKeymap,
           ...completionKeymap,
@@ -280,4 +281,9 @@ export class EditorStore {
   toggleLintPanel(): void {
     this.setLintPanelOpen(!this.showLintPanel);
   }
+
+  formatText(): boolean {
+    this.client.formatText();
+    return true;
+  }
 }
diff --git a/language-web/src/main/js/xtext/ContentAssistService.ts b/language-web/src/main/js/xtext/ContentAssistService.ts
index aa9a80b0..8b872e06 100644
--- a/language-web/src/main/js/xtext/ContentAssistService.ts
+++ b/language-web/src/main/js/xtext/ContentAssistService.ts
@@ -10,7 +10,7 @@ import escapeStringRegexp from 'escape-string-regexp';
 import { implicitCompletion } from '../language/props';
 import type { UpdateService } from './UpdateService';
 import { getLogger } from '../utils/logger';
-import type { IContentAssistEntry } from './xtextServiceResults';
+import type { ContentAssistEntry } from './xtextServiceResults';
 
 const PROPOSALS_LIMIT = 1000;
 
@@ -67,8 +67,8 @@ function computeSpan(prefix: string, entryCount: number): RegExp {
   return new RegExp(`^${escapedPrefix}$`);
 }
 
-function createCompletion(entry: IContentAssistEntry): Completion {
-  let boost;
+function createCompletion(entry: ContentAssistEntry): Completion {
+  let boost: number;
   switch (entry.kind) {
     case 'KEYWORD':
       // Some hard-to-type operators should be on top.
diff --git a/language-web/src/main/js/xtext/HighlightingService.ts b/language-web/src/main/js/xtext/HighlightingService.ts
index fc3e9e53..dfbb4a19 100644
--- a/language-web/src/main/js/xtext/HighlightingService.ts
+++ b/language-web/src/main/js/xtext/HighlightingService.ts
@@ -1,10 +1,7 @@
 import type { EditorStore } from '../editor/EditorStore';
 import type { IHighlightRange } from '../editor/semanticHighlighting';
 import type { UpdateService } from './UpdateService';
-import { getLogger } from '../utils/logger';
-import { isHighlightingResult } from './xtextServiceResults';
-
-const log = getLogger('xtext.ValidationService');
+import { highlightingResult } from './xtextServiceResults';
 
 export class HighlightingService {
   private readonly store: EditorStore;
@@ -17,13 +14,10 @@ export class HighlightingService {
   }
 
   onPush(push: unknown): void {
-    if (!isHighlightingResult(push)) {
-      log.error('Invalid highlighting result', push);
-      return;
-    }
+    const { regions } = highlightingResult.parse(push);
     const allChanges = this.updateService.computeChangesSinceLastUpdate();
     const ranges: IHighlightRange[] = [];
-    push.regions.forEach(({ offset, length, styleClasses }) => {
+    regions.forEach(({ offset, length, styleClasses }) => {
       if (styleClasses.length === 0) {
         return;
       }
diff --git a/language-web/src/main/js/xtext/OccurrencesService.ts b/language-web/src/main/js/xtext/OccurrencesService.ts
index d1dec9e9..bc865537 100644
--- a/language-web/src/main/js/xtext/OccurrencesService.ts
+++ b/language-web/src/main/js/xtext/OccurrencesService.ts
@@ -7,9 +7,9 @@ import { getLogger } from '../utils/logger';
 import { Timer } from '../utils/Timer';
 import { XtextWebSocketClient } from './XtextWebSocketClient';
 import {
-  isOccurrencesResult,
-  isServiceConflictResult,
-  ITextRegion,
+  isConflictResult,
+  occurrencesResult,
+  TextRegion,
 } from './xtextServiceResults';
 
 const FIND_OCCURRENCES_TIMEOUT_MS = 1000;
@@ -20,7 +20,7 @@ const CLEAR_OCCURRENCES_TIMEOUT_MS = 10;
 
 const log = getLogger('xtext.OccurrencesService');
 
-function transformOccurrences(regions: ITextRegion[]): IOccurrence[] {
+function transformOccurrences(regions: TextRegion[]): IOccurrence[] {
   const occurrences: IOccurrence[] = [];
   regions.forEach(({ offset, length }) => {
     if (length > 0) {
@@ -87,21 +87,32 @@ export class OccurrencesService {
       caretOffset: this.store.state.selection.main.head,
     });
     const allChanges = this.updateService.computeChangesSinceLastUpdate();
-    if (!allChanges.empty
-      || (isServiceConflictResult(result) && result.conflict === 'canceled')) {
+    if (!allChanges.empty || isConflictResult(result, 'canceled')) {
       // Stale occurrences result, the user already made some changes.
       // We can safely ignore the occurrences and schedule a new find occurrences call.
       this.clearOccurrences();
       this.findOccurrencesTimer.schedule();
       return;
     }
-    if (!isOccurrencesResult(result) || result.stateId !== this.updateService.xtextStateId) {
-      log.error('Unexpected occurrences result', result);
+    const parsedOccurrencesResult = occurrencesResult.safeParse(result);
+    if (!parsedOccurrencesResult.success) {
+      log.error(
+        'Unexpected occurences result',
+        result,
+        'not an OccurrencesResult: ',
+        parsedOccurrencesResult.error,
+      );
       this.clearOccurrences();
       return;
     }
-    const write = transformOccurrences(result.writeRegions);
-    const read = transformOccurrences(result.readRegions);
+    const { stateId, writeRegions, readRegions } = parsedOccurrencesResult.data;
+    if (stateId !== this.updateService.xtextStateId) {
+      log.error('Unexpected state id, expected:', this.updateService.xtextStateId, 'got:', stateId);
+      this.clearOccurrences();
+      return;
+    }
+    const write = transformOccurrences(writeRegions);
+    const read = transformOccurrences(readRegions);
     this.hasOccurrences = write.length > 0 || read.length > 0;
     log.debug('Found', write.length, 'write and', read.length, 'read occurrences');
     this.store.updateOccurrences(write, read);
diff --git a/language-web/src/main/js/xtext/UpdateService.ts b/language-web/src/main/js/xtext/UpdateService.ts
index 9b672e79..e78944a9 100644
--- a/language-web/src/main/js/xtext/UpdateService.ts
+++ b/language-web/src/main/js/xtext/UpdateService.ts
@@ -1,6 +1,8 @@
 import {
   ChangeDesc,
   ChangeSet,
+  ChangeSpec,
+  StateEffect,
   Transaction,
 } from '@codemirror/state';
 import { nanoid } from 'nanoid';
@@ -11,10 +13,11 @@ import { ConditionVariable } from '../utils/ConditionVariable';
 import { getLogger } from '../utils/logger';
 import { Timer } from '../utils/Timer';
 import {
-  IContentAssistEntry,
-  isContentAssistResult,
-  isDocumentStateResult,
-  isInvalidStateIdConflictResult,
+  ContentAssistEntry,
+  contentAssistResult,
+  documentStateResult,
+  formattingResult,
+  isConflictResult,
 } from './xtextServiceResults';
 
 const UPDATE_TIMEOUT_MS = 500;
@@ -23,6 +26,8 @@ const WAIT_FOR_UPDATE_TIMEOUT_MS = 1000;
 
 const log = getLogger('xtext.UpdateService');
 
+const setDirtyChanges = StateEffect.define<ChangeSet>();
+
 export interface IAbortSignal {
   aborted: boolean;
 }
@@ -38,12 +43,12 @@ export class UpdateService {
    * The changes being synchronized to the server if a full or delta text update is running,
    * `null` otherwise.
    */
-  private pendingUpdate: ChangeDesc | null = null;
+  private pendingUpdate: ChangeSet | null = null;
 
   /**
    * Local changes not yet sychronized to the server and not part of the running update, if any.
    */
-  private dirtyChanges: ChangeDesc;
+  private dirtyChanges: ChangeSet;
 
   private readonly webSocketClient: XtextWebSocketClient;
 
@@ -59,7 +64,7 @@ export class UpdateService {
   constructor(store: EditorStore, webSocketClient: XtextWebSocketClient) {
     this.resourceName = `${nanoid(7)}.problem`;
     this.store = store;
-    this.dirtyChanges = this.newEmptyChangeDesc();
+    this.dirtyChanges = this.newEmptyChangeSet();
     this.webSocketClient = webSocketClient;
   }
 
@@ -71,8 +76,19 @@ export class UpdateService {
   }
 
   onTransaction(transaction: Transaction): void {
+    const setDirtyChangesEffect = transaction.effects.find(
+      (effect) => effect.is(setDirtyChanges),
+    ) as StateEffect<ChangeSet> | undefined;
+    if (setDirtyChangesEffect) {
+      const { value } = setDirtyChangesEffect;
+      if (this.pendingUpdate !== null) {
+        this.pendingUpdate = ChangeSet.empty(value.length);
+      }
+      this.dirtyChanges = value;
+      return;
+    }
     if (transaction.docChanged) {
-      this.dirtyChanges = this.dirtyChanges.composeDesc(transaction.changes.desc);
+      this.dirtyChanges = this.dirtyChanges.compose(transaction.changes);
       this.idleUpdateTimer.reschedule();
     }
   }
@@ -86,7 +102,7 @@ export class UpdateService {
    * @return the summary of changes since the last update
    */
   computeChangesSinceLastUpdate(): ChangeDesc {
-    return this.pendingUpdate?.composeDesc(this.dirtyChanges) || this.dirtyChanges;
+    return this.pendingUpdate?.composeDesc(this.dirtyChanges.desc) || this.dirtyChanges.desc;
   }
 
   private handleIdleUpdate() {
@@ -101,9 +117,8 @@ export class UpdateService {
     this.idleUpdateTimer.reschedule();
   }
 
-  private newEmptyChangeDesc() {
-    const changeSet = ChangeSet.of([], this.store.state.doc.length);
-    return changeSet.desc;
+  private newEmptyChangeSet() {
+    return ChangeSet.of([], this.store.state.doc.length);
   }
 
   async updateFullText(): Promise<void> {
@@ -116,11 +131,8 @@ export class UpdateService {
       serviceType: 'update',
       fullText: this.store.state.doc.sliceString(0),
     });
-    if (isDocumentStateResult(result)) {
-      return [result.stateId, undefined];
-    }
-    log.error('Unexpected full text update result:', result);
-    throw new Error('Full text update failed');
+    const { stateId } = documentStateResult.parse(result);
+    return [stateId, undefined];
   }
 
   /**
@@ -146,14 +158,14 @@ export class UpdateService {
         requiredStateId: this.xtextStateId,
         ...delta,
       });
-      if (isDocumentStateResult(result)) {
-        return [result.stateId, undefined];
+      const parsedDocumentStateResult = documentStateResult.safeParse(result);
+      if (parsedDocumentStateResult.success) {
+        return [parsedDocumentStateResult.data.stateId, undefined];
       }
-      if (isInvalidStateIdConflictResult(result)) {
+      if (isConflictResult(result, 'invalidStateId')) {
         return this.doFallbackToUpdateFullText();
       }
-      log.error('Unexpected delta text update result:', result);
-      throw new Error('Delta text update failed');
+      throw parsedDocumentStateResult.error;
     });
   }
 
@@ -163,15 +175,15 @@ export class UpdateService {
     }
     log.warn('Delta update failed, performing full text update');
     this.xtextStateId = null;
-    this.pendingUpdate = this.pendingUpdate.composeDesc(this.dirtyChanges);
-    this.dirtyChanges = this.newEmptyChangeDesc();
+    this.pendingUpdate = this.pendingUpdate.compose(this.dirtyChanges);
+    this.dirtyChanges = this.newEmptyChangeSet();
     return this.doUpdateFullText();
   }
 
   async fetchContentAssist(
     params: Record<string, unknown>,
     signal: IAbortSignal,
-  ): Promise<IContentAssistEntry[]> {
+  ): Promise<ContentAssistEntry[]> {
     await this.prepareForDeltaUpdate();
     if (signal.aborted) {
       return [];
@@ -185,18 +197,20 @@ export class UpdateService {
           requiredStateId: this.xtextStateId,
           ...delta,
         });
-        if (isContentAssistResult(result)) {
-          return [result.stateId, result.entries];
+        const parsedContentAssistResult = contentAssistResult.safeParse(result);
+        if (parsedContentAssistResult.success) {
+          const { stateId, entries: resultEntries } = parsedContentAssistResult.data;
+          return [stateId, resultEntries];
         }
-        if (isInvalidStateIdConflictResult(result)) {
+        if (isConflictResult(result, 'invalidStateId')) {
+          log.warn('Server state invalid during content assist');
           const [newStateId] = await this.doFallbackToUpdateFullText();
           // We must finish this state update transaction to prepare for any push events
           // before querying for content assist, so we just return `null` and will query
           // the content assist service later.
           return [newStateId, null];
         }
-        log.error('Unextpected content assist result with delta update', result);
-        throw new Error('Unexpexted content assist result with delta update');
+        throw parsedContentAssistResult.error;
       });
       if (entries !== null) {
         return entries;
@@ -214,11 +228,36 @@ export class UpdateService {
       ...params,
       requiredStateId: expectedStateId,
     });
-    if (isContentAssistResult(result) && result.stateId === expectedStateId) {
-      return result.entries;
+    const { stateId, entries } = contentAssistResult.parse(result);
+    if (stateId !== expectedStateId) {
+      throw new Error(`Unexpected state id, expected: ${expectedStateId} got: ${stateId}`);
     }
-    log.error('Unexpected content assist result', result);
-    throw new Error('Unexpected content assist result');
+    return entries;
+  }
+
+  async formatText(): Promise<void> {
+    await this.update();
+    let { from, to } = this.store.state.selection.main;
+    if (to <= from) {
+      from = 0;
+      to = this.store.state.doc.length;
+    }
+    log.debug('Formatting from', from, 'to', to);
+    await this.withUpdate(async () => {
+      const result = await this.webSocketClient.send({
+        resource: this.resourceName,
+        serviceType: 'format',
+        selectionStart: from,
+        selectionEnd: to,
+      });
+      const { stateId, formattedText } = formattingResult.parse(result);
+      this.applyBeforeDirtyChanges({
+        from,
+        to,
+        insert: formattedText,
+      });
+      return [stateId, null];
+    });
   }
 
   private computeDelta() {
@@ -242,6 +281,20 @@ export class UpdateService {
     };
   }
 
+  private applyBeforeDirtyChanges(changeSpec: ChangeSpec) {
+    const pendingChanges = this.pendingUpdate?.compose(this.dirtyChanges) || this.dirtyChanges;
+    const revertChanges = pendingChanges.invert(this.store.state.doc);
+    const applyBefore = ChangeSet.of(changeSpec, revertChanges.newLength);
+    const redoChanges = pendingChanges.map(applyBefore.desc);
+    const changeSet = revertChanges.compose(applyBefore).compose(redoChanges);
+    this.store.dispatch({
+      changes: changeSet,
+      effects: [
+        setDirtyChanges.of(redoChanges),
+      ],
+    });
+  }
+
   /**
    * Executes an asynchronous callback that updates the state on the server.
    *
@@ -268,7 +321,7 @@ export class UpdateService {
       throw new Error('Another update is pending, will not perform update');
     }
     this.pendingUpdate = this.dirtyChanges;
-    this.dirtyChanges = this.newEmptyChangeDesc();
+    this.dirtyChanges = this.newEmptyChangeSet();
     let newStateId: string | null = null;
     try {
       let result: T;
@@ -282,7 +335,7 @@ export class UpdateService {
       if (this.pendingUpdate === null) {
         log.error('pendingUpdate was cleared during update');
       } else {
-        this.dirtyChanges = this.pendingUpdate.composeDesc(this.dirtyChanges);
+        this.dirtyChanges = this.pendingUpdate.compose(this.dirtyChanges);
       }
       this.pendingUpdate = null;
       this.webSocketClient.forceReconnectOnError();
diff --git a/language-web/src/main/js/xtext/ValidationService.ts b/language-web/src/main/js/xtext/ValidationService.ts
index 8e4934ac..c7f6ac7f 100644
--- a/language-web/src/main/js/xtext/ValidationService.ts
+++ b/language-web/src/main/js/xtext/ValidationService.ts
@@ -3,9 +3,7 @@ import type { Diagnostic } from '@codemirror/lint';
 import type { EditorStore } from '../editor/EditorStore';
 import type { UpdateService } from './UpdateService';
 import { getLogger } from '../utils/logger';
-import { isValidationResult } from './xtextServiceResults';
-
-const log = getLogger('xtext.ValidationService');
+import { validationResult } from './xtextServiceResults';
 
 export class ValidationService {
   private readonly store: EditorStore;
@@ -18,13 +16,10 @@ export class ValidationService {
   }
 
   onPush(push: unknown): void {
-    if (!isValidationResult(push)) {
-      log.error('Invalid validation result', push);
-      return;
-    }
+    const { issues } = validationResult.parse(push);
     const allChanges = this.updateService.computeChangesSinceLastUpdate();
     const diagnostics: Diagnostic[] = [];
-    push.issues.forEach(({
+    issues.forEach(({
       offset,
       length,
       severity,
diff --git a/language-web/src/main/js/xtext/XtextClient.ts b/language-web/src/main/js/xtext/XtextClient.ts
index 28f3d0cc..0898e725 100644
--- a/language-web/src/main/js/xtext/XtextClient.ts
+++ b/language-web/src/main/js/xtext/XtextClient.ts
@@ -12,6 +12,7 @@ import { UpdateService } from './UpdateService';
 import { getLogger } from '../utils/logger';
 import { ValidationService } from './ValidationService';
 import { XtextWebSocketClient } from './XtextWebSocketClient';
+import { XtextWebPushService } from './xtextMessages';
 
 const log = getLogger('xtext.XtextClient');
 
@@ -52,7 +53,7 @@ export class XtextClient {
     this.occurrencesService.onTransaction(transaction);
   }
 
-  private onPush(resource: string, stateId: string, service: string, push: unknown) {
+  private onPush(resource: string, stateId: string, service: XtextWebPushService, push: unknown) {
     const { resourceName, xtextStateId } = this.updateService;
     if (resource !== resourceName) {
       log.error('Unknown resource name: expected:', resourceName, 'got:', resource);
@@ -70,14 +71,16 @@ export class XtextClient {
         return;
       case 'validate':
         this.validationService.onPush(push);
-        return;
-      default:
-        log.error('Unknown push service:', service);
-        break;
     }
   }
 
   contentAssist(context: CompletionContext): Promise<CompletionResult> {
     return this.contentAssistService.contentAssist(context);
   }
+
+  formatText(): void {
+    this.updateService.formatText().catch((e) => {
+      log.error('Error while formatting text', e);
+    });
+  }
 }
diff --git a/language-web/src/main/js/xtext/XtextWebSocketClient.ts b/language-web/src/main/js/xtext/XtextWebSocketClient.ts
index 488e4b3b..2ce20a54 100644
--- a/language-web/src/main/js/xtext/XtextWebSocketClient.ts
+++ b/language-web/src/main/js/xtext/XtextWebSocketClient.ts
@@ -4,12 +4,13 @@ import { getLogger } from '../utils/logger';
 import { PendingTask } from '../utils/PendingTask';
 import { Timer } from '../utils/Timer';
 import {
-  isErrorResponse,
-  isOkResponse,
-  isPushMessage,
-  IXtextWebRequest,
+  xtextWebErrorResponse,
+  XtextWebRequest,
+  xtextWebOkResponse,
+  xtextWebPushMessage,
+  XtextWebPushService,
 } from './xtextMessages';
-import { isPongResult } from './xtextServiceResults';
+import { pongResult } from './xtextServiceResults';
 
 const XTEXT_SUBPROTOCOL_V1 = 'tools.refinery.language.web.xtext.v1';
 
@@ -32,7 +33,7 @@ export type ReconnectHandler = () => void;
 export type PushHandler = (
   resourceId: string,
   stateId: string,
-  service: string,
+  service: XtextWebPushService,
   data: unknown,
 ) => void;
 
@@ -192,11 +193,12 @@ export class XtextWebSocketClient {
     const ping = nanoid();
     log.trace('Ping', ping);
     this.send({ ping }).then((result) => {
-      if (isPongResult(result) && result.pong === ping) {
+      const parsedPongResult = pongResult.safeParse(result);
+      if (parsedPongResult.success && parsedPongResult.data.pong === ping) {
         log.trace('Pong', ping);
         this.pingTimer.schedule();
       } else {
-        log.error('Invalid pong');
+        log.error('Invalid pong:', parsedPongResult, 'expected:', ping);
         this.forceReconnectOnError();
       }
     }).catch((error) => {
@@ -222,7 +224,7 @@ export class XtextWebSocketClient {
     const message = JSON.stringify({
       id: messageId,
       request,
-    } as IXtextWebRequest);
+    } as XtextWebRequest);
     log.trace('Sending message', message);
     return new Promise((resolve, reject) => {
       const task = new PendingTask(resolve, reject, REQUEST_TIMEOUT_MS, () => {
@@ -248,23 +250,42 @@ export class XtextWebSocketClient {
       this.forceReconnectOnError();
       return;
     }
-    if (isOkResponse(message)) {
-      this.resolveRequest(message.id, message.response);
-    } else if (isErrorResponse(message)) {
-      this.rejectRequest(message.id, new Error(`${message.error} error: ${message.message}`));
-      if (message.error === 'server') {
-        log.error('Reconnecting due to server error: ', message.message);
+    const okResponse = xtextWebOkResponse.safeParse(message);
+    if (okResponse.success) {
+      const { id, response } = okResponse.data;
+      this.resolveRequest(id, response);
+      return;
+    }
+    const errorResponse = xtextWebErrorResponse.safeParse(message);
+    if (errorResponse.success) {
+      const { id, error, message: errorMessage } = errorResponse.data;
+      this.rejectRequest(id, new Error(`${error} error: ${errorMessage}`));
+      if (error === 'server') {
+        log.error('Reconnecting due to server error: ', errorMessage);
         this.forceReconnectOnError();
       }
-    } else if (isPushMessage(message)) {
-      this.onPush(
-        message.resource,
-        message.stateId,
-        message.service,
-        message.push,
-      );
+      return;
+    }
+    const pushMessage = xtextWebPushMessage.safeParse(message);
+    if (pushMessage.success) {
+      const {
+        resource,
+        stateId,
+        service,
+        push,
+      } = pushMessage.data;
+      this.onPush(resource, stateId, service, push);
     } else {
-      log.error('Unexpected websocket message', message);
+      log.error(
+        'Unexpected websocket message:',
+        message,
+        'not ok response because:',
+        okResponse.error,
+        'not error response because:',
+        errorResponse.error,
+        'not push message because:',
+        pushMessage.error,
+      );
       this.forceReconnectOnError();
     }
   }
diff --git a/language-web/src/main/js/xtext/xtextMessages.ts b/language-web/src/main/js/xtext/xtextMessages.ts
index 68737958..c4305fcf 100644
--- a/language-web/src/main/js/xtext/xtextMessages.ts
+++ b/language-web/src/main/js/xtext/xtextMessages.ts
@@ -1,62 +1,40 @@
-export interface IXtextWebRequest {
-  id: string;
+import { z } from 'zod';
 
-  request: unknown;
-}
+export const xtextWebRequest = z.object({
+  id: z.string().nonempty(),
+  request: z.unknown(),
+});
 
-export interface IXtextWebOkResponse {
-  id: string;
+export type XtextWebRequest = z.infer<typeof xtextWebRequest>;
 
-  response: unknown;
-}
+export const xtextWebOkResponse = z.object({
+  id: z.string().nonempty(),
+  response: z.unknown(),
+});
 
-export function isOkResponse(response: unknown): response is IXtextWebOkResponse {
-  const okResponse = response as IXtextWebOkResponse;
-  return typeof okResponse === 'object'
-    && typeof okResponse.id === 'string'
-    && typeof okResponse.response !== 'undefined';
-}
+export type XtextWebOkResponse = z.infer<typeof xtextWebOkResponse>;
 
-export const VALID_XTEXT_WEB_ERROR_KINDS = ['request', 'server'] as const;
+export const xtextWebErrorKind = z.enum(['request', 'server']);
 
-export type XtextWebErrorKind = typeof VALID_XTEXT_WEB_ERROR_KINDS[number];
+export type XtextWebErrorKind = z.infer<typeof xtextWebErrorKind>;
 
-export function isXtextWebErrorKind(value: unknown): value is XtextWebErrorKind {
-  return typeof value === 'string'
-    && VALID_XTEXT_WEB_ERROR_KINDS.includes(value as XtextWebErrorKind);
-}
+export const xtextWebErrorResponse = z.object({
+  id: z.string().nonempty(),
+  error: xtextWebErrorKind,
+  message: z.string(),
+});
 
-export interface IXtextWebErrorResponse {
-  id: string;
+export type XtextWebErrorResponse = z.infer<typeof xtextWebErrorResponse>;
 
-  error: XtextWebErrorKind;
+export const xtextWebPushService = z.enum(['highlight', 'validate']);
 
-  message: string;
-}
+export type XtextWebPushService = z.infer<typeof xtextWebPushService>;
 
-export function isErrorResponse(response: unknown): response is IXtextWebErrorResponse {
-  const errorResponse = response as IXtextWebErrorResponse;
-  return typeof errorResponse === 'object'
-    && typeof errorResponse.id === 'string'
-    && isXtextWebErrorKind(errorResponse.error)
-    && typeof errorResponse.message === 'string';
-}
+export const xtextWebPushMessage = z.object({
+  resource: z.string().nonempty(),
+  stateId: z.string().nonempty(),
+  service: xtextWebPushService,
+  push: z.unknown(),
+});
 
-export interface IXtextWebPushMessage {
-  resource: string;
-
-  stateId: string;
-
-  service: string;
-
-  push: unknown;
-}
-
-export function isPushMessage(response: unknown): response is IXtextWebPushMessage {
-  const pushMessage = response as IXtextWebPushMessage;
-  return typeof pushMessage === 'object'
-    && typeof pushMessage.resource === 'string'
-    && typeof pushMessage.stateId === 'string'
-    && typeof pushMessage.service === 'string'
-    && typeof pushMessage.push !== 'undefined';
-}
+export type XtextWebPushMessage = z.infer<typeof xtextWebPushMessage>;
diff --git a/language-web/src/main/js/xtext/xtextServiceResults.ts b/language-web/src/main/js/xtext/xtextServiceResults.ts
index b2de1e4a..f79b059c 100644
--- a/language-web/src/main/js/xtext/xtextServiceResults.ts
+++ b/language-web/src/main/js/xtext/xtextServiceResults.ts
@@ -1,239 +1,112 @@
-export interface IPongResult {
-  pong: string;
-}
-
-export function isPongResult(result: unknown): result is IPongResult {
-  const pongResult = result as IPongResult;
-  return typeof pongResult === 'object'
-    && typeof pongResult.pong === 'string';
-}
-
-export interface IDocumentStateResult {
-  stateId: string;
-}
-
-export function isDocumentStateResult(result: unknown): result is IDocumentStateResult {
-  const documentStateResult = result as IDocumentStateResult;
-  return typeof documentStateResult === 'object'
-    && typeof documentStateResult.stateId === 'string';
-}
-
-export const VALID_CONFLICTS = ['invalidStateId', 'canceled'] as const;
-
-export type Conflict = typeof VALID_CONFLICTS[number];
-
-export function isConflict(value: unknown): value is Conflict {
-  return typeof value === 'string' && VALID_CONFLICTS.includes(value as Conflict);
-}
-
-export interface IServiceConflictResult {
-  conflict: Conflict;
-}
-
-export function isServiceConflictResult(result: unknown): result is IServiceConflictResult {
-  const serviceConflictResult = result as IServiceConflictResult;
-  return typeof serviceConflictResult === 'object'
-    && isConflict(serviceConflictResult.conflict);
-}
-
-export function isInvalidStateIdConflictResult(result: unknown): boolean {
-  return isServiceConflictResult(result) && result.conflict === 'invalidStateId';
-}
-
-export const VALID_SEVERITIES = ['error', 'warning', 'info', 'ignore'] as const;
-
-export type Severity = typeof VALID_SEVERITIES[number];
-
-export function isSeverity(value: unknown): value is Severity {
-  return typeof value === 'string' && VALID_SEVERITIES.includes(value as Severity);
-}
-
-export interface IIssue {
-  description: string;
-
-  severity: Severity;
-
-  line: number;
-
-  column: number;
-
-  offset: number;
+import { z } from 'zod';
 
-  length: number;
-}
+export const pongResult = z.object({
+  pong: z.string().nonempty(),
+});
 
-export function isIssue(value: unknown): value is IIssue {
-  const issue = value as IIssue;
-  return typeof issue === 'object'
-    && typeof issue.description === 'string'
-    && isSeverity(issue.severity)
-    && typeof issue.line === 'number'
-    && typeof issue.column === 'number'
-    && typeof issue.offset === 'number'
-    && typeof issue.length === 'number';
-}
+export type PongResult = z.infer<typeof pongResult>;
 
-export interface IValidationResult {
-  issues: IIssue[];
-}
+export const documentStateResult = z.object({
+  stateId: z.string().nonempty(),
+});
 
-function isArrayOfType<T>(value: unknown, check: (entry: unknown) => entry is T): value is T[] {
-  return Array.isArray(value) && (value as T[]).every(check);
-}
+export type DocumentStateResult = z.infer<typeof documentStateResult>;
 
-export function isValidationResult(result: unknown): result is IValidationResult {
-  const validationResult = result as IValidationResult;
-  return typeof validationResult === 'object'
-    && isArrayOfType(validationResult.issues, isIssue);
-}
-
-export interface IReplaceRegion {
-  offset: number;
+export const conflict = z.enum(['invalidStateId', 'canceled']);
 
-  length: number;
+export type Conflict = z.infer<typeof conflict>;
 
-  text: string;
-}
+export const serviceConflictResult = z.object({
+  conflict,
+});
 
-export function isReplaceRegion(value: unknown): value is IReplaceRegion {
-  const replaceRegion = value as IReplaceRegion;
-  return typeof replaceRegion === 'object'
-    && typeof replaceRegion.offset === 'number'
-    && typeof replaceRegion.length === 'number'
-    && typeof replaceRegion.text === 'string';
-}
-
-export interface ITextRegion {
-  offset: number;
-
-  length: number;
-}
-
-export function isTextRegion(value: unknown): value is ITextRegion {
-  const textRegion = value as ITextRegion;
-  return typeof textRegion === 'object'
-    && typeof textRegion.offset === 'number'
-    && typeof textRegion.length === 'number';
-}
+export type ServiceConflictResult = z.infer<typeof serviceConflictResult>;
 
-export const VALID_XTEXT_CONTENT_ASSIST_ENTRY_KINDS = [
-  'TEXT',
-  'METHOD',
-  'FUNCTION',
-  'CONSTRUCTOR',
-  'FIELD',
-  'VARIABLE',
-  'CLASS',
-  'INTERFACE',
-  'MODULE',
-  'PROPERTY',
-  'UNIT',
-  'VALUE',
-  'ENUM',
-  'KEYWORD',
-  'SNIPPET',
-  'COLOR',
-  'FILE',
-  'REFERENCE',
-  'UNKNOWN',
-] as const;
-
-export type XtextContentAssistEntryKind = typeof VALID_XTEXT_CONTENT_ASSIST_ENTRY_KINDS[number];
-
-export function isXtextContentAssistEntryKind(
-  value: unknown,
-): value is XtextContentAssistEntryKind {
-  return typeof value === 'string'
-    && VALID_XTEXT_CONTENT_ASSIST_ENTRY_KINDS.includes(value as XtextContentAssistEntryKind);
+export function isConflictResult(result: unknown, conflictType: Conflict): boolean {
+  const parsedConflictResult = serviceConflictResult.safeParse(result);
+  return parsedConflictResult.success && parsedConflictResult.data.conflict === conflictType;
 }
 
-export interface IContentAssistEntry {
-  prefix: string;
+export const severity = z.enum(['error', 'warning', 'info', 'ignore']);
 
-  proposal: string;
+export type Severity = z.infer<typeof severity>;
 
-  label?: string;
+export const issue = z.object({
+  description: z.string().nonempty(),
+  severity,
+  line: z.number().int(),
+  column: z.number().int().nonnegative(),
+  offset: z.number().int().nonnegative(),
+  length: z.number().int().nonnegative(),
+});
 
-  description?: string;
+export type Issue = z.infer<typeof issue>;
 
-  documentation?: string;
+export const validationResult = z.object({
+  issues: issue.array(),
+});
 
-  escapePosition?: number;
+export type ValidationResult = z.infer<typeof validationResult>;
 
-  textReplacements: IReplaceRegion[];
+export const replaceRegion = z.object({
+  offset: z.number().int().nonnegative(),
+  length: z.number().int().nonnegative(),
+  text: z.string(),
+});
 
-  editPositions: ITextRegion[];
+export type ReplaceRegion = z.infer<typeof replaceRegion>;
 
-  kind: XtextContentAssistEntryKind | string;
-}
+export const textRegion = z.object({
+  offset: z.number().int().nonnegative(),
+  length: z.number().int().nonnegative(),
+});
 
-function isStringOrUndefined(value: unknown): value is string | undefined {
-  return typeof value === 'string' || typeof value === 'undefined';
-}
+export type TextRegion = z.infer<typeof textRegion>;
 
-function isNumberOrUndefined(value: unknown): value is number | undefined {
-  return typeof value === 'number' || typeof value === 'undefined';
-}
+export const contentAssistEntry = z.object({
+  prefix: z.string(),
+  proposal: z.string().nonempty(),
+  label: z.string().optional(),
+  description: z.string().nonempty().optional(),
+  documentation: z.string().nonempty().optional(),
+  escapePosition: z.number().int().nonnegative().optional(),
+  textReplacements: replaceRegion.array(),
+  editPositions: textRegion.array(),
+  kind: z.string().nonempty(),
+});
 
-export function isContentAssistEntry(value: unknown): value is IContentAssistEntry {
-  const entry = value as IContentAssistEntry;
-  return typeof entry === 'object'
-    && typeof entry.prefix === 'string'
-    && typeof entry.proposal === 'string'
-    && isStringOrUndefined(entry.label)
-    && isStringOrUndefined(entry.description)
-    && isStringOrUndefined(entry.documentation)
-    && isNumberOrUndefined(entry.escapePosition)
-    && isArrayOfType(entry.textReplacements, isReplaceRegion)
-    && isArrayOfType(entry.editPositions, isTextRegion)
-    && typeof entry.kind === 'string';
-}
+export type ContentAssistEntry = z.infer<typeof contentAssistEntry>;
 
-export interface IContentAssistResult extends IDocumentStateResult {
-  entries: IContentAssistEntry[];
-}
+export const contentAssistResult = documentStateResult.extend({
+  entries: contentAssistEntry.array(),
+});
 
-export function isContentAssistResult(result: unknown): result is IContentAssistResult {
-  const contentAssistResult = result as IContentAssistResult;
-  return isDocumentStateResult(result)
-    && isArrayOfType(contentAssistResult.entries, isContentAssistEntry);
-}
+export type ContentAssistResult = z.infer<typeof contentAssistResult>;
 
-export interface IHighlightingRegion {
-  offset: number;
+export const highlightingRegion = z.object({
+  offset: z.number().int().nonnegative(),
+  length: z.number().int().nonnegative(),
+  styleClasses: z.string().nonempty().array(),
+});
 
-  length: number;
+export type HighlightingRegion = z.infer<typeof highlightingRegion>;
 
-  styleClasses: string[];
-}
+export const highlightingResult = z.object({
+  regions: highlightingRegion.array(),
+});
 
-export function isHighlightingRegion(value: unknown): value is IHighlightingRegion {
-  const region = value as IHighlightingRegion;
-  return typeof region === 'object'
-    && typeof region.offset === 'number'
-    && typeof region.length === 'number'
-    && isArrayOfType(region.styleClasses, (s): s is string => typeof s === 'string');
-}
-
-export interface IHighlightingResult {
-  regions: IHighlightingRegion[];
-}
+export type HighlightingResult = z.infer<typeof highlightingResult>;
 
-export function isHighlightingResult(result: unknown): result is IHighlightingResult {
-  const highlightingResult = result as IHighlightingResult;
-  return typeof highlightingResult === 'object'
-    && isArrayOfType(highlightingResult.regions, isHighlightingRegion);
-}
+export const occurrencesResult = documentStateResult.extend({
+  writeRegions: textRegion.array(),
+  readRegions: textRegion.array(),
+});
 
-export interface IOccurrencesResult extends IDocumentStateResult {
-  writeRegions: ITextRegion[];
+export type OccurrencesResult = z.infer<typeof occurrencesResult>;
 
-  readRegions: ITextRegion[];
-}
+export const formattingResult = documentStateResult.extend({
+  formattedText: z.string(),
+  replaceRegion: textRegion,
+});
 
-export function isOccurrencesResult(result: unknown): result is IOccurrencesResult {
-  const occurrencesResult = result as IOccurrencesResult;
-  return isDocumentStateResult(occurrencesResult)
-    && isArrayOfType(occurrencesResult.writeRegions, isTextRegion)
-    && isArrayOfType(occurrencesResult.readRegions, isTextRegion);
-}
+export type FormattingResult = z.infer<typeof formattingResult>;
diff --git a/language-web/yarn.lock b/language-web/yarn.lock
index 06b30508..ebebe1ff 100644
--- a/language-web/yarn.lock
+++ b/language-web/yarn.lock
@@ -7784,3 +7784,8 @@ yocto-queue@^0.1.0:
   version "0.1.0"
   resolved "https://registry.yarnpkg.com/yocto-queue/-/yocto-queue-0.1.0.tgz#0294eb3dee05028d31ee1a5fa2c556a6aaf10a1b"
   integrity sha512-rVksvsnNCdJ/ohGc6xgPwyN8eheCxsiLM8mxuE/t/mOVqJewPuO1miLpTHQiRgTKCLexL4MeAFVagts7HmNZ2Q==
+
+zod@^3.11.6:
+  version "3.11.6"
+  resolved "https://registry.yarnpkg.com/zod/-/zod-3.11.6.tgz#e43a5e0c213ae2e02aefe7cb2b1a6fa3d7f1f483"
+  integrity sha512-daZ80A81I3/9lIydI44motWe6n59kRBfNzTuS2bfzVh1nAXi667TOTWWtatxyG+fwgNUiagSj/CWZwRRbevJIg==
diff --git a/language/src/main/java/tools/refinery/language/GenerateProblem.mwe2 b/language/src/main/java/tools/refinery/language/GenerateProblem.mwe2
index 58620d6a..0d934b68 100644
--- a/language/src/main/java/tools/refinery/language/GenerateProblem.mwe2
+++ b/language/src/main/java/tools/refinery/language/GenerateProblem.mwe2
@@ -39,6 +39,9 @@ Workflow {
                         serializer = {
                                 generateStub = false
                         }
+                        formatter = {
+                                generateStub = true
+                        }
                         validator = {
                                 generateDeprecationValidation = true
                         }
diff --git a/language/src/main/java/tools/refinery/language/Problem.xtext b/language/src/main/java/tools/refinery/language/Problem.xtext
index 26773047..c94d40ab 100644
--- a/language/src/main/java/tools/refinery/language/Problem.xtext
+++ b/language/src/main/java/tools/refinery/language/Problem.xtext
@@ -8,7 +8,8 @@ Problem:
         statements+=Statement*;
 
 Statement:
-        ClassDeclaration | EnumDeclaration | PredicateDefinition | RuleDefinition | Assertion | NodeValueAssertion | ScopeDeclaration |
+        ClassDeclaration | EnumDeclaration | PredicateDefinition | RuleDefinition | Assertion | NodeValueAssertion |
+        ScopeDeclaration |
         IndividualDeclaration;
 
 ClassDeclaration:
@@ -67,7 +68,7 @@ Literal:
 
 ValueLiteral:
         atom=Atom
-        (refinement?=":"|"=")
+        (refinement?=":" | "=")
         values+=LogicConstant ("|" values+=LogicConstant)*;
 
 NegativeLiteral:
@@ -78,7 +79,7 @@ ActionLiteral:
 
 ValueActionLiteral:
         atom=Atom
-        (refinement?=":"|"=")
+        (refinement?=":" | "=")
         value=LogicValue;
 
 DeleteActionLiteral:
@@ -86,7 +87,7 @@ DeleteActionLiteral:
 
 NewActionLiteral:
         "new" variable=NewVariable;
-        
+
 NewVariable:
         name=Identifier;
 
diff --git a/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java b/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java
new file mode 100644
index 00000000..903347f7
--- /dev/null
+++ b/language/src/main/java/tools/refinery/language/formatting2/ProblemFormatter.java
@@ -0,0 +1,183 @@
+/*
+ * generated by Xtext 2.26.0.M2
+ */
+package tools.refinery.language.formatting2;
+
+import org.eclipse.emf.ecore.EObject;
+import org.eclipse.xtext.formatting2.AbstractJavaFormatter;
+import org.eclipse.xtext.formatting2.IFormattableDocument;
+import org.eclipse.xtext.formatting2.IHiddenRegionFormatter;
+import org.eclipse.xtext.formatting2.regionaccess.ISemanticRegionsFinder;
+import org.eclipse.xtext.formatting2.regionaccess.ISequentialRegion;
+import org.eclipse.xtext.xbase.lib.Procedures.Procedure1;
+
+import tools.refinery.language.model.problem.Assertion;
+import tools.refinery.language.model.problem.Atom;
+import tools.refinery.language.model.problem.ClassDeclaration;
+import tools.refinery.language.model.problem.Conjunction;
+import tools.refinery.language.model.problem.IndividualDeclaration;
+import tools.refinery.language.model.problem.NegativeLiteral;
+import tools.refinery.language.model.problem.Parameter;
+import tools.refinery.language.model.problem.PredicateDefinition;
+import tools.refinery.language.model.problem.Problem;
+import tools.refinery.language.model.problem.ProblemPackage;
+
+public class ProblemFormatter extends AbstractJavaFormatter {
+
+        protected void format(Problem problem, IFormattableDocument doc) {
+                doc.prepend(problem, this::noSpace);
+                var region = regionFor(problem);
+                doc.append(region.keyword("problem"), this::oneSpace);
+                doc.prepend(region.keyword("."), this::noSpace);
+                appendNewLines(doc, region.keyword("."), this::twoNewLines);
+                for (var statement : problem.getStatements()) {
+                        doc.format(statement);
+                }
+        }
+
+        protected void format(Assertion assertion, IFormattableDocument doc) {
+                surroundNewLines(doc, assertion, this::singleNewLine);
+                var region = regionFor(assertion);
+                doc.append(region.feature(ProblemPackage.Literals.ASSERTION__DEFAULT), this::oneSpace);
+                doc.append(region.feature(ProblemPackage.Literals.ASSERTION__VALUE), this::noSpace);
+                doc.append(region.feature(ProblemPackage.Literals.ASSERTION__RELATION), this::noSpace);
+                formatParenthesizedList(region, doc);
+                doc.prepend(region.keyword(":"), this::noSpace);
+                doc.append(region.keyword(":"), this::oneSpace);
+                doc.prepend(region.keyword("."), this::noSpace);
+                for (var argument : assertion.getArguments()) {
+                        doc.format(argument);
+                }
+        }
+        
+        protected void format(ClassDeclaration classDeclaration, IFormattableDocument doc) {
+                surroundNewLines(doc, classDeclaration, this::twoNewLines);
+                var region = regionFor(classDeclaration);
+                doc.append(region.feature(ProblemPackage.Literals.CLASS_DECLARATION__ABSTRACT), this::oneSpace);
+                doc.append(region.keyword("class"), this::oneSpace);
+                doc.surround(region.keyword("extends"), this::oneSpace);
+                formatList(region, ",", doc);
+                doc.prepend(region.keyword("{"), this::oneSpace);
+                doc.append(region.keyword("{"), it -> it.setNewLines(1, 1, 2));
+                doc.prepend(region.keyword("}"), it -> it.setNewLines(1, 1, 2));
+                doc.prepend(region.keyword("."), this::noSpace);
+                for (var referenceDeclaration : classDeclaration.getReferenceDeclarations()) {
+                        doc.format(referenceDeclaration);
+                }
+        }
+
+        protected void format(PredicateDefinition predicateDefinition, IFormattableDocument doc) {
+                surroundNewLines(doc, predicateDefinition, this::twoNewLines);
+                var region = regionFor(predicateDefinition);
+                doc.append(region.feature(ProblemPackage.Literals.PREDICATE_DEFINITION__KIND), this::oneSpace);
+                doc.append(region.keyword("pred"), this::oneSpace);
+                doc.append(region.feature(ProblemPackage.Literals.NAMED_ELEMENT__NAME), this::noSpace);
+                formatParenthesizedList(region, doc);
+                doc.surround(region.keyword("<->"), this::oneSpace);
+                formatList(region, ";", doc);
+                doc.prepend(region.keyword("."), this::noSpace);
+                for (var parameter : predicateDefinition.getParameters()) {
+                        doc.format(parameter);
+                }
+                for (var body : predicateDefinition.getBodies()) {
+                        doc.format(body);
+                }
+        }
+
+        protected void format(Parameter parameter, IFormattableDocument doc) {
+                doc.append(regionFor(parameter).feature(ProblemPackage.Literals.PARAMETER__PARAMETER_TYPE), this::oneSpace);
+        }
+
+        protected void format(Conjunction conjunction, IFormattableDocument doc) {
+                var region = regionFor(conjunction);
+                formatList(region, ",", doc);
+                for (var literal : conjunction.getLiterals()) {
+                        doc.format(literal);
+                }
+        }
+
+        protected void format(NegativeLiteral literal, IFormattableDocument doc) {
+                var region = regionFor(literal);
+                doc.append(region.keyword("!"), this::noSpace);
+                doc.format(literal.getAtom());
+        }
+
+        protected void format(Atom atom, IFormattableDocument doc) {
+                var region = regionFor(atom);
+                doc.append(region.feature(ProblemPackage.Literals.ATOM__RELATION), this::noSpace);
+                doc.append(region.feature(ProblemPackage.Literals.ATOM__TRANSITIVE_CLOSURE), this::noSpace);
+                formatParenthesizedList(region, doc);
+                for (var argument : atom.getArguments()) {
+                        doc.format(argument);
+                }
+        }
+
+        protected void format(IndividualDeclaration individualDeclaration, IFormattableDocument doc) {
+                surroundNewLines(doc, individualDeclaration, this::singleNewLine);
+                var region = regionFor(individualDeclaration);
+                doc.append(region.keyword("indiv"), this::oneSpace);
+                formatList(region, ",", doc);
+                doc.prepend(region.keyword("."), this::noSpace);
+        }
+
+        protected void formatParenthesizedList(ISemanticRegionsFinder region, IFormattableDocument doc) {
+                doc.append(region.keyword("("), this::noSpace);
+                doc.prepend(region.keyword(")"), this::noSpace);
+                formatList(region, ",", doc);
+        }
+
+        protected void formatList(ISemanticRegionsFinder region, String separator, IFormattableDocument doc) {
+                for (var comma : region.keywords(separator)) {
+                        doc.prepend(comma, this::noSpace);
+                        doc.append(comma, this::oneSpace);
+                }
+        }
+
+        protected void singleNewLine(IHiddenRegionFormatter it) {
+                it.setNewLines(1, 1, 2);
+        }
+
+        protected void twoNewLines(IHiddenRegionFormatter it) {
+                it.highPriority();
+                it.setNewLines(2);
+        }
+
+        protected void surroundNewLines(IFormattableDocument doc, EObject eObject,
+                        Procedure1<? super IHiddenRegionFormatter> init) {
+                var region = doc.getRequest().getTextRegionAccess().regionForEObject(eObject);
+                preprendNewLines(doc, region, init);
+                appendNewLines(doc, region, init);
+        }
+
+        protected void preprendNewLines(IFormattableDocument doc, ISequentialRegion region,
+                        Procedure1<? super IHiddenRegionFormatter> init) {
+                if (region == null) {
+                        return;
+                }
+                var previousHiddenRegion = region.getPreviousHiddenRegion();
+                if (previousHiddenRegion == null) {
+                        return;
+                }
+                if (previousHiddenRegion.getPreviousSequentialRegion() == null) {
+                        doc.set(previousHiddenRegion, it -> it.setNewLines(0));
+                } else {
+                        doc.set(previousHiddenRegion, init);
+                }
+        }
+
+        protected void appendNewLines(IFormattableDocument doc, ISequentialRegion region,
+                        Procedure1<? super IHiddenRegionFormatter> init) {
+                if (region == null) {
+                        return;
+                }
+                var nextHiddenRegion = region.getNextHiddenRegion();
+                if (nextHiddenRegion == null) {
+                        return;
+                }
+                if (nextHiddenRegion.getNextSequentialRegion() == null) {
+                        doc.set(nextHiddenRegion, it -> it.setNewLines(1));
+                } else {
+                        doc.set(nextHiddenRegion, init);
+                }
+        }
+}
diff --git a/language/src/test/java/tools/refinery/language/tests/formatting2/ProblemFormatterTest.java b/language/src/test/java/tools/refinery/language/tests/formatting2/ProblemFormatterTest.java
new file mode 100644
index 00000000..41ad2d31
--- /dev/null
+++ b/language/src/test/java/tools/refinery/language/tests/formatting2/ProblemFormatterTest.java
@@ -0,0 +1,235 @@
+package tools.refinery.language.tests.formatting2;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static org.hamcrest.Matchers.equalTo;
+
+import java.util.List;
+
+import org.eclipse.xtext.formatting2.FormatterRequest;
+import org.eclipse.xtext.formatting2.IFormatter2;
+import org.eclipse.xtext.formatting2.regionaccess.ITextRegionAccess;
+import org.eclipse.xtext.formatting2.regionaccess.ITextReplacement;
+import org.eclipse.xtext.formatting2.regionaccess.TextRegionAccessBuilder;
+import org.eclipse.xtext.resource.XtextResource;
+import org.eclipse.xtext.testing.InjectWith;
+import org.eclipse.xtext.testing.extensions.InjectionExtension;
+import org.eclipse.xtext.testing.util.ParseHelper;
+import org.junit.jupiter.api.Test;
+import org.junit.jupiter.api.extension.ExtendWith;
+
+import com.google.inject.Inject;
+import com.google.inject.Provider;
+
+import tools.refinery.language.model.problem.Problem;
+import tools.refinery.language.tests.ProblemInjectorProvider;
+
+@ExtendWith(InjectionExtension.class)
+@InjectWith(ProblemInjectorProvider.class)
+class ProblemFormatterTest {
+        @Inject
+        private ParseHelper<Problem> parseHelper;
+
+        @Inject
+        private Provider<FormatterRequest> formatterRequestProvider;
+
+        @Inject
+        private TextRegionAccessBuilder regionBuilder;
+
+        @Inject
+        private IFormatter2 formatter2;
+
+        @Test
+        void problemNameTest() {
+                testFormatter("  problem  problem  .  ", "problem problem.\n");
+        }
+
+        @Test
+        void assertionTest() {
+                testFormatter("  equals (  a  ,  b  ,  *  )  :  true  .  ", "equals(a, b, *): true.\n");
+        }
+
+        @Test
+        void defaultAssertionTest() {
+                testFormatter("  default  equals (  a  ,  b  ,  *  )  :  true  .  ", "default equals(a, b, *): true.\n");
+        }
+
+        @Test
+        void assertionShortTrueTest() {
+                testFormatter("  equals (  a  ,  b  ,  *  )  .  ", "equals(a, b, *).\n");
+        }
+
+        @Test
+        void defaultAssertionShortTrueTest() {
+                testFormatter("  default  equals (  a  ,  b  ,  *  )  .  ", "default equals(a, b, *).\n");
+        }
+
+        @Test
+        void assertionShortFalseTest() {
+                testFormatter("  !  equals (  a  ,  b  ,  *  )  .  ", "!equals(a, b, *).\n");
+        }
+
+        @Test
+        void defaultAssertionShortFalseTest() {
+                testFormatter("  default  !  equals (  a  ,  b  ,  *  )  .  ", "default !equals(a, b, *).\n");
+        }
+
+        @Test
+        void assertionShortUnknownTest() {
+                testFormatter("  ?  equals (  a  ,  b  ,  *  )  .  ", "?equals(a, b, *).\n");
+        }
+
+        @Test
+        void defaultAssertionShortUnknownTest() {
+                testFormatter("  default  ?  equals (  a  ,  b  ,  *  )  .  ", "default ?equals(a, b, *).\n");
+        }
+
+        @Test
+        void multipleAssertionsTest() {
+                testFormatter("  exists (  a  )  .  ?  equals  (  a  ,  a  ).", """
+                                exists(a).
+                                ?equals(a, a).
+                                """);
+        }
+
+        @Test
+        void multipleAssertionsNamedProblemTest() {
+                testFormatter("  problem  foo  .  exists (  a  )  .  ?  equals  (  a  ,  a  ).", """
+                                problem foo.
+
+                                exists(a).
+                                ?equals(a, a).
+                                """);
+        }
+
+        @Test
+        void classWithoutBodyTest() {
+                testFormatter("  class  Foo  .  ", "class Foo.\n");
+        }
+
+        @Test
+        void abstractClassWithoutBodyTest() {
+                testFormatter("  abstract  class  Foo  .  ", "abstract class Foo.\n");
+        }
+
+        @Test
+        void classExtendsWithoutBodyTest() {
+                testFormatter("  class  Foo.  class  Bar  .  class  Quux  extends  Foo  ,  Bar  .  ", """
+                                class Foo.
+
+                                class Bar.
+
+                                class Quux extends Foo, Bar.
+                                """);
+        }
+
+        @Test
+        void classWithEmptyBodyTest() {
+                testFormatter("  class  Foo  {  }  ", """
+                                class Foo {
+                                }
+                                """);
+        }
+
+        @Test
+        void classExtendsWithBodyTest() {
+                testFormatter("  class  Foo.  class  Bar  .  class  Quux  extends  Foo  ,  Bar  {  }  ", """
+                                class Foo.
+
+                                class Bar.
+
+                                class Quux extends Foo, Bar {
+                                }
+                                """);
+        }
+
+        @Test
+        void predicateWithoutBodyTest() {
+                testFormatter("  pred  foo  (  node  a  ,  b  )  .  ", "pred foo(node a, b).\n");
+        }
+
+        @Test
+        void predicateWithBodyTest() {
+                testFormatter(
+                                "  pred  foo  (  node  a  ,  b  )  <->  equal  (a  ,  _c  )  ,  !  equal  (  a  ,  b  )  ;  equal+(  a  ,  b  )  .  ",
+                                "pred foo(node a, b) <-> equal(a, _c), !equal(a, b); equal+(a, b).\n");
+        }
+
+        @Test
+        void predicatesWithoutBodyTest() {
+                testFormatter("  pred  foo  (  node  a  ,  b  )  .  pred  bar  (  node  c  )  .  ", """
+                                pred foo(node a, b).
+
+                                pred bar(node c).
+                                """);
+        }
+
+        @Test
+        void predicateCommentsTest() {
+                testFormatter("""
+                                  % Some foo
+                                pred  foo  (  node  a  ,  b  )  .
+                                  % Some bar
+                                pred  bar  (  node  c  )  .
+                                """, """
+                                % Some foo
+                                pred foo(node a, b).
+
+                                % Some bar
+                                pred bar(node c).
+                                """);
+        }
+
+        @Test
+        void individualDeclarationTest() {
+                testFormatter("  indiv  a  ,  b  .  ", "indiv a, b.\n");
+        }
+
+        @Test
+        void mixedDeclarationsTest() {
+                testFormatter("""
+                                problem test.
+                                pred foo(node a).
+                                class Foo.
+                                foo(n1, n2).
+                                indiv i1.
+                                !foo(i1, n1).
+                                pred bar(node a, node b).
+                                pred quux().
+                                default !bar(*, *).
+                                """, """
+                                problem test.
+
+                                pred foo(node a).
+
+                                class Foo.
+
+                                foo(n1, n2).
+                                indiv i1.
+                                !foo(i1, n1).
+
+                                pred bar(node a, node b).
+
+                                pred quux().
+
+                                default !bar(*, *).
+                                """);
+        }
+
+        private void testFormatter(String toFormat, String expected) {
+                Problem problem;
+                try {
+                        problem = parseHelper.parse(toFormat);
+                } catch (Exception e) {
+                        throw new RuntimeException("Failed to parse document", e);
+                }
+                var resource = (XtextResource) problem.eResource();
+                FormatterRequest request = formatterRequestProvider.get();
+                request.setAllowIdentityEdits(false);
+                request.setFormatUndefinedHiddenRegionsOnly(false);
+                ITextRegionAccess regionAccess = regionBuilder.forNodeModel(resource).create();
+                request.setTextRegionAccess(regionAccess);
+                List<ITextReplacement> replacements = formatter2.format(request);
+                var formattedString = regionAccess.getRewriter().renderToString(replacements);
+                assertThat(formattedString, equalTo(expected));
+        }
+}
diff --git a/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java b/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java
index 22c79a09..ba3aaeb7 100644
--- a/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java
+++ b/language/src/test/java/tools/refinery/language/tests/serializer/ProblemSerializerTest.java
@@ -38,16 +38,16 @@ import tools.refinery.language.tests.ProblemInjectorProvider;
 @InjectWith(ProblemInjectorProvider.class)
 class ProblemSerializerTest {
         @Inject
-        ResourceSet resourceSet;
+        private ResourceSet resourceSet;
 
         @Inject
-        ProblemTestUtil testUtil;
+        private ProblemTestUtil testUtil;
 
-        Resource resource;
+        private Resource resource;
 
-        Problem problem;
+        private Problem problem;
 
-        Problem builtin;
+        private Problem builtin;
 
         @BeforeEach
         void beforeEach() {
@@ -68,14 +68,16 @@ class ProblemSerializerTest {
                 problem.getStatements().add(individualDeclaration);
                 createAssertion(pred, node, value);
 
-                assertSerializedResult("pred foo ( node p ) . indiv a . " + serializedAssertion);
+                assertSerializedResult("""
+                                pred foo(node p).
+
+                                indiv a.
+                                """ + serializedAssertion + "\n");
         }
 
         static Stream<Arguments> assertionTest() {
-                return Stream.of(Arguments.of(LogicValue.TRUE, "foo ( a ) ."),
-                                Arguments.of(LogicValue.FALSE, "! foo ( a ) ."),
-                                Arguments.of(LogicValue.UNKNOWN, "? foo ( a ) ."),
-                                Arguments.of(LogicValue.ERROR, "foo ( a ) : error ."));
+                return Stream.of(Arguments.of(LogicValue.TRUE, "foo(a)."), Arguments.of(LogicValue.FALSE, "!foo(a)."),
+                                Arguments.of(LogicValue.UNKNOWN, "?foo(a)."), Arguments.of(LogicValue.ERROR, "foo(a): error."));
         }
 
         @Test
@@ -86,7 +88,11 @@ class ProblemSerializerTest {
                 problem.getNodes().add(node);
                 createAssertion(pred, node);
 
-                assertSerializedResult("pred foo ( node p ) . foo ( a ) .");
+                assertSerializedResult("""
+                                pred foo(node p).
+
+                                foo(a).
+                                """);
         }
 
         private PredicateDefinition createPred() {
@@ -111,7 +117,11 @@ class ProblemSerializerTest {
                 problem.getStatements().add(classDeclaration);
                 createAssertion(classDeclaration, newNode);
 
-                assertSerializedResult("class Foo . Foo ( Foo::new ) .");
+                assertSerializedResult("""
+                                class Foo.
+
+                                Foo(Foo::new).
+                                """);
         }
 
         private void createAssertion(Relation relation, Node node) {
@@ -151,7 +161,9 @@ class ProblemSerializerTest {
                 pred.getBodies().add(conjunction);
                 problem.getStatements().add(pred);
 
-                assertSerializedResult("pred foo ( node p1 , node p2 ) <-> equals ( p1 , q ) , equals ( q , p2 ) .");
+                assertSerializedResult("""
+                                pred foo(node p1, node p2) <-> equals(p1, q), equals(q, p2).
+                                """);
         }
 
         private Atom createAtom(Relation relation, VariableOrNode variable1, VariableOrNode variable2) {
@@ -192,7 +204,9 @@ class ProblemSerializerTest {
                 pred.getBodies().add(conjunction);
                 problem.getStatements().add(pred);
 
-                assertSerializedResult("pred foo ( node p ) <-> equals ( p , _q ) .");
+                assertSerializedResult("""
+                                pred foo(node p) <-> equals(p, _q).
+                                """);
         }
 
         private void assertSerializedResult(String expected) {