Skip to content

Render src/nova/*.nova to syntax-highlighted HTML, deploy to GitHub Pages - #44

Merged
Russoul merged 1 commit into
mainfrom
host-the-docs
Aug 3, 2026
Merged

Render src/nova/*.nova to syntax-highlighted HTML, deploy to GitHub Pages#44
Russoul merged 1 commit into
mainfrom
host-the-docs

Conversation

@Russoul

@Russoul Russoul commented Aug 3, 2026

Copy link
Copy Markdown
Owner

Summary

  • New nova-docs executable (nova-docs.ipkg, src/idris/Nova/Docs/Render.idr) batch-renders .nova surface files to standalone HTML pages. It reuses the LSP's own token classification and hole-state overlay (Nova.LSP.SemanticTokens) rather than a separate classifier, so the highlighting always matches what an editor's LSP client shows.
  • Nova.LSP.SemanticTokens/Capabilities gain small exports (sortTokens, overlay, tokenTypeNames) to make that classification reusable outside the LSP server — no behavior change.
  • tools/nova-docs.css / tools/pages-index.html: styling (matching the existing rendered-specs palette) and a small landing page linking the two doc sets.
  • CI (.github/workflows/nova.yml): build-and-test now also builds nova-docs and renders src/nova/*.nova; a new deploy-pages job (gated to pushes on main) combines that output with the existing rendered spec pages and deploys both to GitHub Pages.

Note

GitHub Pages needs to be enabled once for this repo (Settings → Pages → Source → "GitHub Actions") before deploy-pages can succeed.

…ages

Reuses the LSP's own token classification and hole-state overlay
(Nova.LSP.SemanticTokens) instead of a separate classifier, so the
highlighting always matches what an editor's LSP client shows. CI now
builds and deploys the rendered sources alongside the existing spec
pages.
@Russoul
Russoul merged commit 48352c3 into main Aug 3, 2026
3 checks passed
@Russoul
Russoul deleted the host-the-docs branch August 3, 2026 19:02
@github-project-automation github-project-automation Bot moved this from Backlog to Done in Nova Progress tracker Aug 3, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

Development

Successfully merging this pull request may close these issues.

1 participant