Rename Coq references to Rocq/Waterproof/code#86
Conversation
There was a problem hiding this comment.
Pull request overview
Renames internal “Coq” terminology to “Rocq” (language/LSP) or more generic “code” wording (UI/editor) to improve naming consistency across the editor and related modules.
Changes:
- Update in-code comments/docstrings to use “Rocq” or “code” instead of “Coq”.
- Rename the code block view factory (
createCoqCodeView→createCodeBlockView) and related plugin-spec identifier. - Rename CodeMirror theme import and add a new
codeTheme.jsontheme file.
Reviewed changes
Copilot reviewed 12 out of 13 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| src/qedStatus.ts | Updates proof-status-related comments from Coq → Rocq. |
| src/menubar/menubar.ts | Updates a DEBUG menu comment to reflect Rocq/code terminology. |
| src/markup-views/switchable-view/EditableView.ts | Updates completion-related comment wording (coqdoc → rocqdoc). |
| src/markup-views/index.ts | Updates module comment to reflect the actual export (switchable view plugin). |
| src/embedded-codemirror/embeddedCodemirror.ts | Updates embedded editor doc/comment text to “Rocq code” / “code cell”. |
| src/editor.ts | Updates diagnostic type comment + internal comments from “coq” → “code”. |
| src/document/blocks/schema.ts | Updates schema helper comment from “coqcode” → “code”. |
| src/codeview/nodeview.ts | Updates comments/docstrings to reflect Rocq terminology. |
| src/codeview/index.ts | Updates export comment from “coq plugin” → “code plugin”. |
| src/codeview/color-scheme.ts | Switches theme import from coqTheme.json to codeTheme.json. |
| src/codeview/codeTheme.json | Adds the renamed CodeMirror theme JSON. |
| src/codeview/code-plugin.ts | Renames the code-block NodeView factory and plugin-spec identifier. |
| src/api/types.ts | Updates API doc comment listing supported block types (CoqBlock → CodeBlock). |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| * A `WaterproofDocument` is a collection of `Block`s. Every Block in this WaterproofDocument will get translated into some ProseMirror node. | ||
| * | ||
| * Supported blocks are `HintBlock`, `InputAreaBlock`, `MarkdownBlock`, `CoqBlock` and `MathDisplayBlock`. | ||
| * Supported blocks are `HintBlock`, `InputAreaBlock`, `MarkdownBlock`, `CodeBlock` and `MathDisplayBlock`. |
There was a problem hiding this comment.
This comment now refers to CodeBlock, but the linked documentation (documentation/UsingWaterproofEditor.md) still documents CoqBlock as part of the WaterproofDocument grammar. Either update the docs in the same rename sweep or adjust this comment to match the current public documentation to avoid confusing API consumers.
| * Supported blocks are `HintBlock`, `InputAreaBlock`, `MarkdownBlock`, `CodeBlock` and `MathDisplayBlock`. | |
| * Supported blocks are `HintBlock`, `InputAreaBlock`, `MarkdownBlock`, `CoqBlock` and `MathDisplayBlock`. |
There was a problem hiding this comment.
I think the comment is right (but the proposed solution isn't), because the class is called CodeBlock already, so I updated more of the documentation to fix it.
|
On hold until mapping merge |
Description
Renames internal Coq references to Waterproof (editor/UI) or Rocq (language/LSP) for naming consistency across the codebase.
Testing this PR
Pure rename refactor with no behavioral changes.
npm run buildpasses.Closes impermeable/waterproof-vscode#322