From e42a307594c6518fe15c99f2d06d2dc47915d17f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 00:39:38 +0100 Subject: [PATCH 01/21] Add a browser-native LiquidJava playground Run the published verifier locally through CheerpJ with a Z3 WebAssembly native-method adapter and playground-scoped cross-origin isolation. Build the runtime in the docs Pages workflow and show source diagnostics. Co-authored-by: Codex --- .github/workflows/pages.yml | 18 + .gitignore | 3 + README.md | 29 + _config.yml | 5 + package-lock.json | 1328 +++++++++++++++++ package.json | 19 + pages/index.md | 1 + playground/editor.css | 17 + playground/index.md | 35 + playground/isolation.js | 14 + scripts/playground/adapter.mjs | 34 + scripts/playground/adapter.test.mjs | 51 + scripts/playground/build.mjs | 8 + scripts/playground/build.py | 97 ++ scripts/playground/editor.js | 123 ++ scripts/playground/examples.mjs | 58 + .../java/com/microsoft/z3/Z3Loader.java | 6 + .../liquidjava/playground/BrowserRunner.java | 94 ++ scripts/playground/worker.js | 39 + 19 files changed, 1979 insertions(+) create mode 100644 package-lock.json create mode 100644 package.json create mode 100644 playground/editor.css create mode 100644 playground/index.md create mode 100644 playground/isolation.js create mode 100644 scripts/playground/adapter.mjs create mode 100644 scripts/playground/adapter.test.mjs create mode 100644 scripts/playground/build.mjs create mode 100644 scripts/playground/build.py create mode 100644 scripts/playground/editor.js create mode 100644 scripts/playground/examples.mjs create mode 100644 scripts/playground/java/com/microsoft/z3/Z3Loader.java create mode 100644 scripts/playground/java/liquidjava/playground/BrowserRunner.java create mode 100644 scripts/playground/worker.js diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml index fe3997c..c72862e 100644 --- a/.github/workflows/pages.yml +++ b/.github/workflows/pages.yml @@ -28,6 +28,24 @@ jobs: ruby-version: "2.6" bundler-cache: true + - name: Setup Node + uses: actions/setup-node@v4 + with: + node-version: "22" + cache: npm + + - name: Setup Java + uses: actions/setup-java@v4 + with: + distribution: temurin + java-version: "17" + + - name: Build playground + run: | + npm ci --ignore-scripts --no-audit --no-fund + npm run build:playground + npm run test:playground + - name: Setup Pages uses: actions/configure-pages@v5 diff --git a/.gitignore b/.gitignore index 23cf3de..b1b3066 100644 --- a/.gitignore +++ b/.gitignore @@ -5,3 +5,6 @@ _site/ .bundle/ vendor/ Gemfile.lock +node_modules/ +.playground-build/ +playground/runtime/ diff --git a/README.md b/README.md index 22a3c07..68cdb70 100644 --- a/README.md +++ b/README.md @@ -32,3 +32,32 @@ bundle exec jekyll build ## Publishing The site is configured as a GitHub Pages project site at [https://liquid-java.github.io/liquidjava-docs/](https://liquid-java.github.io/liquidjava-docs/). + +## Browser playground + +The `/playground/` page runs LiquidJava in a browser worker with CheerpJ 4.3 and the official Z3 WebAssembly package. Code is checked locally. Stop terminates the worker, including a running solver, and the next check creates a fresh runtime. + +Build the runtime before building Jekyll: + +```bash +npm ci --ignore-scripts --no-audit --no-fund +npm run build:playground +npm run test:playground +bundle exec jekyll build +``` + +The build requires JDK 17, Python 3, Node.js, and access to Maven Central. It recompiles the published verifier 0.0.35 and annotation API 0.0.7 sources for Java 17 without changing them, packages their dependencies, and adds the docs-owned runner and Z3 loader. The standard-library classpath comes from the build JDK's `java.base.jmod`. Generated runtime files are ignored by Git and included in the Pages artifact. The normal Pages workflow builds everything automatically. + +The browser package also adapts Spoon 10.4.2's query initialization: when CheerpJ supplies an empty cast-exception stack trace, it selects Spoon's existing exotic-JVM query mode. The pinned source is downloaded and the adaptation checked during the build. This change is limited to the docs' generated dependency; the verifier repository and published sources remain unchanged. + +For local testing, after building the runtime: + +```bash +npm run serve:playground +``` + +Open `http://127.0.0.1:8770/playground/`. This uses a static server with HTTP range support, which CheerpJ needs when loading JARs. Ordinary `jekyll serve` does not supply the required range responses. + +`playground/isolation.js` is a service worker scoped to `/playground/`. It adds the cross-origin isolation response headers Z3 requires on static hosting, including GitHub Pages. The first visit registers it and reloads once. Other docs pages are outside its scope. CheerpJ loads from its official CDN inside the verification worker; its runtime is not copied into this repository. + +The playground checks a single Java file using Java 8 source syntax, bundled annotations and core standard-library types from `java.base`. External dependencies and other Java modules are not available. Z3 4.16 runs behind the verifier's 4.8.17 Java API; browser integration tests must be repeated when updating either version. Unsupported native operations and unknown solver results fail explicitly instead of reporting success. This integration is kept entirely in `liquidjava-docs`. diff --git a/_config.yml b/_config.yml index 8fdb797..6d27a9e 100644 --- a/_config.yml +++ b/_config.yml @@ -46,6 +46,11 @@ defaults: image: /assets/images/Liquid2.png exclude: + - node_modules + - scripts + - package.json + - package-lock.json + - .playground-build - .DS_Store - vendor - Gemfile diff --git a/package-lock.json b/package-lock.json new file mode 100644 index 0000000..8ee2ab3 --- /dev/null +++ b/package-lock.json @@ -0,0 +1,1328 @@ +{ + "name": "liquidjava-docs", + "lockfileVersion": 3, + "requires": true, + "packages": { + "": { + "name": "liquidjava-docs", + "dependencies": { + "@codemirror/lang-java": "6.0.2", + "@codemirror/lint": "6.8.5", + "codemirror": "6.0.2" + }, + "devDependencies": { + "esbuild": "0.25.10", + "http-server": "14.1.1", + "z3-solver": "4.16.0" + } + }, + "node_modules/@codemirror/autocomplete": { + "version": "6.20.3", + "resolved": "https://registry.npmjs.org/@codemirror/autocomplete/-/autocomplete-6.20.3.tgz", + "integrity": "sha512-tlosUqb+3BbxCxZdu4tKeRghPFC+QM7q4X5YhKV2eCmPG+1r2F3f4AaSz5sCrFqUtX4Jh20VFTKecl16MgiV9g==", + "license": "MIT", + "dependencies": { + "@codemirror/language": "^6.0.0", + "@codemirror/state": "^6.0.0", + "@codemirror/view": "^6.17.0", + "@lezer/common": "^1.0.0" + } + }, + "node_modules/@codemirror/commands": { + "version": "6.11.1", + "resolved": "https://registry.npmjs.org/@codemirror/commands/-/commands-6.11.1.tgz", + "integrity": "sha512-O/4hG3SC1YwcmQ0d2UVNDs+AsaNWd1iHVxbTeEBuqH+6bExAiPK3iS/BvpY6rZGURALv4ZD3sIgcCmRvw3ehBg==", + "license": "MIT", + "dependencies": { + "@codemirror/language": "^6.0.0", + "@codemirror/state": "^6.7.0", + "@codemirror/view": "^6.27.0", + "@lezer/common": "^1.1.0" + } + }, + "node_modules/@codemirror/lang-java": { + "version": "6.0.2", + "resolved": "https://registry.npmjs.org/@codemirror/lang-java/-/lang-java-6.0.2.tgz", + "integrity": "sha512-m5Nt1mQ/cznJY7tMfQTJchmrjdjQ71IDs+55d1GAa8DGaB8JXWsVCkVT284C3RTASaY43YknrK2X3hPO/J3MOQ==", + "license": "MIT", + "dependencies": { + "@codemirror/language": "^6.0.0", + "@lezer/java": "^1.0.0" + } + }, + "node_modules/@codemirror/language": { + "version": "6.12.4", + "resolved": "https://registry.npmjs.org/@codemirror/language/-/language-6.12.4.tgz", + "integrity": "sha512-1q4PaT+o6PbgpkJt4Q8Fv5XJxTy4FUZ4MWETtyiDw3J0Pyr9E2vqcKL+k9wcvjNTIsauxvE7OfmWj3FRPHQ76A==", + "license": "MIT", + "dependencies": { + "@codemirror/state": "^6.0.0", + "@codemirror/view": "^6.23.0", + "@lezer/common": "^1.5.0", + "@lezer/highlight": "^1.0.0", + "@lezer/lr": "^1.0.0", + "style-mod": "^4.0.0" + } + }, + "node_modules/@codemirror/lint": { + "version": "6.8.5", + "resolved": "https://registry.npmjs.org/@codemirror/lint/-/lint-6.8.5.tgz", + "integrity": "sha512-s3n3KisH7dx3vsoeGMxsbRAgKe4O1vbrnKBClm99PU0fWxmxsx5rR2PfqQgIt+2MMJBHbiJ5rfIdLYfB9NNvsA==", + "license": "MIT", + "dependencies": { + "@codemirror/state": "^6.0.0", + "@codemirror/view": "^6.35.0", + "crelt": "^1.0.5" + } + }, + "node_modules/@codemirror/search": { + "version": "6.7.2", + "resolved": "https://registry.npmjs.org/@codemirror/search/-/search-6.7.2.tgz", + "integrity": "sha512-gUYkYhT2+n/+VGZ+8EzE5WFkYZUZYm1VOKDudIsNqh42uRVQJ0a6Yss9sdKT3MeOYfuL1N6AZA57oza0Oyr0LA==", + "license": "MIT", + "dependencies": { + "@codemirror/state": "^6.0.0", + "@codemirror/view": "^6.37.0", + "crelt": "^1.0.5" + } + }, + "node_modules/@codemirror/state": { + "version": "6.7.6", + "resolved": "https://registry.npmjs.org/@codemirror/state/-/state-6.7.6.tgz", + "integrity": "sha512-kAz+AncRtKuIknedxT1bq4XwXv4UowhbkHU1myPrtVb/jZtImWuV5BXzv5vK6i3kYACsdiZiQKFQQ5Mq7elW8w==", + "license": "MIT", + "dependencies": { + "@marijn/find-cluster-break": "^1.0.0" + } + }, + "node_modules/@codemirror/view": { + "version": "6.43.13", + "resolved": "https://registry.npmjs.org/@codemirror/view/-/view-6.43.13.tgz", + "integrity": "sha512-sihaFrUzAsYBQsL9J2t69y8nfMQGwcYmggAZsk+kjPbjYZMyuf2hU8tUNTZ+P+isb6XRr8JE22TZlJxBoVdH1A==", + "license": "MIT", + "dependencies": { + "@codemirror/state": "^6.7.0", + "crelt": "^1.0.6", + "style-mod": "^4.1.0", + "w3c-keyname": "^2.2.4" + } + }, + "node_modules/@esbuild/aix-ppc64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/aix-ppc64/-/aix-ppc64-0.25.10.tgz", + "integrity": "sha512-0NFWnA+7l41irNuaSVlLfgNT12caWJVLzp5eAVhZ0z1qpxbockccEt3s+149rE64VUI3Ml2zt8Nv5JVc4QXTsw==", + "cpu": [ + "ppc64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "aix" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/android-arm": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/android-arm/-/android-arm-0.25.10.tgz", + "integrity": "sha512-dQAxF1dW1C3zpeCDc5KqIYuZ1tgAdRXNoZP7vkBIRtKZPYe2xVr/d3SkirklCHudW1B45tGiUlz2pUWDfbDD4w==", + "cpu": [ + "arm" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "android" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/android-arm64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/android-arm64/-/android-arm64-0.25.10.tgz", + "integrity": "sha512-LSQa7eDahypv/VO6WKohZGPSJDq5OVOo3UoFR1E4t4Gj1W7zEQMUhI+lo81H+DtB+kP+tDgBp+M4oNCwp6kffg==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "android" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/android-x64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/android-x64/-/android-x64-0.25.10.tgz", + "integrity": "sha512-MiC9CWdPrfhibcXwr39p9ha1x0lZJ9KaVfvzA0Wxwz9ETX4v5CHfF09bx935nHlhi+MxhA63dKRRQLiVgSUtEg==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "android" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/darwin-arm64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/darwin-arm64/-/darwin-arm64-0.25.10.tgz", + "integrity": "sha512-JC74bdXcQEpW9KkV326WpZZjLguSZ3DfS8wrrvPMHgQOIEIG/sPXEN/V8IssoJhbefLRcRqw6RQH2NnpdprtMA==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "darwin" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/darwin-x64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/darwin-x64/-/darwin-x64-0.25.10.tgz", + "integrity": "sha512-tguWg1olF6DGqzws97pKZ8G2L7Ig1vjDmGTwcTuYHbuU6TTjJe5FXbgs5C1BBzHbJ2bo1m3WkQDbWO2PvamRcg==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "darwin" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/freebsd-arm64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/freebsd-arm64/-/freebsd-arm64-0.25.10.tgz", + "integrity": "sha512-3ZioSQSg1HT2N05YxeJWYR+Libe3bREVSdWhEEgExWaDtyFbbXWb49QgPvFH8u03vUPX10JhJPcz7s9t9+boWg==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "freebsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/freebsd-x64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/freebsd-x64/-/freebsd-x64-0.25.10.tgz", + "integrity": "sha512-LLgJfHJk014Aa4anGDbh8bmI5Lk+QidDmGzuC2D+vP7mv/GeSN+H39zOf7pN5N8p059FcOfs2bVlrRr4SK9WxA==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "freebsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-arm": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/linux-arm/-/linux-arm-0.25.10.tgz", + "integrity": "sha512-oR31GtBTFYCqEBALI9r6WxoU/ZofZl962pouZRTEYECvNF/dtXKku8YXcJkhgK/beU+zedXfIzHijSRapJY3vg==", + "cpu": [ + "arm" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-arm64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/linux-arm64/-/linux-arm64-0.25.10.tgz", + "integrity": "sha512-5luJWN6YKBsawd5f9i4+c+geYiVEw20FVW5x0v1kEMWNq8UctFjDiMATBxLvmmHA4bf7F6hTRaJgtghFr9iziQ==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-ia32": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/linux-ia32/-/linux-ia32-0.25.10.tgz", + "integrity": "sha512-NrSCx2Kim3EnnWgS4Txn0QGt0Xipoumb6z6sUtl5bOEZIVKhzfyp/Lyw4C1DIYvzeW/5mWYPBFJU3a/8Yr75DQ==", + "cpu": [ + "ia32" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-loong64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/linux-loong64/-/linux-loong64-0.25.10.tgz", + "integrity": "sha512-xoSphrd4AZda8+rUDDfD9J6FUMjrkTz8itpTITM4/xgerAZZcFW7Dv+sun7333IfKxGG8gAq+3NbfEMJfiY+Eg==", + "cpu": [ + "loong64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-mips64el": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/linux-mips64el/-/linux-mips64el-0.25.10.tgz", + "integrity": "sha512-ab6eiuCwoMmYDyTnyptoKkVS3k8fy/1Uvq7Dj5czXI6DF2GqD2ToInBI0SHOp5/X1BdZ26RKc5+qjQNGRBelRA==", + "cpu": [ + "mips64el" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-ppc64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/linux-ppc64/-/linux-ppc64-0.25.10.tgz", + "integrity": "sha512-NLinzzOgZQsGpsTkEbdJTCanwA5/wozN9dSgEl12haXJBzMTpssebuXR42bthOF3z7zXFWH1AmvWunUCkBE4EA==", + "cpu": [ + "ppc64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-riscv64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/linux-riscv64/-/linux-riscv64-0.25.10.tgz", + "integrity": "sha512-FE557XdZDrtX8NMIeA8LBJX3dC2M8VGXwfrQWU7LB5SLOajfJIxmSdyL/gU1m64Zs9CBKvm4UAuBp5aJ8OgnrA==", + "cpu": [ + "riscv64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-s390x": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/linux-s390x/-/linux-s390x-0.25.10.tgz", + "integrity": "sha512-3BBSbgzuB9ajLoVZk0mGu+EHlBwkusRmeNYdqmznmMc9zGASFjSsxgkNsqmXugpPk00gJ0JNKh/97nxmjctdew==", + "cpu": [ + "s390x" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/linux-x64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/linux-x64/-/linux-x64-0.25.10.tgz", + "integrity": "sha512-QSX81KhFoZGwenVyPoberggdW1nrQZSvfVDAIUXr3WqLRZGZqWk/P4T8p2SP+de2Sr5HPcvjhcJzEiulKgnxtA==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "linux" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/netbsd-arm64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/netbsd-arm64/-/netbsd-arm64-0.25.10.tgz", + "integrity": "sha512-AKQM3gfYfSW8XRk8DdMCzaLUFB15dTrZfnX8WXQoOUpUBQ+NaAFCP1kPS/ykbbGYz7rxn0WS48/81l9hFl3u4A==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "netbsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/netbsd-x64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/netbsd-x64/-/netbsd-x64-0.25.10.tgz", + "integrity": "sha512-7RTytDPGU6fek/hWuN9qQpeGPBZFfB4zZgcz2VK2Z5VpdUxEI8JKYsg3JfO0n/Z1E/6l05n0unDCNc4HnhQGig==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "netbsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/openbsd-arm64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/openbsd-arm64/-/openbsd-arm64-0.25.10.tgz", + "integrity": "sha512-5Se0VM9Wtq797YFn+dLimf2Zx6McttsH2olUBsDml+lm0GOCRVebRWUvDtkY4BWYv/3NgzS8b/UM3jQNh5hYyw==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "openbsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/openbsd-x64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/openbsd-x64/-/openbsd-x64-0.25.10.tgz", + "integrity": "sha512-XkA4frq1TLj4bEMB+2HnI0+4RnjbuGZfet2gs/LNs5Hc7D89ZQBHQ0gL2ND6Lzu1+QVkjp3x1gIcPKzRNP8bXw==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "openbsd" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/openharmony-arm64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/openharmony-arm64/-/openharmony-arm64-0.25.10.tgz", + "integrity": "sha512-AVTSBhTX8Y/Fz6OmIVBip9tJzZEUcY8WLh7I59+upa5/GPhh2/aM6bvOMQySspnCCHvFi79kMtdJS1w0DXAeag==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "openharmony" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/sunos-x64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/sunos-x64/-/sunos-x64-0.25.10.tgz", + "integrity": "sha512-fswk3XT0Uf2pGJmOpDB7yknqhVkJQkAQOcW/ccVOtfx05LkbWOaRAtn5SaqXypeKQra1QaEa841PgrSL9ubSPQ==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "sunos" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/win32-arm64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/win32-arm64/-/win32-arm64-0.25.10.tgz", + "integrity": "sha512-ah+9b59KDTSfpaCg6VdJoOQvKjI33nTaQr4UluQwW7aEwZQsbMCfTmfEO4VyewOxx4RaDT/xCy9ra2GPWmO7Kw==", + "cpu": [ + "arm64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "win32" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/win32-ia32": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/win32-ia32/-/win32-ia32-0.25.10.tgz", + "integrity": "sha512-QHPDbKkrGO8/cz9LKVnJU22HOi4pxZnZhhA2HYHez5Pz4JeffhDjf85E57Oyco163GnzNCVkZK0b/n4Y0UHcSw==", + "cpu": [ + "ia32" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "win32" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@esbuild/win32-x64": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/@esbuild/win32-x64/-/win32-x64-0.25.10.tgz", + "integrity": "sha512-9KpxSVFCu0iK1owoez6aC/s/EdUQLDN3adTxGCqxMVhrPDj6bt5dbrHDXUuq+Bs2vATFBBrQS5vdQ/Ed2P+nbw==", + "cpu": [ + "x64" + ], + "dev": true, + "license": "MIT", + "optional": true, + "os": [ + "win32" + ], + "engines": { + "node": ">=18" + } + }, + "node_modules/@lezer/common": { + "version": "1.5.3", + "resolved": "https://registry.npmjs.org/@lezer/common/-/common-1.5.3.tgz", + "integrity": "sha512-H0iErY4e43LpXbYDyBci5W4v/RwTgGV3YzYOlJPiGZ8RY8w51kVE+xLn1tg3Z6UmSfyETvtsUK3r7YsgDQEI7Q==", + "license": "MIT" + }, + "node_modules/@lezer/highlight": { + "version": "1.2.5", + "resolved": "https://registry.npmjs.org/@lezer/highlight/-/highlight-1.2.5.tgz", + "integrity": "sha512-O1GMVKgtf5YspFaRzpmqkVgMtIk2HG9uMAbH6wdAIdNh3TVzCsch/+cRi+6l2//UGDKe6NB9BW3cvuR5ezMQ0w==", + "license": "MIT", + "dependencies": { + "@lezer/common": "^1.3.0" + } + }, + "node_modules/@lezer/java": { + "version": "1.1.4", + "resolved": "https://registry.npmjs.org/@lezer/java/-/java-1.1.4.tgz", + "integrity": "sha512-gQylJ2xHV2xXsVqtnAcJrcROvLZJaQiC0tR//+q0k961BxqvyYttusPkJ8d9T1fPDJKHJW2etUH8XbIn9jhVUg==", + "license": "MIT", + "dependencies": { + "@lezer/common": "^1.2.0", + "@lezer/highlight": "^1.0.0", + "@lezer/lr": "^1.0.0" + } + }, + "node_modules/@lezer/lr": { + "version": "1.4.10", + "resolved": "https://registry.npmjs.org/@lezer/lr/-/lr-1.4.10.tgz", + "integrity": "sha512-rnCpTIBafOx4mRp43xOxDJbFipJm/c0cia/V5TiGlhmMa+wsSdoGmUN3w5Bqrks/09Q/D4tNAmWaT8p6NRi77A==", + "license": "MIT", + "dependencies": { + "@lezer/common": "^1.0.0" + } + }, + "node_modules/@marijn/find-cluster-break": { + "version": "1.0.4", + "resolved": "https://registry.npmjs.org/@marijn/find-cluster-break/-/find-cluster-break-1.0.4.tgz", + "integrity": "sha512-Wy0V7+SGUjnF9/TkiM1hKVDPj7jKXduPNboMVtHTA8dySMURWqfg/JZ9E2Sq8JgSJmkl7k7Qe9FLeMSrSraWmQ==", + "license": "MIT" + }, + "node_modules/ansi-styles": { + "version": "4.3.0", + "resolved": "https://registry.npmjs.org/ansi-styles/-/ansi-styles-4.3.0.tgz", + "integrity": "sha512-zbB9rCJAT1rbjiVDb2hqKFHNYLxgtk8NURxZ3IZwD3F6NtxbXZQCnnSi1Lkx+IDohdPlFp222wVALIheZJQSEg==", + "dev": true, + "license": "MIT", + "dependencies": { + "color-convert": "^2.0.1" + }, + "engines": { + "node": ">=8" + }, + "funding": { + "url": "https://github.com/chalk/ansi-styles?sponsor=1" + } + }, + "node_modules/async": { + "version": "3.2.6", + "resolved": "https://registry.npmjs.org/async/-/async-3.2.6.tgz", + "integrity": "sha512-htCUDlxyyCLMgaM3xXg0C0LW2xqfuQ6p05pCEIsXuyQ+a1koYKTuBMzRNwmybfLgvJDMd0r1LTn4+E0Ti6C2AA==", + "dev": true, + "license": "MIT" + }, + "node_modules/async-mutex": { + "version": "0.3.2", + "resolved": "https://registry.npmjs.org/async-mutex/-/async-mutex-0.3.2.tgz", + "integrity": "sha512-HuTK7E7MT7jZEh1P9GtRW9+aTWiDWWi9InbZ5hjxrnRa39KS4BW04+xLBhYNS2aXhHUIKZSw3gj4Pn1pj+qGAA==", + "dev": true, + "license": "MIT", + "dependencies": { + "tslib": "^2.3.1" + } + }, + "node_modules/basic-auth": { + "version": "2.0.1", + "resolved": "https://registry.npmjs.org/basic-auth/-/basic-auth-2.0.1.tgz", + "integrity": "sha512-NF+epuEdnUYVlGuhaxbbq+dvJttwLnGY+YixlXlME5KpQ5W3CnXA5cVTneY3SPbPDRkcjMbifrwmFYcClgOZeg==", + "dev": true, + "license": "MIT", + "dependencies": { + "safe-buffer": "5.1.2" + }, + "engines": { + "node": ">= 0.8" + } + }, + "node_modules/call-bind-apply-helpers": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/call-bind-apply-helpers/-/call-bind-apply-helpers-1.0.2.tgz", + "integrity": "sha512-Sp1ablJ0ivDkSzjcaJdxEunN5/XvksFJ2sMBFfq6x0ryhQV/2b/KwFe21cMpmHtPOSij8K99/wSfoEuTObmuMQ==", + "dev": true, + "license": "MIT", + "dependencies": { + "es-errors": "^1.3.0", + "function-bind": "^1.1.2" + }, + "engines": { + "node": ">= 0.4" + } + }, + "node_modules/call-bound": { + "version": "1.0.4", + "resolved": "https://registry.npmjs.org/call-bound/-/call-bound-1.0.4.tgz", + "integrity": "sha512-+ys997U96po4Kx/ABpBCqhA9EuxJaQWDQg7295H4hBphv3IZg0boBKuwYpt4YXp6MZ5AmZQnU/tyMTlRpaSejg==", + "dev": true, + "license": "MIT", + "dependencies": { + "call-bind-apply-helpers": "^1.0.2", + "get-intrinsic": "^1.3.0" + }, + "engines": { + "node": ">= 0.4" + }, + "funding": { + "url": "https://github.com/sponsors/ljharb" + } + }, + "node_modules/chalk": { + "version": "4.1.2", + "resolved": "https://registry.npmjs.org/chalk/-/chalk-4.1.2.tgz", + "integrity": "sha512-oKnbhFyRIXpUuez8iBMmyEa4nbj4IOQyuhc/wy9kY7/WVPcwIO9VA668Pu8RkO7+0G76SLROeyw9CpQ061i4mA==", + "dev": true, + "license": "MIT", + "dependencies": { + "ansi-styles": "^4.1.0", + "supports-color": "^7.1.0" + }, + "engines": { + "node": ">=10" + }, + "funding": { + "url": "https://github.com/chalk/chalk?sponsor=1" + } + }, + "node_modules/codemirror": { + "version": "6.0.2", + "resolved": "https://registry.npmjs.org/codemirror/-/codemirror-6.0.2.tgz", + "integrity": "sha512-VhydHotNW5w1UGK0Qj96BwSk/Zqbp9WbnyK2W/eVMv4QyF41INRGpjUhFJY7/uDNuudSc33a/PKr4iDqRduvHw==", + "license": "MIT", + "dependencies": { + "@codemirror/autocomplete": "^6.0.0", + "@codemirror/commands": "^6.0.0", + "@codemirror/language": "^6.0.0", + "@codemirror/lint": "^6.0.0", + "@codemirror/search": "^6.0.0", + "@codemirror/state": "^6.0.0", + "@codemirror/view": "^6.0.0" + } + }, + "node_modules/color-convert": { + "version": "2.0.1", + "resolved": "https://registry.npmjs.org/color-convert/-/color-convert-2.0.1.tgz", + "integrity": "sha512-RRECPsj7iu/xb5oKYcsFHSppFNnsj/52OVTRKb4zP5onXwVF3zVmmToNcOfGC+CRDpfK/U584fMg38ZHCaElKQ==", + "dev": true, + "license": "MIT", + "dependencies": { + "color-name": "~1.1.4" + }, + "engines": { + "node": ">=7.0.0" + } + }, + "node_modules/color-name": { + "version": "1.1.4", + "resolved": "https://registry.npmjs.org/color-name/-/color-name-1.1.4.tgz", + "integrity": "sha512-dOy+3AuW3a2wNbZHIuMZpTcgjGuLU/uBL/ubcZF9OXbDo8ff4O8yVp5Bf0efS8uEoYo5q4Fx7dY9OgQGXgAsQA==", + "dev": true, + "license": "MIT" + }, + "node_modules/corser": { + "version": "2.0.1", + "resolved": "https://registry.npmjs.org/corser/-/corser-2.0.1.tgz", + "integrity": "sha512-utCYNzRSQIZNPIcGZdQc92UVJYAhtGAteCFg0yRaFm8f0P+CPtyGyHXJcGXnffjCybUCEx3FQ2G7U3/o9eIkVQ==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">= 0.4.0" + } + }, + "node_modules/crelt": { + "version": "1.0.7", + "resolved": "https://registry.npmjs.org/crelt/-/crelt-1.0.7.tgz", + "integrity": "sha512-aK6BbWfhf4U/wCcLHKPJl/xa6VkVstRaPywWtMKGwuOLc/wZTyQYuoxgvZnNsBvv7Kg3YTBQYYBCggcviQczuA==", + "license": "MIT" + }, + "node_modules/debug": { + "version": "4.4.3", + "resolved": "https://registry.npmjs.org/debug/-/debug-4.4.3.tgz", + "integrity": "sha512-RGwwWnwQvkVfavKVt22FGLw+xYSdzARwm0ru6DhTVA3umU5hZc28V3kO4stgYryrTlLpuvgI9GiijltAjNbcqA==", + "dev": true, + "license": "MIT", + "dependencies": { + "ms": "^2.1.3" + }, + "engines": { + "node": ">=6.0" + }, + "peerDependenciesMeta": { + "supports-color": { + "optional": true + } + } + }, + "node_modules/dunder-proto": { + "version": "1.0.1", + "resolved": "https://registry.npmjs.org/dunder-proto/-/dunder-proto-1.0.1.tgz", + "integrity": "sha512-KIN/nDJBQRcXw0MLVhZE9iQHmG68qAVIBg9CqmUYjmQIhgij9U5MFvrqkUL5FbtyyzZuOeOt0zdeRe4UY7ct+A==", + "dev": true, + "license": "MIT", + "dependencies": { + "call-bind-apply-helpers": "^1.0.1", + "es-errors": "^1.3.0", + "gopd": "^1.2.0" + }, + "engines": { + "node": ">= 0.4" + } + }, + "node_modules/es-define-property": { + "version": "1.0.1", + "resolved": "https://registry.npmjs.org/es-define-property/-/es-define-property-1.0.1.tgz", + "integrity": "sha512-e3nRfgfUZ4rNGL232gUgX06QNyyez04KdjFrF+LTRoOXmrOgFKDg4BCdsjW8EnT69eqdYGmRpJwiPVYNrCaW3g==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">= 0.4" + } + }, + "node_modules/es-errors": { + "version": "1.3.0", + "resolved": "https://registry.npmjs.org/es-errors/-/es-errors-1.3.0.tgz", + "integrity": "sha512-Zf5H2Kxt2xjTvbJvP2ZWLEICxA6j+hAmMzIlypy4xcBg1vKVnx89Wy0GbS+kf5cwCVFFzdCFh2XSCFNULS6csw==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">= 0.4" + } + }, + "node_modules/es-object-atoms": { + "version": "1.1.2", + "resolved": "https://registry.npmjs.org/es-object-atoms/-/es-object-atoms-1.1.2.tgz", + "integrity": "sha512-HWcBoN6NileqtSydK2FqHbS/LoDd2pqrnQHLyJzBj4kOp/ky2MWMN694xOfkK8/SnUsW2DH7EfyVlydKCsm1Zw==", + "dev": true, + "license": "MIT", + "dependencies": { + "es-errors": "^1.3.0" + }, + "engines": { + "node": ">= 0.4" + } + }, + "node_modules/esbuild": { + "version": "0.25.10", + "resolved": "https://registry.npmjs.org/esbuild/-/esbuild-0.25.10.tgz", + "integrity": "sha512-9RiGKvCwaqxO2owP61uQ4BgNborAQskMR6QusfWzQqv7AZOg5oGehdY2pRJMTKuwxd1IDBP4rSbI5lHzU7SMsQ==", + "dev": true, + "hasInstallScript": true, + "license": "MIT", + "bin": { + "esbuild": "bin/esbuild" + }, + "engines": { + "node": ">=18" + }, + "optionalDependencies": { + "@esbuild/aix-ppc64": "0.25.10", + "@esbuild/android-arm": "0.25.10", + "@esbuild/android-arm64": "0.25.10", + "@esbuild/android-x64": "0.25.10", + "@esbuild/darwin-arm64": "0.25.10", + "@esbuild/darwin-x64": "0.25.10", + "@esbuild/freebsd-arm64": "0.25.10", + "@esbuild/freebsd-x64": "0.25.10", + "@esbuild/linux-arm": "0.25.10", + "@esbuild/linux-arm64": "0.25.10", + "@esbuild/linux-ia32": "0.25.10", + "@esbuild/linux-loong64": "0.25.10", + "@esbuild/linux-mips64el": "0.25.10", + "@esbuild/linux-ppc64": "0.25.10", + "@esbuild/linux-riscv64": "0.25.10", + "@esbuild/linux-s390x": "0.25.10", + "@esbuild/linux-x64": "0.25.10", + "@esbuild/netbsd-arm64": "0.25.10", + "@esbuild/netbsd-x64": "0.25.10", + "@esbuild/openbsd-arm64": "0.25.10", + "@esbuild/openbsd-x64": "0.25.10", + "@esbuild/openharmony-arm64": "0.25.10", + "@esbuild/sunos-x64": "0.25.10", + "@esbuild/win32-arm64": "0.25.10", + "@esbuild/win32-ia32": "0.25.10", + "@esbuild/win32-x64": "0.25.10" + } + }, + "node_modules/eventemitter3": { + "version": "4.0.7", + "resolved": "https://registry.npmjs.org/eventemitter3/-/eventemitter3-4.0.7.tgz", + "integrity": "sha512-8guHBZCwKnFhYdHr2ysuRWErTwhoN2X8XELRlrRwpmfeY2jjuUN4taQMsULKUVo1K4DvZl+0pgfyoysHxvmvEw==", + "dev": true, + "license": "MIT" + }, + "node_modules/follow-redirects": { + "version": "1.16.1", + "resolved": "https://registry.npmjs.org/follow-redirects/-/follow-redirects-1.16.1.tgz", + "integrity": "sha512-FNvFGzoMLWmE6Yj9spb/zjd7yiNCHiAW9/Tg9CXrQ8wuu32HtlJOwWO11OJafl5FfY3DxTdQ0vj42zU1kvv5jg==", + "dev": true, + "funding": [ + { + "type": "individual", + "url": "https://github.com/sponsors/RubenVerborgh" + } + ], + "license": "MIT", + "engines": { + "node": ">=4.0" + }, + "peerDependenciesMeta": { + "debug": { + "optional": true + } + } + }, + "node_modules/function-bind": { + "version": "1.1.2", + "resolved": "https://registry.npmjs.org/function-bind/-/function-bind-1.1.2.tgz", + "integrity": "sha512-7XHNxH7qX9xG5mIwxkhumTox/MIRNcOgDrxWsMt2pAr23WHp6MrRlN7FBSFpCpr+oVO0F744iUgR82nJMfG2SA==", + "dev": true, + "license": "MIT", + "funding": { + "url": "https://github.com/sponsors/ljharb" + } + }, + "node_modules/get-intrinsic": { + "version": "1.3.0", + "resolved": "https://registry.npmjs.org/get-intrinsic/-/get-intrinsic-1.3.0.tgz", + "integrity": "sha512-9fSjSaos/fRIVIp+xSJlE6lfwhES7LNtKaCBIamHsjr2na1BiABJPo0mOjjz8GJDURarmCPGqaiVg5mfjb98CQ==", + "dev": true, + "license": "MIT", + "dependencies": { + "call-bind-apply-helpers": "^1.0.2", + "es-define-property": "^1.0.1", + "es-errors": "^1.3.0", + "es-object-atoms": "^1.1.1", + "function-bind": "^1.1.2", + "get-proto": "^1.0.1", + "gopd": "^1.2.0", + "has-symbols": "^1.1.0", + "hasown": "^2.0.2", + "math-intrinsics": "^1.1.0" + }, + "engines": { + "node": ">= 0.4" + }, + "funding": { + "url": "https://github.com/sponsors/ljharb" + } + }, + "node_modules/get-proto": { + "version": "1.0.1", + "resolved": "https://registry.npmjs.org/get-proto/-/get-proto-1.0.1.tgz", + "integrity": "sha512-sTSfBjoXBp89JvIKIefqw7U2CCebsc74kiY6awiGogKtoSGbgjYE/G/+l9sF3MWFPNc9IcoOC4ODfKHfxFmp0g==", + "dev": true, + "license": "MIT", + "dependencies": { + "dunder-proto": "^1.0.1", + "es-object-atoms": "^1.0.0" + }, + "engines": { + "node": ">= 0.4" + } + }, + "node_modules/gopd": { + "version": "1.2.0", + "resolved": "https://registry.npmjs.org/gopd/-/gopd-1.2.0.tgz", + "integrity": "sha512-ZUKRh6/kUFoAiTAtTYPZJ3hw9wNxx+BIBOijnlG9PnrJsCcSjs1wyyD6vJpaYtgnzDrKYRSqf3OO6Rfa93xsRg==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">= 0.4" + }, + "funding": { + "url": "https://github.com/sponsors/ljharb" + } + }, + "node_modules/has-flag": { + "version": "4.0.0", + "resolved": "https://registry.npmjs.org/has-flag/-/has-flag-4.0.0.tgz", + "integrity": "sha512-EykJT/Q1KjTWctppgIAgfSO0tKVuZUjhgMr17kqTumMl6Afv3EISleU7qZUzoXDFTAHTDC4NOoG/ZxU3EvlMPQ==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">=8" + } + }, + "node_modules/has-symbols": { + "version": "1.1.0", + "resolved": "https://registry.npmjs.org/has-symbols/-/has-symbols-1.1.0.tgz", + "integrity": "sha512-1cDNdwJ2Jaohmb3sg4OmKaMBwuC48sYni5HUw2DvsC8LjGTLK9h+eb1X6RyuOHe4hT0ULCW68iomhjUoKUqlPQ==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">= 0.4" + }, + "funding": { + "url": "https://github.com/sponsors/ljharb" + } + }, + "node_modules/hasown": { + "version": "2.0.4", + "resolved": "https://registry.npmjs.org/hasown/-/hasown-2.0.4.tgz", + "integrity": "sha512-T2UbfbBEF32wiepXIsMlTW9+dDYC6wMh/t/vYA4tuOMKqWz/n3vr1NFSxQiyP+zk2mXsoMA/i/7qV6LKut1t1A==", + "dev": true, + "license": "MIT", + "dependencies": { + "function-bind": "^1.1.2" + }, + "engines": { + "node": ">= 0.4" + } + }, + "node_modules/he": { + "version": "1.2.0", + "resolved": "https://registry.npmjs.org/he/-/he-1.2.0.tgz", + "integrity": "sha512-F/1DnUGPopORZi0ni+CvrCgHQ5FyEAHRLSApuYWMmrbSwoN2Mn/7k+Gl38gJnR7yyDZk6WLXwiGod1JOWNDKGw==", + "dev": true, + "license": "MIT", + "bin": { + "he": "bin/he" + } + }, + "node_modules/html-encoding-sniffer": { + "version": "3.0.0", + "resolved": "https://registry.npmjs.org/html-encoding-sniffer/-/html-encoding-sniffer-3.0.0.tgz", + "integrity": "sha512-oWv4T4yJ52iKrufjnyZPkrN0CH3QnrUqdB6In1g5Fe1mia8GmF36gnfNySxoZtxD5+NmYw1EElVXiBk93UeskA==", + "dev": true, + "license": "MIT", + "dependencies": { + "whatwg-encoding": "^2.0.0" + }, + "engines": { + "node": ">=12" + } + }, + "node_modules/http-proxy": { + "version": "1.18.1", + "resolved": "https://registry.npmjs.org/http-proxy/-/http-proxy-1.18.1.tgz", + "integrity": "sha512-7mz/721AbnJwIVbnaSv1Cz3Am0ZLT/UBwkC92VlxhXv/k/BBQfM2fXElQNC27BVGr0uwUpplYPQM9LnaBMR5NQ==", + "dev": true, + "license": "MIT", + "dependencies": { + "eventemitter3": "^4.0.0", + "follow-redirects": "^1.0.0", + "requires-port": "^1.0.0" + }, + "engines": { + "node": ">=8.0.0" + } + }, + "node_modules/http-server": { + "version": "14.1.1", + "resolved": "https://registry.npmjs.org/http-server/-/http-server-14.1.1.tgz", + "integrity": "sha512-+cbxadF40UXd9T01zUHgA+rlo2Bg1Srer4+B4NwIHdaGxAGGv59nYRnGGDJ9LBk7alpS0US+J+bLLdQOOkJq4A==", + "dev": true, + "license": "MIT", + "dependencies": { + "basic-auth": "^2.0.1", + "chalk": "^4.1.2", + "corser": "^2.0.1", + "he": "^1.2.0", + "html-encoding-sniffer": "^3.0.0", + "http-proxy": "^1.18.1", + "mime": "^1.6.0", + "minimist": "^1.2.6", + "opener": "^1.5.1", + "portfinder": "^1.0.28", + "secure-compare": "3.0.1", + "union": "~0.5.0", + "url-join": "^4.0.1" + }, + "bin": { + "http-server": "bin/http-server" + }, + "engines": { + "node": ">=12" + } + }, + "node_modules/iconv-lite": { + "version": "0.6.3", + "resolved": "https://registry.npmjs.org/iconv-lite/-/iconv-lite-0.6.3.tgz", + "integrity": "sha512-4fCk79wshMdzMp2rH06qWrJE4iolqLhCUH+OiuIgU++RB0+94NlDL81atO7GX55uUKueo0txHNtvEyI6D7WdMw==", + "dev": true, + "license": "MIT", + "dependencies": { + "safer-buffer": ">= 2.1.2 < 3.0.0" + }, + "engines": { + "node": ">=0.10.0" + } + }, + "node_modules/math-intrinsics": { + "version": "1.1.0", + "resolved": "https://registry.npmjs.org/math-intrinsics/-/math-intrinsics-1.1.0.tgz", + "integrity": "sha512-/IXtbwEk5HTPyEwyKX6hGkYXxM9nbj64B+ilVJnC/R6B0pH5G4V3b0pVbL7DBj4tkhBAppbQUlf6F6Xl9LHu1g==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">= 0.4" + } + }, + "node_modules/mime": { + "version": "1.6.0", + "resolved": "https://registry.npmjs.org/mime/-/mime-1.6.0.tgz", + "integrity": "sha512-x0Vn8spI+wuJ1O6S7gnbaQg8Pxh4NNHb7KSINmEWKiPE4RKOplvijn+NkmYmmRgP68mc70j2EbeTFRsrswaQeg==", + "dev": true, + "license": "MIT", + "bin": { + "mime": "cli.js" + }, + "engines": { + "node": ">=4" + } + }, + "node_modules/minimist": { + "version": "1.2.8", + "resolved": "https://registry.npmjs.org/minimist/-/minimist-1.2.8.tgz", + "integrity": "sha512-2yyAR8qBkN3YuheJanUpWC5U3bb5osDywNB8RzDVlDwDHbocAJveqqj1u8+SVD7jkWT4yvsHCpWqqWqAxb0zCA==", + "dev": true, + "license": "MIT", + "funding": { + "url": "https://github.com/sponsors/ljharb" + } + }, + "node_modules/ms": { + "version": "2.1.3", + "resolved": "https://registry.npmjs.org/ms/-/ms-2.1.3.tgz", + "integrity": "sha512-6FlzubTLZG3J2a/NVCAleEhjzq5oxgHyaCU9yYXvcLsvoVaHJq/s5xXI6/XXP6tz7R9xAOtHnSO/tXtF3WRTlA==", + "dev": true, + "license": "MIT" + }, + "node_modules/object-inspect": { + "version": "1.13.4", + "resolved": "https://registry.npmjs.org/object-inspect/-/object-inspect-1.13.4.tgz", + "integrity": "sha512-W67iLl4J2EXEGTbfeHCffrjDfitvLANg0UlX3wFUUSTx92KXRFegMHUVgSqE+wvhAbi4WqjGg9czysTV2Epbew==", + "dev": true, + "license": "MIT", + "engines": { + "node": ">= 0.4" + }, + "funding": { + "url": "https://github.com/sponsors/ljharb" + } + }, + "node_modules/opener": { + "version": "1.5.2", + "resolved": "https://registry.npmjs.org/opener/-/opener-1.5.2.tgz", + "integrity": "sha512-ur5UIdyw5Y7yEj9wLzhqXiy6GZ3Mwx0yGI+5sMn2r0N0v3cKJvUmFH5yPP+WXh9e0xfyzyJX95D8l088DNFj7A==", + "dev": true, + "license": "(WTFPL OR MIT)", + "bin": { + "opener": "bin/opener-bin.js" + } + }, + "node_modules/portfinder": { + "version": "1.0.38", + "resolved": "https://registry.npmjs.org/portfinder/-/portfinder-1.0.38.tgz", + "integrity": "sha512-rEwq/ZHlJIKw++XtLAO8PPuOQA/zaPJOZJ37BVuN97nLpMJeuDVLVGRwbFoBgLudgdTMP2hdRJP++H+8QOA3vg==", + "dev": true, + "license": "MIT", + "dependencies": { + "async": "^3.2.6", + "debug": "^4.3.6" + }, + "engines": { + "node": ">= 10.12" + } + }, + "node_modules/qs": { + "version": "6.16.0", + "resolved": "https://registry.npmjs.org/qs/-/qs-6.16.0.tgz", + "integrity": "sha512-h6fhOIaRrID2CbEY2fqs+7t+UXZo+MLAnU5gRIq85uFtdiUPCdsApMlHhXogKVM4HM2DVbIjGNTTYH2OcmP1vA==", + "dev": true, + "license": "BSD-3-Clause", + "dependencies": { + "es-define-property": "^1.0.1", + "side-channel": "^1.1.1" + }, + "engines": { + "node": ">=0.6" + }, + "funding": { + "url": "https://github.com/sponsors/ljharb" + } + }, + "node_modules/requires-port": { + "version": "1.0.0", + "resolved": "https://registry.npmjs.org/requires-port/-/requires-port-1.0.0.tgz", + "integrity": "sha512-KigOCHcocU3XODJxsu8i/j8T9tzT4adHiecwORRQ0ZZFcp7ahwXuRU1m+yuO90C5ZUyGeGfocHDI14M3L3yDAQ==", + "dev": true, + "license": "MIT" + }, + "node_modules/safe-buffer": { + "version": "5.1.2", + "resolved": "https://registry.npmjs.org/safe-buffer/-/safe-buffer-5.1.2.tgz", + "integrity": "sha512-Gd2UZBJDkXlY7GbJxfsE8/nvKkUEU1G38c1siN6QP6a9PT9MmHB8GnpscSmMJSoF8LOIrt8ud/wPtojys4G6+g==", + "dev": true, + "license": "MIT" + }, + "node_modules/safer-buffer": { + "version": "2.1.2", + "resolved": "https://registry.npmjs.org/safer-buffer/-/safer-buffer-2.1.2.tgz", + "integrity": "sha512-YZo3K82SD7Riyi0E1EQPojLz7kpepnSQI9IyPbHHg1XXXevb5dJI7tpyN2ADxGcQbHG7vcyRHk0cbwqcQriUtg==", + "dev": true, + "license": "MIT" + }, + "node_modules/secure-compare": { + "version": "3.0.1", + "resolved": "https://registry.npmjs.org/secure-compare/-/secure-compare-3.0.1.tgz", + "integrity": "sha512-AckIIV90rPDcBcglUwXPF3kg0P0qmPsPXAj6BBEENQE1p5yA1xfmDJzfi1Tappj37Pv2mVbKpL3Z1T+Nn7k1Qw==", + "dev": true, + "license": "MIT" + }, + "node_modules/side-channel": { + "version": "1.1.1", + "resolved": "https://registry.npmjs.org/side-channel/-/side-channel-1.1.1.tgz", + "integrity": "sha512-6x6dK6zJdpTzF4sQeNYxwtvBzf6Eg4GtlesS94HOvTudUeyK2WXAaIfmDgsyslYrRBeFIlsi54AYsFGUuhmvrQ==", + "dev": true, + "license": "MIT", + "dependencies": { + "es-errors": "^1.3.0", + "object-inspect": "^1.13.4", + "side-channel-list": "^1.0.1", + "side-channel-map": "^1.0.1", + "side-channel-weakmap": "^1.0.2" + }, + "engines": { + "node": ">= 0.4" + }, + "funding": { + "url": "https://github.com/sponsors/ljharb" + } + }, + "node_modules/side-channel-list": { + "version": "1.0.1", + "resolved": "https://registry.npmjs.org/side-channel-list/-/side-channel-list-1.0.1.tgz", + "integrity": "sha512-mjn/0bi/oUURjc5Xl7IaWi/OJJJumuoJFQJfDDyO46+hBWsfaVM65TBHq2eoZBhzl9EchxOijpkbRC8SVBQU0w==", + "dev": true, + "license": "MIT", + "dependencies": { + "es-errors": "^1.3.0", + "object-inspect": "^1.13.4" + }, + "engines": { + "node": ">= 0.4" + }, + "funding": { + "url": "https://github.com/sponsors/ljharb" + } + }, + "node_modules/side-channel-map": { + "version": "1.0.1", + "resolved": "https://registry.npmjs.org/side-channel-map/-/side-channel-map-1.0.1.tgz", + "integrity": "sha512-VCjCNfgMsby3tTdo02nbjtM/ewra6jPHmpThenkTYh8pG9ucZ/1P8So4u4FGBek/BjpOVsDCMoLA/iuBKIFXRA==", + "dev": true, + "license": "MIT", + "dependencies": { + "call-bound": "^1.0.2", + "es-errors": "^1.3.0", + "get-intrinsic": "^1.2.5", + "object-inspect": "^1.13.3" + }, + "engines": { + "node": ">= 0.4" + }, + "funding": { + "url": "https://github.com/sponsors/ljharb" + } + }, + "node_modules/side-channel-weakmap": { + "version": "1.0.2", + "resolved": "https://registry.npmjs.org/side-channel-weakmap/-/side-channel-weakmap-1.0.2.tgz", + "integrity": "sha512-WPS/HvHQTYnHisLo9McqBHOJk2FkHO/tlpvldyrnem4aeQp4hai3gythswg6p01oSoTl58rcpiFAjF2br2Ak2A==", + "dev": true, + "license": "MIT", + "dependencies": { + "call-bound": "^1.0.2", + "es-errors": "^1.3.0", + "get-intrinsic": "^1.2.5", + "object-inspect": "^1.13.3", + "side-channel-map": "^1.0.1" + }, + "engines": { + "node": ">= 0.4" + }, + "funding": { + "url": "https://github.com/sponsors/ljharb" + } + }, + "node_modules/style-mod": { + "version": "4.1.4", + "resolved": "https://registry.npmjs.org/style-mod/-/style-mod-4.1.4.tgz", + "integrity": "sha512-XXWIQt633/EpAFx8aZDOTjBzrCaGmhvEQlQo6MVPfa2OzO2cWo+4hV9h+6UkHYlXGfy+ODXKUdP7Pthmcu5ATw==", + "license": "MIT" + }, + "node_modules/supports-color": { + "version": "7.2.0", + "resolved": "https://registry.npmjs.org/supports-color/-/supports-color-7.2.0.tgz", + "integrity": "sha512-qpCAvRl9stuOHveKsn7HncJRvv501qIacKzQlO/+Lwxc9+0q2wLyv4Dfvt80/DPn2pqOBsJdDiogXGR9+OvwRw==", + "dev": true, + "license": "MIT", + "dependencies": { + "has-flag": "^4.0.0" + }, + "engines": { + "node": ">=8" + } + }, + "node_modules/tslib": { + "version": "2.8.1", + "resolved": "https://registry.npmjs.org/tslib/-/tslib-2.8.1.tgz", + "integrity": "sha512-oJFu94HQb+KVduSUQL7wnpmqnfmLsOA/nAh6b6EH0wCEoK0/mPeXU6c3wKDV83MkOuHPRHtSXKKU99IBazS/2w==", + "dev": true, + "license": "0BSD" + }, + "node_modules/union": { + "version": "0.5.0", + "resolved": "https://registry.npmjs.org/union/-/union-0.5.0.tgz", + "integrity": "sha512-N6uOhuW6zO95P3Mel2I2zMsbsanvvtgn6jVqJv4vbVcz/JN0OkL9suomjQGmWtxJQXOCqUJvquc1sMeNz/IwlA==", + "dev": true, + "dependencies": { + "qs": "^6.4.0" + }, + "engines": { + "node": ">= 0.8.0" + } + }, + "node_modules/url-join": { + "version": "4.0.1", + "resolved": "https://registry.npmjs.org/url-join/-/url-join-4.0.1.tgz", + "integrity": "sha512-jk1+QP6ZJqyOiuEI9AEWQfju/nB2Pw466kbA0LEZljHwKeMgd9WrAEgEGxjPDD2+TNbbb37rTyhEfrCXfuKXnA==", + "dev": true, + "license": "MIT" + }, + "node_modules/w3c-keyname": { + "version": "2.2.8", + "resolved": "https://registry.npmjs.org/w3c-keyname/-/w3c-keyname-2.2.8.tgz", + "integrity": "sha512-dpojBhNsCNN7T82Tm7k26A6G9ML3NkhDsnw9n/eoxSRlVBB4CEtIQ/KTCLI2Fwf3ataSXRhYFkQi3SlnFwPvPQ==", + "license": "MIT" + }, + "node_modules/whatwg-encoding": { + "version": "2.0.0", + "resolved": "https://registry.npmjs.org/whatwg-encoding/-/whatwg-encoding-2.0.0.tgz", + "integrity": "sha512-p41ogyeMUrw3jWclHWTQg1k05DSVXPLcVxRTYsXUk+ZooOCZLcoYgPZ/HL/D/N+uQPOtcp1me1WhBEaX02mhWg==", + "deprecated": "Use @exodus/bytes instead for a more spec-conformant and faster implementation", + "dev": true, + "license": "MIT", + "dependencies": { + "iconv-lite": "0.6.3" + }, + "engines": { + "node": ">=12" + } + }, + "node_modules/z3-solver": { + "version": "4.16.0", + "resolved": "https://registry.npmjs.org/z3-solver/-/z3-solver-4.16.0.tgz", + "integrity": "sha512-vWT+I5Yz0dXtseLVZsnkwAIrRmbxw0rCX5a6Xglc6n1CyPESNMnHB3iAWh7XTQQHZRlpWYnKJXTJ0ahTTNHZEg==", + "dev": true, + "license": "MIT", + "dependencies": { + "async-mutex": "^0.3.2" + }, + "engines": { + "node": ">=16" + } + } + } +} diff --git a/package.json b/package.json new file mode 100644 index 0000000..663980c --- /dev/null +++ b/package.json @@ -0,0 +1,19 @@ +{ + "name": "liquidjava-docs", + "private": true, + "scripts": { + "build:playground": "python3 scripts/playground/build.py && node scripts/playground/build.mjs", + "test:playground": "node --test scripts/playground/*.test.mjs", + "serve:playground": "bundle exec jekyll build --baseurl \"\" && http-server _site -a 127.0.0.1 -p 8770 -c-1" + }, + "devDependencies": { + "esbuild": "0.25.10", + "http-server": "14.1.1", + "z3-solver": "4.16.0" + }, + "dependencies": { + "@codemirror/lang-java": "6.0.2", + "@codemirror/lint": "6.8.5", + "codemirror": "6.0.2" + } +} diff --git a/pages/index.md b/pages/index.md index 4375c71..62c13d9 100644 --- a/pages/index.md +++ b/pages/index.md @@ -10,6 +10,7 @@ description: Documentation for LiquidJava, a lightweight verification system for

Extending Java with Liquid Types

LiquidJava is an additional type system for Java that uses liquid types to express constraints programs must follow, helping catch more bugs before they run.

+

Try LiquidJava in your browser

LiquidJava banner diff --git a/playground/editor.css b/playground/editor.css new file mode 100644 index 0000000..2bac767 --- /dev/null +++ b/playground/editor.css @@ -0,0 +1,17 @@ +.lj-playground { border: 1px solid var(--border-color, #d7dce2); border-radius: 8px; overflow: hidden; margin: 1.5rem 0; } +.lj-toolbar { display: flex; align-items: center; flex-wrap: wrap; gap: .6rem; padding: 1rem; background: #f5f7fa; } +.lj-toolbar label { font-weight: 600; } +.lj-toolbar select { font: inherit; max-width: 100%; padding: .35rem; border: 1px solid #bbc4ce; border-radius: 4px; background: white; } +.lj-toolbar button:disabled { opacity: .5; cursor: default; } +.lj-playground .cm-editor { font-size: 14px; background: #fff; } +.lj-playground .cm-scroller { min-height: 300px; max-height: 560px; overflow: auto; font-family: 'JetBrains Mono', monospace; } +.lj-playground .cm-focused { outline: 2px solid #1269a8; outline-offset: -2px; } +#lj-status { margin: 0; padding: 1rem; border-top: 1px solid #d7dce2; font-size: .9rem; } +#lj-status[data-state="success"] { color: #156b35; background: #eef9f1; } +#lj-status[data-state="error"], #lj-status[data-state="failure"] { color: #9b2323; background: #fff1f1; } +.lj-issue { padding: 1rem; border-top: 1px solid #d7dce2; } +.lj-issue h3 { margin: 0 0 .5rem; font-size: 1rem; } +.lj-issue p { margin: .5rem 0; white-space: pre-wrap; } +.lj-issue pre { white-space: pre-wrap; margin: .5rem 0; } +.lj-issue button { font: inherit; border: 0; padding: 0; background: transparent; color: #1269a8; cursor: pointer; text-decoration: underline; } +@media (max-width: 600px) { .lj-toolbar { gap: .5rem; padding: .75rem; } .lj-playground .cm-editor { font-size: 12px; } } diff --git a/playground/index.md b/playground/index.md new file mode 100644 index 0000000..1325384 --- /dev/null +++ b/playground/index.md @@ -0,0 +1,35 @@ +--- +title: Playground +nav_order: 1.5 +permalink: /playground/ +has_toc: false +description: Try LiquidJava refinements and typestates directly in your browser. +--- + +# Playground + +Edit an example and select **Verify** to check it with LiquidJava. Verification runs in your browser; your code is not sent to a server. The first check downloads the verifier and may take a moment. + + +
+
+ + + + + +
+
+

Choose an example or edit the code, then verify. Ctrl+Enter / ⌘+Enter also verifies.

+
+ +
+ +The playground checks one Java file using Java 8 syntax, with the bundled LiquidJava annotations and core Java types. External dependencies are not supported. For projects, use the [VS Code extension]({{ '/vscode-extension/' | relative_url }}). + + diff --git a/playground/isolation.js b/playground/isolation.js new file mode 100644 index 0000000..aef32c9 --- /dev/null +++ b/playground/isolation.js @@ -0,0 +1,14 @@ +// GitHub Pages cannot set these response headers; isolate only the playground. +self.addEventListener('install', () => self.skipWaiting()); +self.addEventListener('activate', event => event.waitUntil(self.clients.claim())); +self.addEventListener('fetch', event => { + if (new URL(event.request.url).origin !== self.location.origin) return; + event.respondWith((async () => { + const response = await fetch(event.request); + if (response.type === 'opaque') return response; + const headers = new Headers(response.headers); + headers.set('Cross-Origin-Opener-Policy', 'same-origin'); + headers.set('Cross-Origin-Embedder-Policy', 'require-corp'); + return new Response(response.body, { status: response.status, statusText: response.statusText, headers }); + })()); +}); diff --git a/scripts/playground/adapter.mjs b/scripts/playground/adapter.mjs new file mode 100644 index 0000000..e0875ab --- /dev/null +++ b/scripts/playground/adapter.mjs @@ -0,0 +1,34 @@ +export function createNatives(Z3, methods) { + const natives = { Java_com_microsoft_z3_Native_setInternalErrorHandler() {} }; + for (const { name, types, api } of methods) { + natives[`Java_com_microsoft_z3_Native_${name}`] = async (_lib, ...args) => { + const input = args.map((value, i) => types[i] === 'long' ? Number(value) : value); + // numeric int64 arguments are values, whereas other longs are WASM pointers + if (api === 'mk_int64' || api === 'mk_unsigned_int64') input[1] = BigInt(args[1]); + if (api === 'model_eval') { + const value = await Z3.model_eval(...input.slice(0, 4)); + if (value === null) return false; + args[4].value = value; + return true; + } + if (types.some(type => type.endsWith('Ptr'))) { + throw new Error(`Unsupported Z3 output parameter: ${api}`); + } + // the JS binding derives array counts from the array itself + for (let i = types.length - 1; i >= 1; i--) { + if (types[i] === 'long[]' && types[i - 1] === 'int') { + input[i] = Array.from(input[i], Number); + input.splice(i - 1, 1); + } + } + if (typeof Z3[api] !== 'function') throw new Error(`Unsupported Z3 operation: ${api}`); + const result = await Z3[api](...input); + // the desktop verifier treats unknown as success; the playground must not + if ((api === 'solver_check' || api === 'solver_check_assumptions') && result === 0) { + throw new Error('Z3 could not determine whether this refinement holds.'); + } + return result; + }; + } + return natives; +} diff --git a/scripts/playground/adapter.test.mjs b/scripts/playground/adapter.test.mjs new file mode 100644 index 0000000..ab41234 --- /dev/null +++ b/scripts/playground/adapter.test.mjs @@ -0,0 +1,51 @@ +import test from 'node:test'; +import assert from 'node:assert/strict'; +import { readFile } from 'node:fs/promises'; +import z3 from 'z3-solver'; +const { init } = z3; +import { createNatives } from './adapter.mjs'; + +const methods = JSON.parse(await readFile(new URL('../../playground/runtime/native-methods.json', import.meta.url))); + +test('existing Java ABI checks bounds, evaluates models and passes counted arrays to WASM', async () => { + const { Z3, em } = await init(); + const natives = createNatives(Z3, methods); + const call = (name, ...args) => natives[`Java_com_microsoft_z3_Native_INTERNAL${name}`](null, ...args); + const ctx = await call('mkContext', 0); + try { + const sort = await call('mkIntSort', ctx); + const name = await call('mkStringSymbol', ctx, 'x'); + const x = await call('mkConst', ctx, name, sort); + const zero = await call('mkInt', ctx, 0, sort); + const two = await call('mkInt', ctx, 2, sort); + const large = await call('mkInt64', ctx, 9007199254740993n, sort); + assert.equal(await call('getNumeralString', ctx, large), '9007199254740993'); + const lower = await call('mkGt', ctx, x, zero); + const upper = await call('mkLt', ctx, x, two); + const bounds = await call('mkAnd', ctx, 2, new BigInt64Array([BigInt(lower), BigInt(upper)])); + const solver = await call('mkSolver', ctx); + await call('solverIncRef', ctx, solver); + await call('solverAssert', ctx, solver, bounds); + assert.equal(await call('solverCheck', ctx, solver), 1); + const model = await call('solverGetModel', ctx, solver); + const output = { value: 0 }; + assert.equal(await call('modelEval', ctx, model, x, true, output), true); + assert.equal(await call('getNumeralString', ctx, output.value), '1'); + await call('solverAssert', ctx, solver, await call('mkLt', ctx, x, zero)); + assert.equal(await call('solverCheck', ctx, solver), -1); + await call('solverDecRef', ctx, solver); + } finally { + await call('delContext', ctx); + em.PThread.terminateAllThreads(); + } +}); + +test('an unknown solver result cannot become a successful verification', async () => { + const natives = createNatives({ solver_check: async () => 0 }, methods); + await assert.rejects(natives.Java_com_microsoft_z3_Native_INTERNALsolverCheck(null, 1, 2), /could not determine/); +}); + +test('unimplemented ABI operations fail explicitly', async () => { + const natives = createNatives({}, methods); + await assert.rejects(natives.Java_com_microsoft_z3_Native_INTERNALgetNumeralInt(null, 1, 2, { value: 0 }), /Unsupported Z3 output parameter/); +}); diff --git a/scripts/playground/build.mjs b/scripts/playground/build.mjs new file mode 100644 index 0000000..298f3f7 --- /dev/null +++ b/scripts/playground/build.mjs @@ -0,0 +1,8 @@ +import { build } from 'esbuild'; +import { copyFile } from 'node:fs/promises'; +const output = 'playground/runtime'; +await build({ entryPoints: ['scripts/playground/worker.js'], bundle: true, format: 'iife', platform: 'browser', outfile: `${output}/worker.js` }); +await build({ entryPoints: ['scripts/playground/editor.js'], bundle: true, format: 'esm', platform: 'browser', outfile: `${output}/editor.js` }); +for (const file of ['z3-built.js', 'z3-built.wasm']) { + await copyFile(`node_modules/z3-solver/build/${file}`, `${output}/${file}`); +} diff --git a/scripts/playground/build.py b/scripts/playground/build.py new file mode 100644 index 0000000..d4ea394 --- /dev/null +++ b/scripts/playground/build.py @@ -0,0 +1,97 @@ +"""Build the browser runner from unmodified published LiquidJava sources.""" +import json +import re +import subprocess +import shutil +import urllib.request +import zipfile +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +WORK = ROOT / '.playground-build' +OUTPUT = ROOT / 'playground/runtime' +VERIFIER = '0.0.35' +API = '0.0.7' +Z3 = '4.8.17' +SPOON = '10.4.2' + + +def artifact(group, name, version, classifier=''): + filename = f'{name}-{version}{classifier}.jar' + target = WORK / filename + if not target.exists(): + url = f'https://repo.maven.apache.org/maven2/{group.replace(".", "/")}/{name}/{version}/{filename}' + print(f'Downloading {filename}', flush=True) + urllib.request.urlretrieve(url, target) + return target + + +def main(): + properties = subprocess.run(['java', '-XshowSettings:properties', '-version'], capture_output=True, text=True, check=True).stderr + java_home = Path(re.search(r'java.home = (.+)', properties).group(1).strip()) + if not re.search(r'java.version = 17[.\s]', properties): + raise RuntimeError('Build the playground with JDK 17 (set JAVA_HOME and PATH)') + WORK.mkdir(exist_ok=True) + OUTPUT.mkdir(parents=True, exist_ok=True) + verifier = artifact('io.github.liquid-java', 'liquidjava-verifier', VERIFIER) + sources = artifact('io.github.liquid-java', 'liquidjava-verifier', VERIFIER, '-sources') + annotations = artifact('io.github.liquid-java', 'liquidjava-api', API, '-sources') + z3_sources = artifact('tools.aqua', 'z3-turnkey', Z3, '-sources') + spoon_sources = artifact('fr.inria.gforge.spoon', 'spoon-core', SPOON, '-sources') + source_dir = WORK / 'sources' + if source_dir.exists(): + shutil.rmtree(source_dir) + source_dir.mkdir() + for source in [sources, annotations]: + with zipfile.ZipFile(source) as jar: + for item in jar.namelist(): + if item.endswith('.java'): + path = source_dir / item + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(jar.read(item)) + # CheerpJ casts can have empty stack traces. Select Spoon's existing + # exotic-JVM query mode rather than failing its static initialization. + query_path = 'spoon/reflect/visitor/chain/CtQueryImpl.java' + with zipfile.ZipFile(spoon_sources) as jar: + query = jar.read(query_path).decode() + original = 'StackTraceElement[] stack = e.getStackTrace();' + if query.count(original) != 1: + raise RuntimeError('Spoon query adaptation no longer matches its source') + query = query.replace(original, original + '\n\t\t\tif (stack.length == 0) return -1;') + path = source_dir / query_path + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text(query) + classes = WORK / 'classes' + if classes.exists(): + shutil.rmtree(classes) + classes.mkdir() + files = list(source_dir.rglob('*.java')) + list((ROOT / 'scripts/playground/java').rglob('*.java')) + args = WORK / 'javac.args' + args.write_text('\n'.join('"' + str(file) + '"' for file in files)) + subprocess.run(['javac', '--release', '17', '-cp', str(verifier), '-d', str(classes), '@' + str(args)], check=True) + with zipfile.ZipFile(verifier) as jar, zipfile.ZipFile(OUTPUT / 'liquidjava.jar', 'w', zipfile.ZIP_DEFLATED) as out: + for item in jar.infolist(): + # replace compiled classes, keep the remaining dependencies and resources + if (classes / item.filename).is_file() or item.filename.endswith(('.dll', '.so', '.dylib')): + continue + if item.filename.startswith('META-INF/versions/') or item.filename.endswith(('.SF', '.RSA', '.DSA')): + continue + out.writestr(item.filename, jar.read(item.filename)) + for file in classes.rglob('*.class'): + out.writestr(file.relative_to(classes).as_posix(), file.read_bytes()) + with zipfile.ZipFile(java_home / 'jmods/java.base.jmod') as jar, zipfile.ZipFile(OUTPUT / 'java-base.jar', 'w', zipfile.ZIP_DEFLATED) as out: + for name in jar.namelist(): + if name.startswith('classes/') and name.endswith('.class') and name != 'classes/module-info.class': + out.writestr(name[len('classes/'):], jar.read(name)) + with zipfile.ZipFile(z3_sources) as jar: + native = jar.read('com/microsoft/z3/Native.java').decode() + methods = [] + for name, params in re.findall(r'native\s+\w+\s+(INTERNAL\w+)\(([^)]*)\)', native): + types = [param.strip().split()[0] for param in params.split(',') if param.strip()] + api = re.sub(r'([a-z0-9])([A-Z])', r'\1_\2', name[len('INTERNAL'):]).lower() + methods.append(dict(name=name, types=types, api=api)) + (OUTPUT / 'native-methods.json').write_text(json.dumps(methods)) + + +if __name__ == '__main__': + main() diff --git a/scripts/playground/editor.js b/scripts/playground/editor.js new file mode 100644 index 0000000..52d0ce9 --- /dev/null +++ b/scripts/playground/editor.js @@ -0,0 +1,123 @@ +import { EditorView, basicSetup } from 'codemirror'; +import { java } from '@codemirror/lang-java'; +import { setDiagnostics } from '@codemirror/lint'; +import { examples } from './examples.mjs'; + +const root = document.querySelector('#lj-playground'); +const example = document.querySelector('#lj-example'); +const verify = document.querySelector('#lj-verify'); +const stop = document.querySelector('#lj-stop'); +const status = document.querySelector('#lj-status'); +const results = document.querySelector('#lj-results'); +const runtime = new URL(root.dataset.runtime, location.href); +let worker; +let loading = false; +let checking = false; +let source; +let timer; +const view = new EditorView({ + doc: examples.positive, + extensions: [basicSetup, java(), EditorView.contentAttributes.of({ 'aria-label': 'Java source code' }), + EditorView.updateListener.of(update => { + if (update.docChanged) { + queueMicrotask(() => view.dispatch(setDiagnostics(view.state, []))); + } + if (update.docChanged && !checking && !loading) { + results.replaceChildren(); + message('Code changed. Verify to check it.'); + } + })], + parent: document.querySelector('#lj-editor') +}); +function message(text, state = '') { status.textContent = text; status.dataset.state = state; } +function controls(busy) { verify.disabled = busy; stop.disabled = !busy; } +function finish() { clearTimeout(timer); checking = loading = false; controls(false); } +function discard() { worker?.terminate(); worker = undefined; finish(); } +function failure(text) { discard(); message(text, 'failure'); } +function render(result) { + finish(); + if (source !== view.state.doc.toString()) { message('Code changed during verification. Verify again.'); return; } + results.replaceChildren(); + const issues = result.diagnostics || []; + const marks = []; + for (const issue of issues) { + const article = document.createElement('article'); article.className = 'lj-issue'; + const title = document.createElement('h3'); title.textContent = issue.title; article.append(title); + if (issue.line && issue.line <= view.state.doc.lines) { + const line = view.state.doc.line(issue.line); + marks.push({ from: line.from, to: line.to, severity: issue.severity, message: `${issue.title}: ${issue.message}` }); + const jump = document.createElement('button'); jump.textContent = `Line ${issue.line}`; + jump.onclick = () => { view.dispatch({ selection: { anchor: line.from }, scrollIntoView: true }); view.focus(); }; + article.append(jump); + } + for (const text of [issue.message, issue.hint, issue.counterexample]) { + if (!text) continue; + const paragraph = document.createElement('p'); paragraph.textContent = text; article.append(paragraph); + } + results.append(article); + } + view.dispatch(setDiagnostics(view.state, marks)); + const messages = { success: 'Passed verification.', warning: 'Verification finished with warnings.', error: 'Verification found errors.', failure: 'Verification could not complete. ' + (result.message || '') }; + message(messages[result.status] || 'Verification could not complete.', result.status); + if (result.status === 'failure') discard(); +} +function send() { + loading = false; checking = true; + clearTimeout(timer); + message('Verifying…'); + timer = setTimeout(() => failure('Verification timed out. Simplify the example and try again.'), 30000); + worker.postMessage({ type: 'verify', source }); +} +async function run() { + if (checking || loading) return; + if (!crossOriginIsolated || typeof SharedArrayBuffer === 'undefined') { + message('This browser cannot start the verifier. Open the playground directly in a browser with cross-origin isolation support.', 'failure'); return; + } + source = view.state.doc.toString(); + results.replaceChildren(); view.dispatch(setDiagnostics(view.state, [])); + controls(true); + if (worker) { send(); return; } + loading = true; + message('Downloading and starting the verifier. This may take a moment…'); + timer = setTimeout(() => failure('The verifier took too long to load. Check your connection and try again.'), 120000); + try { worker = new Worker(new URL('worker.js', runtime)); } + catch { failure('The verifier could not start. Reload the page and try again.'); return; } + const currentWorker = worker; + worker.onerror = () => { if (worker === currentWorker) failure('The verifier could not start. Reload the page and try again.'); }; + worker.onmessage = event => { + if (worker !== currentWorker) return; + const data = event.data; + if (data.type === 'status') message(data.message); + if (data.type === 'ready') send(); + if (data.type === 'result') render(data.result); + if (data.type === 'failure') failure('Verification could not complete. ' + data.message); + }; +} +verify.onclick = run; +stop.onclick = () => { discard(); message('Verification stopped.'); }; +function reset() { + if (checking || loading) discard(); + view.dispatch({ changes: { from: 0, to: view.state.doc.length, insert: examples[example.value] } }); + view.dispatch(setDiagnostics(view.state, [])); results.replaceChildren(); message('Example ready. Select Verify to check it.'); +} +example.onchange = reset; +document.querySelector('#lj-reset').onclick = reset; +root.addEventListener('keydown', event => { + if ((event.ctrlKey || event.metaKey) && event.key === 'Enter') { event.preventDefault(); run(); } +}); +// Restrict the isolation worker to this page's directory; other docs stay unaffected. +if (!crossOriginIsolated) { + verify.disabled = true; + if (!('serviceWorker' in navigator) || !isSecureContext) { + message('The playground requires HTTPS or localhost and service worker support.', 'failure'); + } else { + message('Preparing the playground…'); + try { + await navigator.serviceWorker.register(new URL('../isolation.js', runtime), { scope: new URL('../', runtime).pathname, updateViaCache: 'none' }); + await navigator.serviceWorker.ready; + const key = 'liquidjava-playground-isolation'; + if (!sessionStorage.getItem(key)) { sessionStorage.setItem(key, 'reload'); location.reload(); } + else { message('This browser could not enable the verifier. Try opening the playground in a current Chrome, Firefox or Safari browser.', 'failure'); } + } catch { message('The playground could not prepare the verifier. Reload and try again.', 'failure'); } + } +} else { verify.disabled = false; sessionStorage.removeItem('liquidjava-playground-isolation'); } diff --git a/scripts/playground/examples.mjs b/scripts/playground/examples.mjs new file mode 100644 index 0000000..45f3f89 --- /dev/null +++ b/scripts/playground/examples.mjs @@ -0,0 +1,58 @@ +export const examples = { + positive: `import liquidjava.specification.Refinement; + +class Example { + void positiveNumbers() { + @Refinement("_ > 0") + int count = 5; + + // try changing 5 to -1 + } +} +`, + bounds: `import liquidjava.specification.Refinement; + +class Example { + void setPercentage(@Refinement("_ >= 0 && _ <= 100") int percentage) {} + + void demo() { + setPercentage(75); + // try changing 75 to 150 + } +} +`, + alias: `import liquidjava.specification.Refinement; +import liquidjava.specification.RefinementAlias; + +@RefinementAlias("Positive(int x) { x > 0 }") +class Example { + void demo() { + @Refinement("Positive(_)") + int amount = 10; + // try changing 10 to 0 + } +} +`, + state: `import liquidjava.specification.StateSet; +import liquidjava.specification.StateRefinement; + +@StateSet({"open", "closed"}) +class Example { + @StateRefinement(to = "open(this)") + Example() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + void close() {} + + @StateRefinement(from = "open(this)") + void read() {} + + static void demo() { + Example resource = new Example(); + resource.read(); + resource.close(); + // try adding resource.read() after close() + } +} +` +}; diff --git a/scripts/playground/java/com/microsoft/z3/Z3Loader.java b/scripts/playground/java/com/microsoft/z3/Z3Loader.java new file mode 100644 index 0000000..5e90af1 --- /dev/null +++ b/scripts/playground/java/com/microsoft/z3/Z3Loader.java @@ -0,0 +1,6 @@ +package com.microsoft.z3; + +// browser methods are supplied through cheerpjInit's natives option +final class Z3Loader { + static void loadZ3() {} +} diff --git a/scripts/playground/java/liquidjava/playground/BrowserRunner.java b/scripts/playground/java/liquidjava/playground/BrowserRunner.java new file mode 100644 index 0000000..75cdc58 --- /dev/null +++ b/scripts/playground/java/liquidjava/playground/BrowserRunner.java @@ -0,0 +1,94 @@ +package liquidjava.playground; + +import com.google.gson.Gson; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.ArrayList; +import java.util.LinkedHashMap; +import java.util.Map; +import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.LJDiagnostic; +import liquidjava.processor.RefinementProcessor; +import liquidjava.processor.context.ContextHistory; +import org.eclipse.jdt.core.compiler.CategorizedProblem; +import spoon.Launcher; +import spoon.compiler.builder.AdvancedOptions; +import spoon.compiler.builder.ClasspathOptions; +import spoon.compiler.builder.ComplianceOptions; +import spoon.compiler.builder.JDTBuilder; +import spoon.compiler.builder.JDTBuilderImpl; +import spoon.compiler.builder.SourceOptions; +import spoon.processing.ProcessingManager; +import spoon.reflect.factory.Factory; +import spoon.support.QueueProcessingManager; +import spoon.support.compiler.jdt.JDTBasedSpoonCompiler; + +public final class BrowserRunner { + public static String verify(String source, String jar, String javaBase) { + Map result = new LinkedHashMap<>(); + ArrayList> issues = new ArrayList<>(); + try { + Path dir = Path.of("/files/playground"); + Files.createDirectories(dir); + Path input = dir.resolve("Example.java"); + Files.writeString(input, source); + Diagnostics.getInstance().clear(); + ContextHistory.getInstance().clearHistory(); + Launcher launcher = new Launcher(); + launcher.addInputResource(input.toString()); + launcher.getEnvironment().setNoClasspath(true); + launcher.getEnvironment().setComplianceLevel(8); + launcher.getEnvironment().setSourceClasspath(new String[] {jar}); + JDTBuilder builder = new JDTBuilderImpl() + .classpathOptions(new ClasspathOptions().classpath(jar).bootclasspath(javaBase)) + .complianceOptions(new ComplianceOptions().compliance(8)) + .advancedOptions(new AdvancedOptions().preserveUnusedVars().continueExecution().enableJavadoc()) + .sources(new SourceOptions().sources(input.toString())); + JDTBasedSpoonCompiler compiler = (JDTBasedSpoonCompiler) launcher.getModelBuilder(); + boolean built = compiler.build(builder); + for (CategorizedProblem problem : compiler.getProblems()) { + if (!problem.isError()) continue; + Map issue = new LinkedHashMap<>(); + issue.put("severity", "error"); + issue.put("title", "Java Error"); + issue.put("message", problem.getMessage()); + issue.put("line", problem.getSourceLineNumber()); + issues.add(issue); + } + if (issues.isEmpty()) { + if (!built) throw new IllegalArgumentException("Java source could not be parsed"); + Factory factory = launcher.getFactory(); + ProcessingManager manager = new QueueProcessingManager(factory); + manager.addProcessor(new RefinementProcessor(factory)); + manager.process(factory.Package().getRootPackage()); + } + Diagnostics diagnostics = Diagnostics.getInstance(); + for (LJDiagnostic error : diagnostics.getErrors()) issues.add(issue(error, "error")); + for (LJDiagnostic warning : diagnostics.getWarnings()) issues.add(issue(warning, "warning")); + result.put("status", !issues.isEmpty() && issues.stream().anyMatch(i -> "error".equals(i.get("severity"))) + ? "error" : diagnostics.foundWarning() ? "warning" : "success"); + } catch (Throwable error) { + result.put("status", "failure"); + result.put("message", error.toString()); + java.io.StringWriter stack = new java.io.StringWriter(); + error.printStackTrace(new java.io.PrintWriter(stack)); + result.put("details", stack.toString()); + } + result.put("diagnostics", issues); + return new Gson().toJson(result); + } + + private static Map issue(LJDiagnostic issue, String severity) { + Map result = new LinkedHashMap<>(); + result.put("severity", severity); + result.put("title", issue.getTitle()); + result.put("message", issue.getMessage()); + result.put("hint", issue.getHint()); + result.put("counterexample", issue.getCounterexampleStr()); + if (issue.getPosition() != null && issue.getPosition().isValidPosition()) { + result.put("line", issue.getPosition().getLine()); + result.put("column", issue.getPosition().getColumn()); + } + return result; + } +} diff --git a/scripts/playground/worker.js b/scripts/playground/worker.js new file mode 100644 index 0000000..e5eef76 --- /dev/null +++ b/scripts/playground/worker.js @@ -0,0 +1,39 @@ +import { init } from 'z3-solver/build/low-level/index.js'; +import { createNatives } from './adapter.mjs'; + +importScripts('https://cjrtnc.leaningtech.com/4.3/loader.js', './z3-built.js'); +const status = message => postMessage({ type: 'status', message }); +let runner; +let runnerJar; +let standardLibrary; +let busy = false; +async function initialize() { + status('Loading the verifier…'); + const { Z3 } = await init(() => self.initZ3({ mainScriptUrlOrBlob: new URL('./z3-built.js', self.location.href).href, locateFile: file => new URL(file, self.location.href).href })); + const response = await fetch('./native-methods.json'); + if (!response.ok) throw new Error('The verifier files could not be loaded.'); + Z3.global_param_set('timeout', '10000'); + const natives = createNatives(Z3, await response.json()); + await cheerpjInit({ version: 17, status: 'none', natives }); + const jar = new URL('./liquidjava.jar', self.location.href); + const lib = await cheerpjRunLibrary('/app' + jar.pathname); + runner = await lib.liquidjava.playground.BrowserRunner; + runnerJar = '/app' + jar.pathname; + standardLibrary = '/app' + new URL('./java-base.jar', self.location.href).pathname; + postMessage({ type: 'ready' }); +} +async function describe(error) { + try { return String(error); } catch { return await error.toString(); } +} +self.onmessage = async event => { + if (busy || event.data.type !== 'verify') return; + busy = true; + try { + await ready; + postMessage({ type: 'result', result: JSON.parse(await runner.verify(event.data.source, runnerJar, standardLibrary)) }); + } catch (error) { + postMessage({ type: 'failure', message: await describe(error) }); + } finally { busy = false; } +}; +const ready = initialize(); +ready.catch(async error => postMessage({ type: 'failure', message: await describe(error) })); From 7a9ad450a907961fc21dbb2c1004bd953a84ff01 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 00:50:26 +0100 Subject: [PATCH 02/21] Use precise source ranges for playground diagnostics Underline declared names and reported expression or syntax spans instead of whole lines, and navigate to the corresponding offset. Co-authored-by: Codex --- scripts/playground/diagnostics.mjs | 5 ++++ scripts/playground/diagnostics.test.mjs | 24 +++++++++++++++++++ scripts/playground/editor.js | 6 +++-- .../liquidjava/playground/BrowserRunner.java | 13 ++++++++++ 4 files changed, 46 insertions(+), 2 deletions(-) create mode 100644 scripts/playground/diagnostics.mjs create mode 100644 scripts/playground/diagnostics.test.mjs diff --git a/scripts/playground/diagnostics.mjs b/scripts/playground/diagnostics.mjs new file mode 100644 index 0000000..a032fb1 --- /dev/null +++ b/scripts/playground/diagnostics.mjs @@ -0,0 +1,5 @@ +export function editorDiagnostic(issue, length) { + const { from, to } = issue; + if (!Number.isInteger(from) || !Number.isInteger(to) || from < 0 || to <= from || to > length) return null; + return { from, to, severity: issue.severity, message: `${issue.title}: ${issue.message}` }; +} diff --git a/scripts/playground/diagnostics.test.mjs b/scripts/playground/diagnostics.test.mjs new file mode 100644 index 0000000..71115d8 --- /dev/null +++ b/scripts/playground/diagnostics.test.mjs @@ -0,0 +1,24 @@ +import test from 'node:test'; +import assert from 'node:assert/strict'; +import { editorDiagnostic } from './diagnostics.mjs'; + +test('underline the reported expression without expanding into indentation or surrounding code', () => { + const source = 'class Example {\n int count = -5;\n}'; + const from = source.indexOf('-5'); + const diagnostic = editorDiagnostic({ from, to: from + 2, severity: 'error', title: 'Refinement Error', message: 'Invalid value' }, source.length); + assert.equal(source.slice(diagnostic.from, diagnostic.to), '-5'); +}); + +test('preserve multiline UTF-16 source ranges', () => { + const source = '// 🧪\ncall(\n value\n);'; + const from = source.indexOf('call'); + const to = source.indexOf(';'); + const diagnostic = editorDiagnostic({ from, to }, source.length); + assert.equal(source.slice(diagnostic.from, diagnostic.to), 'call(\n value\n)'); +}); + +test('missing or invalid positions do not produce misleading underlines', () => { + for (const issue of [{ line: 1 }, { from: -1, to: 2 }, { from: 1, to: 1 }, { from: 2, to: 1 }, { from: 0, to: 11 }]) { + assert.equal(editorDiagnostic(issue, 10), null); + } +}); diff --git a/scripts/playground/editor.js b/scripts/playground/editor.js index 52d0ce9..d9546df 100644 --- a/scripts/playground/editor.js +++ b/scripts/playground/editor.js @@ -2,6 +2,7 @@ import { EditorView, basicSetup } from 'codemirror'; import { java } from '@codemirror/lang-java'; import { setDiagnostics } from '@codemirror/lint'; import { examples } from './examples.mjs'; +import { editorDiagnostic } from './diagnostics.mjs'; const root = document.querySelector('#lj-playground'); const example = document.querySelector('#lj-example'); @@ -43,11 +44,12 @@ function render(result) { for (const issue of issues) { const article = document.createElement('article'); article.className = 'lj-issue'; const title = document.createElement('h3'); title.textContent = issue.title; article.append(title); + const mark = editorDiagnostic(issue, view.state.doc.length); + if (mark) marks.push(mark); if (issue.line && issue.line <= view.state.doc.lines) { const line = view.state.doc.line(issue.line); - marks.push({ from: line.from, to: line.to, severity: issue.severity, message: `${issue.title}: ${issue.message}` }); const jump = document.createElement('button'); jump.textContent = `Line ${issue.line}`; - jump.onclick = () => { view.dispatch({ selection: { anchor: line.from }, scrollIntoView: true }); view.focus(); }; + jump.onclick = () => { view.dispatch({ selection: { anchor: mark?.from ?? line.from }, scrollIntoView: true }); view.focus(); }; article.append(jump); } for (const text of [issue.message, issue.hint, issue.counterexample]) { diff --git a/scripts/playground/java/liquidjava/playground/BrowserRunner.java b/scripts/playground/java/liquidjava/playground/BrowserRunner.java index 75cdc58..45d927f 100644 --- a/scripts/playground/java/liquidjava/playground/BrowserRunner.java +++ b/scripts/playground/java/liquidjava/playground/BrowserRunner.java @@ -20,6 +20,8 @@ import spoon.compiler.builder.SourceOptions; import spoon.processing.ProcessingManager; import spoon.reflect.factory.Factory; +import spoon.reflect.cu.SourcePosition; +import spoon.reflect.cu.position.CompoundSourcePosition; import spoon.support.QueueProcessingManager; import spoon.support.compiler.jdt.JDTBasedSpoonCompiler; @@ -53,6 +55,8 @@ public static String verify(String source, String jar, String javaBase) { issue.put("title", "Java Error"); issue.put("message", problem.getMessage()); issue.put("line", problem.getSourceLineNumber()); + issue.put("from", problem.getSourceStart()); + issue.put("to", problem.getSourceEnd() + 1); issues.add(issue); } if (issues.isEmpty()) { @@ -88,6 +92,15 @@ private static Map issue(LJDiagnostic issue, String severity) { if (issue.getPosition() != null && issue.getPosition().isValidPosition()) { result.put("line", issue.getPosition().getLine()); result.put("column", issue.getPosition().getColumn()); + SourcePosition position = issue.getPosition(); + // declaration ranges include annotations; underline the declared name + if (position instanceof CompoundSourcePosition declaration) { + result.put("from", declaration.getNameStart()); + result.put("to", declaration.getNameEnd() + 1); + } else { + result.put("from", position.getSourceStart()); + result.put("to", position.getSourceEnd() + 1); + } } return result; } From 33be924d50cbeb2e8ccd3434b4b9933da4fe58f5 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 00:55:37 +0100 Subject: [PATCH 03/21] Extend playground declaration underlines through initializers Match the VS Code diagnostic range from the declared name through the initializer, excluding the final delimiter and preceding annotations. Co-authored-by: Codex --- .../playground/java/liquidjava/playground/BrowserRunner.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/playground/java/liquidjava/playground/BrowserRunner.java b/scripts/playground/java/liquidjava/playground/BrowserRunner.java index 45d927f..57a30e2 100644 --- a/scripts/playground/java/liquidjava/playground/BrowserRunner.java +++ b/scripts/playground/java/liquidjava/playground/BrowserRunner.java @@ -93,10 +93,10 @@ private static Map issue(LJDiagnostic issue, String severity) { result.put("line", issue.getPosition().getLine()); result.put("column", issue.getPosition().getColumn()); SourcePosition position = issue.getPosition(); - // declaration ranges include annotations; underline the declared name + // match VS Code: start at the name and span the declaration, excluding its closing delimiter if (position instanceof CompoundSourcePosition declaration) { result.put("from", declaration.getNameStart()); - result.put("to", declaration.getNameEnd() + 1); + result.put("to", position.getSourceEnd()); } else { result.put("from", position.getSourceStart()); result.put("to", position.getSourceEnd() + 1); From 1ff06a8156498be19cd578abe35f51a516250c17 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 13:09:26 +0100 Subject: [PATCH 04/21] Improve playground entry button and navigation order Co-authored-by: Codex --- _sass/custom/custom.scss | 42 +++++++++++++++------------------------- pages/index.md | 2 +- playground/index.md | 2 +- 3 files changed, 18 insertions(+), 28 deletions(-) diff --git a/_sass/custom/custom.scss b/_sass/custom/custom.scss index f5bd9de..60d389b 100644 --- a/_sass/custom/custom.scss +++ b/_sass/custom/custom.scss @@ -259,40 +259,30 @@ margin: 1.5rem 0 0; } -.home-button { +.main-content .home-button { display: inline-flex; align-items: center; justify-content: center; - min-height: 2.9rem; - padding: 0.8rem 1.1rem; - border-radius: 999px; - border: 1px solid transparent; - font-weight: 700; - line-height: 1.1; - text-decoration: none !important; - transition: transform 120ms ease, box-shadow 120ms ease, background-color 120ms ease, border-color 120ms ease; - box-shadow: 0 14px 26px rgba(51, 80, 106, 0.22); -} - -.home-button:hover, -.home-button:focus { - transform: translateY(-1px); -} - -.home-button:focus { - outline: none; - box-shadow: 0 0 0 3px rgba(65, 88, 111, 0.16); + gap: 0.65rem; + padding: 0.7rem 1.1rem; + border-radius: 0.5rem; + color: #fff; + background: #334e68; + font-weight: 600; + line-height: 1.5; + text-decoration: none; + box-shadow: 0 2px 4px rgba(23, 26, 31, 0.12); } -.home-button.primary { +.main-content .home-button:hover { color: #fff; - background: linear-gradient(135deg, #63c093 0%, #4e98a8 50%, #4a80b0 100%); - box-shadow: 0 18px 10px rgba(51, 80, 106, 0.22); + background: #253b50; + text-decoration: none; } -.home-button.secondary { - color: #2a3642; - border-color: rgba(42, 54, 66, 0.15); +.main-content .home-button:focus-visible { + outline: 3px solid #5f7ea1; + outline-offset: 3px; } .card-panel { diff --git a/pages/index.md b/pages/index.md index 62c13d9..32d1cc4 100644 --- a/pages/index.md +++ b/pages/index.md @@ -10,7 +10,7 @@ description: Documentation for LiquidJava, a lightweight verification system for

Extending Java with Liquid Types

LiquidJava is an additional type system for Java that uses liquid types to express constraints programs must follow, helping catch more bugs before they run.

-

Try LiquidJava in your browser

+

Try LiquidJava

LiquidJava banner diff --git a/playground/index.md b/playground/index.md index 1325384..e28f841 100644 --- a/playground/index.md +++ b/playground/index.md @@ -1,6 +1,6 @@ --- title: Playground -nav_order: 1.5 +nav_order: 8 permalink: /playground/ has_toc: false description: Try LiquidJava refinements and typestates directly in your browser. From f1db8d520f9933aa31012baf05dd4d66d281510a Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 13:12:41 +0100 Subject: [PATCH 05/21] Use normal weight for playground entry button Co-authored-by: Codex --- _sass/custom/custom.scss | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/_sass/custom/custom.scss b/_sass/custom/custom.scss index 60d389b..9bdcd9c 100644 --- a/_sass/custom/custom.scss +++ b/_sass/custom/custom.scss @@ -268,7 +268,7 @@ border-radius: 0.5rem; color: #fff; background: #334e68; - font-weight: 600; + font-weight: 400; line-height: 1.5; text-decoration: none; box-shadow: 0 2px 4px rgba(23, 26, 31, 0.12); From a0f7cf1babf014b968ad55c04eaff2c83fd80a88 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 13:19:00 +0100 Subject: [PATCH 06/21] Improve UI --- _sass/custom/custom.scss | 3 ++- package-lock.json | 2 ++ package.json | 2 ++ playground/editor.css | 31 +++++++++++++++------- playground/index.md | 24 +++++++++-------- scripts/playground/editor-theme.mjs | 40 +++++++++++++++++++++++++++++ scripts/playground/editor.js | 4 +-- 7 files changed, 84 insertions(+), 22 deletions(-) create mode 100644 scripts/playground/editor-theme.mjs diff --git a/_sass/custom/custom.scss b/_sass/custom/custom.scss index 9bdcd9c..9657eb1 100644 --- a/_sass/custom/custom.scss +++ b/_sass/custom/custom.scss @@ -43,7 +43,8 @@ } .main-content pre.highlight, -.main-content div.highlighter-rouge { +.main-content div.highlighter-rouge, +.main-content #lj-editor { overflow-x: auto; overflow-y: hidden; scrollbar-width: thin; diff --git a/package-lock.json b/package-lock.json index 8ee2ab3..eea85f8 100644 --- a/package-lock.json +++ b/package-lock.json @@ -7,7 +7,9 @@ "name": "liquidjava-docs", "dependencies": { "@codemirror/lang-java": "6.0.2", + "@codemirror/language": "6.12.4", "@codemirror/lint": "6.8.5", + "@lezer/highlight": "1.2.5", "codemirror": "6.0.2" }, "devDependencies": { diff --git a/package.json b/package.json index 663980c..dafc429 100644 --- a/package.json +++ b/package.json @@ -13,7 +13,9 @@ }, "dependencies": { "@codemirror/lang-java": "6.0.2", + "@codemirror/language": "6.12.4", "@codemirror/lint": "6.8.5", + "@lezer/highlight": "1.2.5", "codemirror": "6.0.2" } } diff --git a/playground/editor.css b/playground/editor.css index 2bac767..75e1241 100644 --- a/playground/editor.css +++ b/playground/editor.css @@ -1,11 +1,24 @@ -.lj-playground { border: 1px solid var(--border-color, #d7dce2); border-radius: 8px; overflow: hidden; margin: 1.5rem 0; } -.lj-toolbar { display: flex; align-items: center; flex-wrap: wrap; gap: .6rem; padding: 1rem; background: #f5f7fa; } -.lj-toolbar label { font-weight: 600; } -.lj-toolbar select { font: inherit; max-width: 100%; padding: .35rem; border: 1px solid #bbc4ce; border-radius: 4px; background: white; } -.lj-toolbar button:disabled { opacity: .5; cursor: default; } -.lj-playground .cm-editor { font-size: 14px; background: #fff; } -.lj-playground .cm-scroller { min-height: 300px; max-height: 560px; overflow: auto; font-family: 'JetBrains Mono', monospace; } -.lj-playground .cm-focused { outline: 2px solid #1269a8; outline-offset: -2px; } +.lj-playground { margin: 1.5rem 0; } +.lj-toolbar { display: flex; align-items: flex-end; justify-content: space-between; flex-wrap: wrap; gap: 1rem; } +.lj-example-picker { display: flex; flex-direction: column; gap: .35rem; max-width: 100%; } +.lj-toolbar label { color: #555c65; font-size: .8rem; font-weight: 400; } +.lj-toolbar select, +.lj-toolbar button { min-height: 2.5rem; border: 1px solid #cbd2d9; border-radius: .5rem; font: inherit; font-size: .875rem; font-weight: 400; line-height: 1.4; } +.lj-toolbar select { max-width: 100%; padding: .5rem .75rem; color: #2a2f36; background: #fff; cursor: pointer; } +.lj-actions { display: flex; align-items: center; flex-wrap: wrap; gap: .5rem; } +.lj-toolbar button { padding: .5rem .9rem; color: #334e68; background: transparent; box-shadow: none; cursor: pointer; } +.lj-toolbar button:hover:not(:disabled) { background: #e5eef7; border-color: #5f7ea1; } +.lj-toolbar #lj-verify { color: #fff; background: #334e68; border-color: #334e68; } +.lj-toolbar #lj-verify:hover:not(:disabled) { background: #253b50; border-color: #253b50; } +.lj-toolbar #lj-reset { border-color: transparent; } +.lj-toolbar button:disabled { color: #8a929b; background: #efefec; border-color: #e4e4e7; cursor: default; } +.lj-toolbar #lj-verify:disabled { color: #fff; background: #7f90a1; border-color: #7f90a1; } +.lj-toolbar select:focus-visible, +.lj-toolbar button:focus-visible { outline: 2px solid #5f7ea1; outline-offset: 3px; } +#lj-editor { margin: 1rem 0; overflow: hidden; } +.lj-playground .cm-editor { font-size: .75em; border-radius: inherit; overflow: hidden; } +.lj-playground .cm-scroller { min-height: 300px; max-height: 560px; overflow: auto; font-family: 'JetBrains Mono', 'SFMono-Regular', Menlo, Consolas, monospace; line-height: 1.6; scrollbar-width: thin; scrollbar-color: rgba(255, 255, 255, .72) rgba(255, 255, 255, .16); } +.lj-playground .cm-focused { outline: 2px solid #7dd3fc; outline-offset: -2px; } #lj-status { margin: 0; padding: 1rem; border-top: 1px solid #d7dce2; font-size: .9rem; } #lj-status[data-state="success"] { color: #156b35; background: #eef9f1; } #lj-status[data-state="error"], #lj-status[data-state="failure"] { color: #9b2323; background: #fff1f1; } @@ -14,4 +27,4 @@ .lj-issue p { margin: .5rem 0; white-space: pre-wrap; } .lj-issue pre { white-space: pre-wrap; margin: .5rem 0; } .lj-issue button { font: inherit; border: 0; padding: 0; background: transparent; color: #1269a8; cursor: pointer; text-decoration: underline; } -@media (max-width: 600px) { .lj-toolbar { gap: .5rem; padding: .75rem; } .lj-playground .cm-editor { font-size: 12px; } } +@media (max-width: 600px) { .lj-example-picker { width: 100%; } } diff --git a/playground/index.md b/playground/index.md index e28f841..faa981d 100644 --- a/playground/index.md +++ b/playground/index.md @@ -13,16 +13,20 @@ Edit an example and select **Verify** to check it with LiquidJava. Verification
- - - - - +
+ + +
+
+ + + +

Choose an example or edit the code, then verify. Ctrl+Enter / ⌘+Enter also verifies.

diff --git a/scripts/playground/editor-theme.mjs b/scripts/playground/editor-theme.mjs new file mode 100644 index 0000000..70a03a6 --- /dev/null +++ b/scripts/playground/editor-theme.mjs @@ -0,0 +1,40 @@ +import { EditorView } from 'codemirror'; +import { javaLanguage } from '@codemirror/lang-java'; +import { HighlightStyle, LanguageSupport, syntaxHighlighting } from '@codemirror/language'; +import { styleTags, tags } from '@lezer/highlight'; + +const snippetJava = javaLanguage.configure({ props: [styleTags({ + 'Annotation/Identifier MarkerAnnotation/Identifier': tags.annotation, + 'ClassDeclaration/Definition InterfaceDeclaration/Definition EnumDeclaration/Definition': tags.typeName, + 'MethodDeclaration/Definition ConstructorDeclaration/Definition': tags.function(tags.variableName), + 'ImportDeclaration/ScopedIdentifier!': tags.namespace +})] }); + +export const editorJava = new LanguageSupport(snippetJava); + +export const editorTheme = [ + EditorView.theme({ + '&': { color: '#e6edf7', backgroundColor: 'transparent' }, + '.cm-content': { caretColor: '#e6edf7', padding: '1rem 0' }, + '.cm-line': { padding: '0 1.15rem' }, + '.cm-gutters': { color: '#7f90ad', backgroundColor: 'transparent', border: 'none' }, + '.cm-activeLine, .cm-activeLineGutter': { backgroundColor: '#ffffff08' }, + '&.cm-focused .cm-selectionBackground, .cm-selectionBackground, ::selection': { backgroundColor: '#334e6880' }, + '.cm-cursor, .cm-dropCursor': { borderLeftColor: '#e6edf7' }, + '.cm-tooltip, .cm-panels': { color: '#e6edf7', backgroundColor: '#172033', borderColor: '#334e68' }, + '.cm-searchMatch': { backgroundColor: '#b39b5e55' }, + '.cm-searchMatch-selected': { backgroundColor: '#b39b5e88' }, + '.cm-matchingBracket': { backgroundColor: '#7dd3fc26', outline: '1px solid #7dd3fc66' } + }, { dark: true }), + syntaxHighlighting(HighlightStyle.define([ + { tag: tags.name, color: '#dce6f2' }, + { tag: tags.comment, color: '#7f90ad', fontStyle: 'italic' }, + { tag: [tags.keyword, tags.bool], color: '#ffb86c' }, + { tag: [tags.typeName, tags.annotation, tags.function(tags.variableName)], color: '#7dd3fc' }, + { tag: tags.string, color: '#a7f3c1' }, + { tag: tags.number, color: '#f6c177' }, + { tag: [tags.namespace, tags.attributeName], color: '#c4b5fd' }, + { tag: [tags.operator, tags.punctuation], color: '#c9d4e5' }, + { tag: tags.invalid, color: '#ffd6d6', backgroundColor: '#b43e4747' } + ])) +]; diff --git a/scripts/playground/editor.js b/scripts/playground/editor.js index d9546df..503bcc9 100644 --- a/scripts/playground/editor.js +++ b/scripts/playground/editor.js @@ -1,8 +1,8 @@ import { EditorView, basicSetup } from 'codemirror'; -import { java } from '@codemirror/lang-java'; import { setDiagnostics } from '@codemirror/lint'; import { examples } from './examples.mjs'; import { editorDiagnostic } from './diagnostics.mjs'; +import { editorJava, editorTheme } from './editor-theme.mjs'; const root = document.querySelector('#lj-playground'); const example = document.querySelector('#lj-example'); @@ -18,7 +18,7 @@ let source; let timer; const view = new EditorView({ doc: examples.positive, - extensions: [basicSetup, java(), EditorView.contentAttributes.of({ 'aria-label': 'Java source code' }), + extensions: [basicSetup, editorJava, editorTheme, EditorView.contentAttributes.of({ 'aria-label': 'Java source code' }), EditorView.updateListener.of(update => { if (update.docChanged) { queueMicrotask(() => view.dispatch(setDiagnostics(view.state, []))); From 6c5806fec2063ea106dbd8f0cadf002e807b1b8a Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 13:26:24 +0100 Subject: [PATCH 07/21] Render full CLI diagnostics with colors in the playground Co-authored-by: Codex --- _sass/custom/custom.scss | 3 ++- package-lock.json | 10 ++++++++ package.json | 1 + playground/editor.css | 24 ++++++++++++------- playground/index.md | 6 +++-- scripts/playground/diagnostics.mjs | 9 ++++++- scripts/playground/diagnostics.test.mjs | 23 +++++++++++++++++- scripts/playground/editor.js | 24 +++++++------------ .../liquidjava/playground/BrowserRunner.java | 10 +++----- 9 files changed, 75 insertions(+), 35 deletions(-) diff --git a/_sass/custom/custom.scss b/_sass/custom/custom.scss index 9657eb1..1059bcf 100644 --- a/_sass/custom/custom.scss +++ b/_sass/custom/custom.scss @@ -44,7 +44,8 @@ .main-content pre.highlight, .main-content div.highlighter-rouge, -.main-content #lj-editor { +.main-content #lj-editor, +.main-content .lj-output { overflow-x: auto; overflow-y: hidden; scrollbar-width: thin; diff --git a/package-lock.json b/package-lock.json index eea85f8..64eca0a 100644 --- a/package-lock.json +++ b/package-lock.json @@ -10,6 +10,7 @@ "@codemirror/language": "6.12.4", "@codemirror/lint": "6.8.5", "@lezer/highlight": "1.2.5", + "ansi_up": "6.0.6", "codemirror": "6.0.2" }, "devDependencies": { @@ -592,6 +593,15 @@ "integrity": "sha512-Wy0V7+SGUjnF9/TkiM1hKVDPj7jKXduPNboMVtHTA8dySMURWqfg/JZ9E2Sq8JgSJmkl7k7Qe9FLeMSrSraWmQ==", "license": "MIT" }, + "node_modules/ansi_up": { + "version": "6.0.6", + "resolved": "https://registry.npmjs.org/ansi_up/-/ansi_up-6.0.6.tgz", + "integrity": "sha512-yIa1x3Ecf8jWP4UWEunNjqNX6gzE4vg2gGz+xqRGY+TBSucnYp6RRdPV4brmtg6bQ1ljD48mZ5iGSEj7QEpRKA==", + "license": "MIT", + "engines": { + "node": "*" + } + }, "node_modules/ansi-styles": { "version": "4.3.0", "resolved": "https://registry.npmjs.org/ansi-styles/-/ansi-styles-4.3.0.tgz", diff --git a/package.json b/package.json index dafc429..3ec2940 100644 --- a/package.json +++ b/package.json @@ -16,6 +16,7 @@ "@codemirror/language": "6.12.4", "@codemirror/lint": "6.8.5", "@lezer/highlight": "1.2.5", + "ansi_up": "6.0.6", "codemirror": "6.0.2" } } diff --git a/playground/editor.css b/playground/editor.css index 75e1241..b69518b 100644 --- a/playground/editor.css +++ b/playground/editor.css @@ -19,12 +19,20 @@ .lj-playground .cm-editor { font-size: .75em; border-radius: inherit; overflow: hidden; } .lj-playground .cm-scroller { min-height: 300px; max-height: 560px; overflow: auto; font-family: 'JetBrains Mono', 'SFMono-Regular', Menlo, Consolas, monospace; line-height: 1.6; scrollbar-width: thin; scrollbar-color: rgba(255, 255, 255, .72) rgba(255, 255, 255, .16); } .lj-playground .cm-focused { outline: 2px solid #7dd3fc; outline-offset: -2px; } -#lj-status { margin: 0; padding: 1rem; border-top: 1px solid #d7dce2; font-size: .9rem; } -#lj-status[data-state="success"] { color: #156b35; background: #eef9f1; } -#lj-status[data-state="error"], #lj-status[data-state="failure"] { color: #9b2323; background: #fff1f1; } -.lj-issue { padding: 1rem; border-top: 1px solid #d7dce2; } -.lj-issue h3 { margin: 0 0 .5rem; font-size: 1rem; } -.lj-issue p { margin: .5rem 0; white-space: pre-wrap; } -.lj-issue pre { white-space: pre-wrap; margin: .5rem 0; } -.lj-issue button { font: inherit; border: 0; padding: 0; background: transparent; color: #1269a8; cursor: pointer; text-decoration: underline; } +.lj-output { color: #e6edf7; } +#lj-status { margin: 0; padding: 1rem 1.15rem; font-family: 'JetBrains Mono', 'SFMono-Regular', Menlo, Consolas, monospace; font-size: .75em; line-height: 1.6; } +#lj-status[data-state="success"] { color: #a7f3c1; } +#lj-status[data-state="warning"] { color: #f6c177; } +#lj-status[data-state="error"], #lj-status[data-state="failure"] { color: #ffd6d6; } +#lj-results:not(:empty) { border-top: 1px solid #ffffff1a; } +.main-content #lj-results pre { margin: 0; } +#lj-results .ansi-black-fg { color: #111827; } +#lj-results .ansi-bright-black-fg { color: #9ca3af; } +#lj-results :is(.ansi-red-fg, .ansi-bright-red-fg) { color: #f29e9e; } +#lj-results :is(.ansi-green-fg, .ansi-bright-green-fg) { color: #a7f3c1; } +#lj-results :is(.ansi-yellow-fg, .ansi-bright-yellow-fg) { color: #f6c177; } +#lj-results :is(.ansi-blue-fg, .ansi-bright-blue-fg) { color: #93b4f4; } +#lj-results :is(.ansi-magenta-fg, .ansi-bright-magenta-fg) { color: #c4b5fd; } +#lj-results :is(.ansi-cyan-fg, .ansi-bright-cyan-fg) { color: #7dd3fc; } +#lj-results :is(.ansi-white-fg, .ansi-bright-white-fg) { color: #e6edf7; } @media (max-width: 600px) { .lj-example-picker { width: 100%; } } diff --git a/playground/index.md b/playground/index.md index faa981d..ab6cd1c 100644 --- a/playground/index.md +++ b/playground/index.md @@ -29,8 +29,10 @@ Edit an example and select **Verify** to check it with LiquidJava. Verification
-

Choose an example or edit the code, then verify. Ctrl+Enter / ⌘+Enter also verifies.

-
+
+

Choose an example or edit the code, then verify. Ctrl+Enter / ⌘+Enter also verifies.

+
+
diff --git a/scripts/playground/diagnostics.mjs b/scripts/playground/diagnostics.mjs index a032fb1..b7bb785 100644 --- a/scripts/playground/diagnostics.mjs +++ b/scripts/playground/diagnostics.mjs @@ -1,5 +1,12 @@ export function editorDiagnostic(issue, length) { const { from, to } = issue; if (!Number.isInteger(from) || !Number.isInteger(to) || from < 0 || to <= from || to > length) return null; - return { from, to, severity: issue.severity, message: `${issue.title}: ${issue.message}` }; + return { from, to, severity: issue.severity, message: issue.output?.replace(/\u001b\[[0-9;]*m/g, '') }; +} +import { AnsiUp } from 'ansi_up'; + +export function diagnosticHtml(output) { + const ansi = new AnsiUp(); + ansi.use_classes = true; + return ansi.ansi_to_html(output); } diff --git a/scripts/playground/diagnostics.test.mjs b/scripts/playground/diagnostics.test.mjs index 71115d8..68cf610 100644 --- a/scripts/playground/diagnostics.test.mjs +++ b/scripts/playground/diagnostics.test.mjs @@ -1,6 +1,27 @@ import test from 'node:test'; import assert from 'node:assert/strict'; -import { editorDiagnostic } from './diagnostics.mjs'; +import { diagnosticHtml, editorDiagnostic } from './diagnostics.mjs'; + +test('render CLI colors and bold with resets and escaped source text', () => { + const html = diagnosticHtml('\u001b[1;31mRefinement Error\u001b[0m: \n\u001b[38;5;208m^^^\u001b[0m\n'); + assert.match(html, /font-weight:bold/); + assert.match(html, /ansi-red-fg/); + assert.match(html, /color:rgb\(/); + assert.match(html, /rgb\(255,135,0\)/); + assert.match(html, /<script>/); + assert.doesNotMatch(html, /\n\u001b[38;5;208m^^^\u001b[0m\n'); assert.match(html, /font-weight:bold/); diff --git a/scripts/playground/editor.js b/scripts/playground/editor.js index 6f3af37..f57b3a8 100644 --- a/scripts/playground/editor.js +++ b/scripts/playground/editor.js @@ -7,8 +7,8 @@ import { editorJava, editorTheme } from './editor-theme.mjs'; const root = document.querySelector('#lj-playground'); const example = document.querySelector('#lj-example'); const verify = document.querySelector('#lj-verify'); -const stop = document.querySelector('#lj-stop'); const status = document.querySelector('#lj-status'); +const output = document.querySelector('.lj-output'); const results = document.querySelector('#lj-results'); const runtime = new URL(root.dataset.runtime, location.href); let worker; @@ -25,13 +25,21 @@ const view = new EditorView({ } if (update.docChanged && !checking && !loading) { results.replaceChildren(); - message('Code changed. Verify to check it.'); + message(''); } })], parent: document.querySelector('#lj-editor') }); -function message(text, state = '') { status.textContent = text; status.dataset.state = state; } -function controls(busy) { verify.disabled = busy; stop.disabled = !busy; } +function message(text, state = '') { + output.hidden = !text; + status.textContent = text; + status.dataset.state = state; + status.classList.toggle('sr-only', state === 'error'); +} +function controls(busy) { + verify.textContent = busy ? 'Stop' : 'Verify'; + verify.dataset.state = busy ? 'busy' : 'idle'; +} function finish() { clearTimeout(timer); checking = loading = false; controls(false); } function discard() { worker?.terminate(); worker = undefined; finish(); } function failure(text) { discard(); message(text, 'failure'); } @@ -89,25 +97,23 @@ async function run() { if (data.type === 'failure') failure('Verification could not complete. ' + data.message); }; } -verify.onclick = run; -stop.onclick = () => { discard(); message('Verification stopped.'); }; +verify.onclick = () => { + if (checking || loading) { discard(); message('Verification stopped.'); } + else run(); +}; function reset() { if (checking || loading) discard(); view.dispatch({ changes: { from: 0, to: view.state.doc.length, insert: examples[example.value] } }); - view.dispatch(setDiagnostics(view.state, [])); results.replaceChildren(); message('Example ready. Select Verify to check it.'); + view.dispatch(setDiagnostics(view.state, [])); results.replaceChildren(); message(''); } example.onchange = reset; document.querySelector('#lj-reset').onclick = reset; -root.addEventListener('keydown', event => { - if ((event.ctrlKey || event.metaKey) && event.key === 'Enter') { event.preventDefault(); run(); } -}); // Restrict the isolation worker to this page's directory; other docs stay unaffected. if (!crossOriginIsolated) { verify.disabled = true; if (!('serviceWorker' in navigator) || !isSecureContext) { message('The playground requires HTTPS or localhost and service worker support.', 'failure'); } else { - message('Preparing the playground…'); try { await navigator.serviceWorker.register(new URL('../isolation.js', runtime), { scope: new URL('../', runtime).pathname, updateViaCache: 'none' }); await navigator.serviceWorker.ready; From b4be3dcf761c07afec16a3e42664403b17641b54 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 14:20:41 +0100 Subject: [PATCH 10/21] Keep playground directory in diagnostic locations Co-authored-by: Codex --- scripts/playground/diagnostics.mjs | 2 +- scripts/playground/diagnostics.test.mjs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/playground/diagnostics.mjs b/scripts/playground/diagnostics.mjs index 4ecfd44..c5f392e 100644 --- a/scripts/playground/diagnostics.mjs +++ b/scripts/playground/diagnostics.mjs @@ -1,7 +1,7 @@ import { AnsiUp } from 'ansi_up'; function shortenLocations(output) { - return output.replace(/^\/files\/playground\/(?=[^/\r\n]+:\d+)/gm, ''); + return output.replace(/^\/files\/playground\/(?=[^/\r\n]+:\d+)/gm, '/playground/'); } export function editorDiagnostic(issue, length) { diff --git a/scripts/playground/diagnostics.test.mjs b/scripts/playground/diagnostics.test.mjs index 7e1aa2b..277ef19 100644 --- a/scripts/playground/diagnostics.test.mjs +++ b/scripts/playground/diagnostics.test.mjs @@ -7,9 +7,9 @@ test('omit leading CLI blank lines while preserving diagnostic spacing and color assert.equal(diagnosticHtml('\n\n' + diagnostic), diagnosticHtml(diagnostic)); }); -test('show only the filename and line in diagnostic locations', () => { +test('show the playground path, filename and line in diagnostic locations', () => { const output = '\u001b[31mError\u001b[0m\n\n/files/playground/Example.java:6\u001b[0m\n\n--> Refinement declared here:\n/files/playground/Example.java:5\u001b[0m\n'; - const expected = output.replaceAll('/files/playground/', ''); + const expected = output.replaceAll('/files/playground/', '/playground/'); assert.equal(diagnosticHtml(output), diagnosticHtml(expected)); assert.equal(editorDiagnostic({ from: 0, to: 1, output }, 1).message, expected.replace(/\u001b\[[0-9;]*m/g, '')); From d2fb4b9e46fc4270c010b398c64311e9cc07c31a Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 14:34:34 +0100 Subject: [PATCH 11/21] Remove editor folding and restore diagnostic navigation Co-authored-by: Codex --- package-lock.json | 23 +++++------------ package.json | 8 ++++-- playground/editor.css | 3 +++ scripts/playground/diagnostics.mjs | 4 ++- scripts/playground/diagnostics.test.mjs | 7 ++++++ scripts/playground/editor-setup.mjs | 33 +++++++++++++++++++++++++ scripts/playground/editor-theme.mjs | 2 +- scripts/playground/editor.js | 19 ++++++++++++-- 8 files changed, 76 insertions(+), 23 deletions(-) create mode 100644 scripts/playground/editor-setup.mjs diff --git a/package-lock.json b/package-lock.json index 64eca0a..aed9e06 100644 --- a/package-lock.json +++ b/package-lock.json @@ -6,12 +6,16 @@ "": { "name": "liquidjava-docs", "dependencies": { + "@codemirror/autocomplete": "6.20.3", + "@codemirror/commands": "6.11.1", "@codemirror/lang-java": "6.0.2", "@codemirror/language": "6.12.4", "@codemirror/lint": "6.8.5", + "@codemirror/search": "6.7.2", + "@codemirror/state": "6.7.6", + "@codemirror/view": "6.43.13", "@lezer/highlight": "1.2.5", - "ansi_up": "6.0.6", - "codemirror": "6.0.2" + "ansi_up": "6.0.6" }, "devDependencies": { "esbuild": "0.25.10", @@ -696,21 +700,6 @@ "url": "https://github.com/chalk/chalk?sponsor=1" } }, - "node_modules/codemirror": { - "version": "6.0.2", - "resolved": "https://registry.npmjs.org/codemirror/-/codemirror-6.0.2.tgz", - "integrity": "sha512-VhydHotNW5w1UGK0Qj96BwSk/Zqbp9WbnyK2W/eVMv4QyF41INRGpjUhFJY7/uDNuudSc33a/PKr4iDqRduvHw==", - "license": "MIT", - "dependencies": { - "@codemirror/autocomplete": "^6.0.0", - "@codemirror/commands": "^6.0.0", - "@codemirror/language": "^6.0.0", - "@codemirror/lint": "^6.0.0", - "@codemirror/search": "^6.0.0", - "@codemirror/state": "^6.0.0", - "@codemirror/view": "^6.0.0" - } - }, "node_modules/color-convert": { "version": "2.0.1", "resolved": "https://registry.npmjs.org/color-convert/-/color-convert-2.0.1.tgz", diff --git a/package.json b/package.json index 3ec2940..e061e57 100644 --- a/package.json +++ b/package.json @@ -12,11 +12,15 @@ "z3-solver": "4.16.0" }, "dependencies": { + "@codemirror/autocomplete": "6.20.3", + "@codemirror/commands": "6.11.1", "@codemirror/lang-java": "6.0.2", "@codemirror/language": "6.12.4", "@codemirror/lint": "6.8.5", + "@codemirror/search": "6.7.2", + "@codemirror/state": "6.7.6", + "@codemirror/view": "6.43.13", "@lezer/highlight": "1.2.5", - "ansi_up": "6.0.6", - "codemirror": "6.0.2" + "ansi_up": "6.0.6" } } diff --git a/playground/editor.css b/playground/editor.css index 5519c73..ec3a961 100644 --- a/playground/editor.css +++ b/playground/editor.css @@ -31,6 +31,9 @@ #lj-status[data-state="warning"] { color: #f6c177; } #lj-status:not(.sr-only) + #lj-results:not(:empty) { border-top: 1px solid #ffffff1a; } .main-content #lj-results pre { margin: 0; } +.main-content #lj-results a { color: #e6edf7; text-decoration: underline; text-underline-offset: .2em; } +.main-content #lj-results a:hover { color: #e6edf7; } +.main-content #lj-results a:focus-visible { outline: 2px solid #7dd3fc; outline-offset: 3px; } #lj-results .ansi-black-fg { color: #111827; } #lj-results .ansi-bright-black-fg { color: #9ca3af; } #lj-status[data-state="error"], diff --git a/scripts/playground/diagnostics.mjs b/scripts/playground/diagnostics.mjs index c5f392e..358de4f 100644 --- a/scripts/playground/diagnostics.mjs +++ b/scripts/playground/diagnostics.mjs @@ -13,5 +13,7 @@ export function editorDiagnostic(issue, length) { export function diagnosticHtml(output) { const ansi = new AnsiUp(); ansi.use_classes = true; - return ansi.ansi_to_html(shortenLocations(output).replace(/^(?:\r?\n)+/, '')); + return ansi.ansi_to_html(shortenLocations(output).replace(/^(?:\r?\n)+/, '')) + .replace(/^(\/playground\/[^<\r\n]+:(\d+))(?=\r?\n|$|<\/span>)/gm, + '$1'); } diff --git a/scripts/playground/diagnostics.test.mjs b/scripts/playground/diagnostics.test.mjs index 277ef19..e6d9146 100644 --- a/scripts/playground/diagnostics.test.mjs +++ b/scripts/playground/diagnostics.test.mjs @@ -2,6 +2,13 @@ import test from 'node:test'; import assert from 'node:assert/strict'; import { diagnosticHtml, editorDiagnostic } from './diagnostics.mjs'; +test('make diagnostic and declaration locations editor links without linking source excerpts', () => { + const html = diagnosticHtml('Error\n6 | String path = "/playground/Example.java:99";\n\n/files/playground/Example.java:6\u001b[0m\n\n--> Refinement declared here:\n/files/playground/Example.java:5\u001b[0m\n'); + assert.match(html, /\/playground\/Example.java:6<\/a>/); + assert.match(html, /\/playground\/Example.java:5<\/a>/); + assert.equal((html.match(/ { const diagnostic = '\u001b[31mError\u001b[0m\n6 | code\n | ^^^\n\nExample.java:6\n'; assert.equal(diagnosticHtml('\n\n' + diagnostic), diagnosticHtml(diagnostic)); diff --git a/scripts/playground/editor-setup.mjs b/scripts/playground/editor-setup.mjs new file mode 100644 index 0000000..47c0d51 --- /dev/null +++ b/scripts/playground/editor-setup.mjs @@ -0,0 +1,33 @@ +import { EditorState } from '@codemirror/state'; +import { lineNumbers, highlightActiveLineGutter, highlightSpecialChars, drawSelection, dropCursor, rectangularSelection, crosshairCursor, highlightActiveLine, keymap } from '@codemirror/view'; +import { indentOnInput, bracketMatching } from '@codemirror/language'; +import { history, defaultKeymap, historyKeymap } from '@codemirror/commands'; +import { highlightSelectionMatches, searchKeymap } from '@codemirror/search'; +import { closeBrackets, autocompletion, closeBracketsKeymap, completionKeymap } from '@codemirror/autocomplete'; +import { lintKeymap } from '@codemirror/lint'; + +export const editorSetup = [ + lineNumbers(), + highlightActiveLineGutter(), + highlightSpecialChars(), + history(), + drawSelection(), + dropCursor(), + EditorState.allowMultipleSelections.of(true), + indentOnInput(), + bracketMatching(), + closeBrackets(), + autocompletion(), + rectangularSelection(), + crosshairCursor(), + highlightActiveLine(), + highlightSelectionMatches(), + keymap.of([ + ...closeBracketsKeymap, + ...defaultKeymap, + ...searchKeymap, + ...historyKeymap, + ...completionKeymap, + ...lintKeymap + ]) +]; diff --git a/scripts/playground/editor-theme.mjs b/scripts/playground/editor-theme.mjs index 70a03a6..a0a1c06 100644 --- a/scripts/playground/editor-theme.mjs +++ b/scripts/playground/editor-theme.mjs @@ -1,4 +1,4 @@ -import { EditorView } from 'codemirror'; +import { EditorView } from '@codemirror/view'; import { javaLanguage } from '@codemirror/lang-java'; import { HighlightStyle, LanguageSupport, syntaxHighlighting } from '@codemirror/language'; import { styleTags, tags } from '@lezer/highlight'; diff --git a/scripts/playground/editor.js b/scripts/playground/editor.js index f57b3a8..eb6e97e 100644 --- a/scripts/playground/editor.js +++ b/scripts/playground/editor.js @@ -1,8 +1,9 @@ -import { EditorView, basicSetup } from 'codemirror'; +import { EditorView } from '@codemirror/view'; import { setDiagnostics } from '@codemirror/lint'; import { examples } from './examples.mjs'; import { diagnosticHtml, editorDiagnostic } from './diagnostics.mjs'; import { editorJava, editorTheme } from './editor-theme.mjs'; +import { editorSetup } from './editor-setup.mjs'; const root = document.querySelector('#lj-playground'); const example = document.querySelector('#lj-example'); @@ -18,7 +19,7 @@ let source; let timer; const view = new EditorView({ doc: examples.positive, - extensions: [basicSetup, editorJava, editorTheme, EditorView.contentAttributes.of({ 'aria-label': 'Java source code' }), + extensions: [editorSetup, editorJava, editorTheme, EditorView.contentAttributes.of({ 'aria-label': 'Java source code' }), EditorView.updateListener.of(update => { if (update.docChanged) { queueMicrotask(() => view.dispatch(setDiagnostics(view.state, []))); @@ -57,6 +58,20 @@ function render(result) { const pre = document.createElement('pre'); const code = document.createElement('code'); code.innerHTML = diagnosticHtml(issues.map(issue => issue.output).join('\n') + (result.details || '')); + for (const link of code.querySelectorAll('a[data-line]')) { + const lineNumber = Number(link.dataset.line); + if (lineNumber < 1 || lineNumber > view.state.doc.lines) continue; + link.onclick = event => { + event.preventDefault(); + const issue = issues.find(issue => issue.line === lineNumber); + const mark = issue && editorDiagnostic(issue, view.state.doc.length); + const line = view.state.doc.line(lineNumber); + const anchor = mark?.from ?? line.from + line.text.search(/\S|$/); + view.dom.scrollIntoView({ block: 'center', inline: 'nearest' }); + view.dispatch({ selection: { anchor }, effects: EditorView.scrollIntoView(anchor, { y: 'center' }) }); + view.focus(); + }; + } pre.append(code); results.append(pre); } From 693f03f193fcc2a217395cd88daa42af77720fd6 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 14:37:14 +0100 Subject: [PATCH 12/21] Disable diagnostic hovers and strengthen Stop button color Co-authored-by: Codex --- playground/editor.css | 4 ++-- scripts/playground/editor-setup.mjs | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/playground/editor.css b/playground/editor.css index ec3a961..954ca17 100644 --- a/playground/editor.css +++ b/playground/editor.css @@ -14,8 +14,8 @@ .lj-toolbar #lj-reset { min-width: 5rem; padding: .6rem .9rem; color: #fff; background: #334e68; border-color: #334e68; white-space: nowrap; flex-shrink: 0; } .lj-toolbar #lj-verify:hover:not(:disabled), .lj-toolbar #lj-reset:hover { background: #253b50; border-color: #253b50; } -.lj-toolbar #lj-verify[data-state="busy"] { background: #7a4343; border-color: #7a4343; } -.lj-toolbar #lj-verify[data-state="busy"]:hover { background: #643535; border-color: #643535; } +.lj-toolbar #lj-verify[data-state="busy"] { background: #c62828; border-color: #c62828; } +.lj-toolbar #lj-verify[data-state="busy"]:hover { background: #a61f1f; border-color: #a61f1f; } .lj-toolbar button:disabled { color: #8a929b; background: #efefec; border-color: #e4e4e7; cursor: default; } .lj-toolbar #lj-verify:disabled { color: #fff; background: #7f90a1; border-color: #7f90a1; } .lj-toolbar select:focus-visible, diff --git a/scripts/playground/editor-setup.mjs b/scripts/playground/editor-setup.mjs index 47c0d51..f164817 100644 --- a/scripts/playground/editor-setup.mjs +++ b/scripts/playground/editor-setup.mjs @@ -4,7 +4,7 @@ import { indentOnInput, bracketMatching } from '@codemirror/language'; import { history, defaultKeymap, historyKeymap } from '@codemirror/commands'; import { highlightSelectionMatches, searchKeymap } from '@codemirror/search'; import { closeBrackets, autocompletion, closeBracketsKeymap, completionKeymap } from '@codemirror/autocomplete'; -import { lintKeymap } from '@codemirror/lint'; +import { linter, lintKeymap } from '@codemirror/lint'; export const editorSetup = [ lineNumbers(), @@ -22,6 +22,7 @@ export const editorSetup = [ crosshairCursor(), highlightActiveLine(), highlightSelectionMatches(), + linter(null, { tooltipFilter: () => [] }), keymap.of([ ...closeBracketsKeymap, ...defaultKeymap, From cb6e6017f873b7ccd30f362635d46d0243aeedff Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 14:42:41 +0100 Subject: [PATCH 13/21] Scroll smoothly before focusing diagnostic locations Co-authored-by: Codex --- scripts/playground/editor-navigation.mjs | 32 ++++++++++++++++++++++++ scripts/playground/editor.js | 5 ++-- 2 files changed, 34 insertions(+), 3 deletions(-) create mode 100644 scripts/playground/editor-navigation.mjs diff --git a/scripts/playground/editor-navigation.mjs b/scripts/playground/editor-navigation.mjs new file mode 100644 index 0000000..1acd8e4 --- /dev/null +++ b/scripts/playground/editor-navigation.mjs @@ -0,0 +1,32 @@ +function scrollTo(element, top, behavior) { + const target = Math.max(0, Math.min(top, element.scrollHeight - element.clientHeight)); + if (Math.abs(target - element.scrollTop) < 1) return Promise.resolve(); + return new Promise(resolve => { + const events = element === document.scrollingElement ? document : element; + if (behavior === 'smooth') events.addEventListener('scrollend', resolve, { once: true }); + element.scrollTo({ top: target, behavior }); + if (behavior === 'instant') resolve(); + }); +} + +export function navigateTo(view, anchor) { + view.requestMeasure({ + read: () => { + const line = view.lineBlockAt(anchor); + const editor = view.dom.getBoundingClientRect(); + return { + editorTop: line.top + line.height / 2 - view.scrollDOM.clientHeight / 2, + pageTop: window.scrollY + editor.top + editor.height / 2 - window.innerHeight / 2 + }; + }, + write: async ({ editorTop, pageTop }) => { + const behavior = matchMedia('(prefers-reduced-motion: reduce)').matches ? 'instant' : 'smooth'; + await Promise.all([ + scrollTo(view.scrollDOM, editorTop, behavior), + scrollTo(document.scrollingElement, pageTop, behavior) + ]); + view.dispatch({ selection: { anchor } }); + view.focus(); + } + }); +} diff --git a/scripts/playground/editor.js b/scripts/playground/editor.js index eb6e97e..f779d8b 100644 --- a/scripts/playground/editor.js +++ b/scripts/playground/editor.js @@ -4,6 +4,7 @@ import { examples } from './examples.mjs'; import { diagnosticHtml, editorDiagnostic } from './diagnostics.mjs'; import { editorJava, editorTheme } from './editor-theme.mjs'; import { editorSetup } from './editor-setup.mjs'; +import { navigateTo } from './editor-navigation.mjs'; const root = document.querySelector('#lj-playground'); const example = document.querySelector('#lj-example'); @@ -67,9 +68,7 @@ function render(result) { const mark = issue && editorDiagnostic(issue, view.state.doc.length); const line = view.state.doc.line(lineNumber); const anchor = mark?.from ?? line.from + line.text.search(/\S|$/); - view.dom.scrollIntoView({ block: 'center', inline: 'nearest' }); - view.dispatch({ selection: { anchor }, effects: EditorView.scrollIntoView(anchor, { y: 'center' }) }); - view.focus(); + navigateTo(view, anchor); }; } pre.append(code); From 23261897d0519914a2aaa1bb144ab8b4f5926e24 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 14:43:03 +0100 Subject: [PATCH 14/21] Minor Changes --- playground/index.md | 6 ++---- scripts/playground/examples.mjs | 29 +++++++++++------------------ 2 files changed, 13 insertions(+), 22 deletions(-) diff --git a/playground/index.md b/playground/index.md index 7527012..22d0171 100644 --- a/playground/index.md +++ b/playground/index.md @@ -8,7 +8,7 @@ description: Try LiquidJava refinements and typestates directly in your browser. # Playground -Edit an example and select **Verify** to check it with LiquidJava. Verification runs in your browser; your code is not sent to a server. The first check downloads the verifier and may take a moment. +Run the LiquidJava verification directly in your browser. Edit an example and select **Verify**.
@@ -23,7 +23,7 @@ Edit an example and select **Verify** to check it with LiquidJava. Verification
- +
@@ -35,6 +35,4 @@ Edit an example and select **Verify** to check it with LiquidJava. Verification -The playground checks one Java file using Java 8 syntax, with the bundled LiquidJava annotations and core Java types. External dependencies are not supported. For projects, use the [VS Code extension]({{ '/vscode-extension/' | relative_url }}). - diff --git a/scripts/playground/examples.mjs b/scripts/playground/examples.mjs index 45f3f89..2369bf9 100644 --- a/scripts/playground/examples.mjs +++ b/scripts/playground/examples.mjs @@ -1,57 +1,50 @@ export const examples = { - positive: `import liquidjava.specification.Refinement; + positive: `import liquidjava.specification.*; class Example { void positiveNumbers() { @Refinement("_ > 0") - int count = 5; - - // try changing 5 to -1 + int count = -1; } } `, - bounds: `import liquidjava.specification.Refinement; + bounds: `import liquidjava.specification.*; class Example { void setPercentage(@Refinement("_ >= 0 && _ <= 100") int percentage) {} void demo() { - setPercentage(75); - // try changing 75 to 150 + setPercentage(125); } } `, - alias: `import liquidjava.specification.Refinement; -import liquidjava.specification.RefinementAlias; + alias: `import liquidjava.specification.*; @RefinementAlias("Positive(int x) { x > 0 }") class Example { void demo() { @Refinement("Positive(_)") - int amount = 10; - // try changing 10 to 0 + int amount = 0; } } `, - state: `import liquidjava.specification.StateSet; -import liquidjava.specification.StateRefinement; + state: `import liquidjava.specification.*; @StateSet({"open", "closed"}) class Example { - @StateRefinement(to = "open(this)") + @StateRefinement(to="open(this)") Example() {} - @StateRefinement(from = "open(this)", to = "closed(this)") + @StateRefinement(from="open(this)", to="closed(this)") void close() {} - @StateRefinement(from = "open(this)") + @StateRefinement(from="open(this)") void read() {} static void demo() { Example resource = new Example(); - resource.read(); resource.close(); - // try adding resource.read() after close() + resource.read(); } } ` From 52af72b042daca55a49a37bc5c1e6a35a4325e60 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 14:47:38 +0100 Subject: [PATCH 15/21] Wrap the sidebar contribution footer with proper spacing Co-authored-by: Codex --- _includes/nav_footer_custom.html | 6 +++--- _sass/custom/custom.scss | 4 ++++ 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/_includes/nav_footer_custom.html b/_includes/nav_footer_custom.html index fc59d87..155ab07 100644 --- a/_includes/nav_footer_custom.html +++ b/_includes/nav_footer_custom.html @@ -1,4 +1,4 @@ -

- Help improve this documentation by contributing on +

 diff --git a/_sass/custom/custom.scss b/_sass/custom/custom.scss index 1059bcf..24b58e6 100644 --- a/_sass/custom/custom.scss +++ b/_sass/custom/custom.scss @@ -28,6 +28,10 @@ $sidebar-color; } +.site-footer { + color: $body-text-color; +} + .main-content a { color: #41586f; text-decoration-thickness: 0.08em; From b6c66212460fc8100200477d2c2e8dd90eee6f0f Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 14:51:58 +0100 Subject: [PATCH 16/21] Add a ghost state tracking playground example Co-authored-by: Codex --- playground/index.md | 1 + scripts/playground/examples.mjs | 21 +++++++++++++++++++++ 2 files changed, 22 insertions(+) diff --git a/playground/index.md b/playground/index.md index 22d0171..a979057 100644 --- a/playground/index.md +++ b/playground/index.md @@ -21,6 +21,7 @@ Run the LiquidJava verification directly in your browser. Edit an example and se + diff --git a/scripts/playground/examples.mjs b/scripts/playground/examples.mjs index 2369bf9..9d65990 100644 --- a/scripts/playground/examples.mjs +++ b/scripts/playground/examples.mjs @@ -47,5 +47,26 @@ class Example { resource.read(); } } +`, + ghost: `import liquidjava.specification.*; + +@Ghost("int count") +class Example { + @StateRefinement(to="count(this) == 0") + Example() {} + + @StateRefinement(to="count(this) == count(old(this)) + 1") + void increment() {} + + @StateRefinement(from="count(this) > 0", to="count(this) == count(old(this)) - 1") + void decrement() {} + + static void demo() { + Example counter = new Example(); + counter.increment(); + counter.decrement(); + counter.decrement(); + } +} ` }; From 6ffd883d1975f9b3ee29ffd6942eba1f57e24ac0 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 14:53:13 +0100 Subject: [PATCH 17/21] Disable matching highlights for selected editor text Co-authored-by: Codex --- scripts/playground/editor-setup.mjs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/scripts/playground/editor-setup.mjs b/scripts/playground/editor-setup.mjs index f164817..1f90a70 100644 --- a/scripts/playground/editor-setup.mjs +++ b/scripts/playground/editor-setup.mjs @@ -2,7 +2,7 @@ import { EditorState } from '@codemirror/state'; import { lineNumbers, highlightActiveLineGutter, highlightSpecialChars, drawSelection, dropCursor, rectangularSelection, crosshairCursor, highlightActiveLine, keymap } from '@codemirror/view'; import { indentOnInput, bracketMatching } from '@codemirror/language'; import { history, defaultKeymap, historyKeymap } from '@codemirror/commands'; -import { highlightSelectionMatches, searchKeymap } from '@codemirror/search'; +import { searchKeymap } from '@codemirror/search'; import { closeBrackets, autocompletion, closeBracketsKeymap, completionKeymap } from '@codemirror/autocomplete'; import { linter, lintKeymap } from '@codemirror/lint'; @@ -21,7 +21,6 @@ export const editorSetup = [ rectangularSelection(), crosshairCursor(), highlightActiveLine(), - highlightSelectionMatches(), linter(null, { tooltipFilter: () => [] }), keymap.of([ ...closeBracketsKeymap, From 7c6f046e55538cbe82bbfe89b83544715d442fa4 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 14:57:02 +0100 Subject: [PATCH 18/21] Use native blue for editor text selection Co-authored-by: Codex --- scripts/playground/editor-theme.mjs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/playground/editor-theme.mjs b/scripts/playground/editor-theme.mjs index a0a1c06..5777cca 100644 --- a/scripts/playground/editor-theme.mjs +++ b/scripts/playground/editor-theme.mjs @@ -19,7 +19,7 @@ export const editorTheme = [ '.cm-line': { padding: '0 1.15rem' }, '.cm-gutters': { color: '#7f90ad', backgroundColor: 'transparent', border: 'none' }, '.cm-activeLine, .cm-activeLineGutter': { backgroundColor: '#ffffff08' }, - '&.cm-focused .cm-selectionBackground, .cm-selectionBackground, ::selection': { backgroundColor: '#334e6880' }, + '&.cm-focused > .cm-scroller > .cm-selectionLayer .cm-selectionBackground, .cm-selectionBackground, ::selection': { backgroundColor: 'Highlight' }, '.cm-cursor, .cm-dropCursor': { borderLeftColor: '#e6edf7' }, '.cm-tooltip, .cm-panels': { color: '#e6edf7', backgroundColor: '#172033', borderColor: '#334e68' }, '.cm-searchMatch': { backgroundColor: '#b39b5e55' }, From 2e6d20a9ac587be07c902e053ad4baba8a023932 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 14:59:14 +0100 Subject: [PATCH 19/21] Keep Tab and Shift-Tab indentation inside the editor Co-authored-by: Codex --- scripts/playground/editor-setup.mjs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/playground/editor-setup.mjs b/scripts/playground/editor-setup.mjs index 1f90a70..162bb98 100644 --- a/scripts/playground/editor-setup.mjs +++ b/scripts/playground/editor-setup.mjs @@ -1,7 +1,7 @@ import { EditorState } from '@codemirror/state'; import { lineNumbers, highlightActiveLineGutter, highlightSpecialChars, drawSelection, dropCursor, rectangularSelection, crosshairCursor, highlightActiveLine, keymap } from '@codemirror/view'; import { indentOnInput, bracketMatching } from '@codemirror/language'; -import { history, defaultKeymap, historyKeymap } from '@codemirror/commands'; +import { history, defaultKeymap, historyKeymap, insertTab, indentLess } from '@codemirror/commands'; import { searchKeymap } from '@codemirror/search'; import { closeBrackets, autocompletion, closeBracketsKeymap, completionKeymap } from '@codemirror/autocomplete'; import { linter, lintKeymap } from '@codemirror/lint'; @@ -24,6 +24,7 @@ export const editorSetup = [ linter(null, { tooltipFilter: () => [] }), keymap.of([ ...closeBracketsKeymap, + { key: 'Tab', run: insertTab, shift: indentLess }, ...defaultKeymap, ...searchKeymap, ...historyKeymap, From 6553f6c535f5231b4e279c064fb54e1a69c8b041 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 15:02:33 +0100 Subject: [PATCH 20/21] Match unindent width to editor tabs Co-authored-by: Codex --- scripts/playground/editor-setup.mjs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/playground/editor-setup.mjs b/scripts/playground/editor-setup.mjs index 162bb98..ce230fc 100644 --- a/scripts/playground/editor-setup.mjs +++ b/scripts/playground/editor-setup.mjs @@ -1,6 +1,6 @@ import { EditorState } from '@codemirror/state'; import { lineNumbers, highlightActiveLineGutter, highlightSpecialChars, drawSelection, dropCursor, rectangularSelection, crosshairCursor, highlightActiveLine, keymap } from '@codemirror/view'; -import { indentOnInput, bracketMatching } from '@codemirror/language'; +import { indentOnInput, indentUnit, bracketMatching } from '@codemirror/language'; import { history, defaultKeymap, historyKeymap, insertTab, indentLess } from '@codemirror/commands'; import { searchKeymap } from '@codemirror/search'; import { closeBrackets, autocompletion, closeBracketsKeymap, completionKeymap } from '@codemirror/autocomplete'; @@ -15,6 +15,7 @@ export const editorSetup = [ dropCursor(), EditorState.allowMultipleSelections.of(true), indentOnInput(), + indentUnit.of(' '), bracketMatching(), closeBrackets(), autocompletion(), From 52258b10b39239d5958e9974d9f14757ac3f7370 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sun, 4 Oct 2026 15:07:16 +0100 Subject: [PATCH 21/21] Reduce the playground editor minimum height Co-authored-by: Codex --- playground/editor.css | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/playground/editor.css b/playground/editor.css index 954ca17..f49fb8a 100644 --- a/playground/editor.css +++ b/playground/editor.css @@ -22,7 +22,7 @@ .lj-toolbar button:focus-visible { outline: 2px solid #5f7ea1; outline-offset: 3px; } #lj-editor { margin: 1rem 0; overflow: hidden; } .lj-playground .cm-editor { font-size: .75em; border-radius: inherit; overflow: hidden; } -.lj-playground .cm-scroller { min-height: 300px; max-height: 560px; overflow: auto; font-family: 'JetBrains Mono', 'SFMono-Regular', Menlo, Consolas, monospace; line-height: 1.6; scrollbar-width: thin; scrollbar-color: rgba(255, 255, 255, .72) rgba(255, 255, 255, .16); } +.lj-playground .cm-scroller { min-height: 200px; max-height: 560px; overflow: auto; font-family: 'JetBrains Mono', 'SFMono-Regular', Menlo, Consolas, monospace; line-height: 1.6; scrollbar-width: thin; scrollbar-color: rgba(255, 255, 255, .72) rgba(255, 255, 255, .16); } .lj-playground .cm-focused { outline: 2px solid #7dd3fc; outline-offset: -2px; } .lj-output { color: #e6edf7; } #lj-status { margin: 0; padding: 1rem 1.15rem; font-family: 'JetBrains Mono', 'SFMono-Regular', Menlo, Consolas, monospace; font-size: .75em; line-height: 1.6; }