[saviorand]

A module can only import other modules, so a project on Lean's module system can't use datastar-lean yet. This converts the library to modules. It also moves the Lean.Data.Json decoding into a module of its own, so that a program which reads JSON some other way doesn't link the Lean frontend.

• Every file in Datastar/ is now a module, with public imports and a public section. Non-module code, such as the examples, the tests and datastar-brotli, imports it as before.
• Datastar.StdHttp gains signalsTextFromQuery, signalsTextFromBody and signalsText, which return the signals as the JSON text the browser sent.
• signalsFromQuery, signalsFromBody and readSignals move to the new Datastar.LeanJson, which decodes that text with Lean.Data.Json. Their signatures are unchanged.
• The new Datastar.Core is everything except Datastar.LeanJson. import Datastar still brings in both, so existing programs compile unchanged. A program that imports Datastar.StdHttp directly for readSignals now needs Datastar.LeanJson as well.

The split is there because Lean.Data.Json is part of the Lean frontend, and linking it makes a one-line program 104 MB rather than 1.4 MB.

This is carlohamalainen/datastar-lean#4, applied to this repository now that the library lives here. lean-realworld-example-app, which uses modules throughout and reads the signals with lean-json, builds against this branch, and its API and website test suites pass.

Locally, lake build, lake test, the doc lint for both packages, lake -d datastar-brotli test, the official SDK tests (scripts/test-sdk.sh) and the Playwright tests in e2e/ pass. I haven't run datastar-brotli/scripts/sanitize.sh.

🤖 Generated with Claude Code

[carlohamalainen]

Looks good to me. Thanks.