Rename Coq references to Rocq/Waterproof/code

documentation/UsingWaterproofEditor.md

@@ -10,7 +10,7 @@ The `WaterproofDocument` serves as an intermediate representation of the input f
 #### Example document constructor
 An example can be found in [the waterproof-vscode repository](https://github.com/impermeable/waterproof-vscode/blob/main/editor/src/document-construction/construct-document.ts). In `waterproof-vscode` we work with `.mv` files (Markdown files containing Rocq code, which use the `.v` file extension).
 
-In our `.mv` constructor, parts surrounded by `<input-area>` and `</input-area>` are mapped to `InputAreaBlock`s, parts surrounded by `<hint title="{some title}">` and `</hint>` are mapped to `HintBlock`s, parts surrounded by ` ```coq ` and ` ``` ` are translated to `CoqBlock`s, etc.
+In our `.mv` constructor, parts surrounded by `<input-area>` and `</input-area>` are mapped to `InputAreaBlock`s, parts surrounded by `<hint title="{some title}">` and `</hint>` are mapped to `HintBlock`s, parts surrounded by ` ```coq ` and ` ``` ` are translated to `CodeBlock`s, etc.
 
 ### WaterproofDocument
 It may be helpful to think of a WaterproofDocument in terms of the following "grammar":
@@ -27,7 +27,7 @@ HintBlock           ::= Container of InnerBlock+ with a title.
 InputAreaBlock      ::= Container of InnerBlock+
 
 MarkdownBlock       ::= A container with markdown content (supports inline LaTeX).
-CodeBlock            ::= A container with code content.
+CodeBlock           ::= A container with code content.
 MathDisplayBlock    ::= A container with LaTeX content that should be rendered in math display mode.
 NewlineBlock        ::= A block that keeps track of significant newlines
 ```

src/api/types.ts

@@ -16,7 +16,7 @@ export type Range = {from: number, to: number};
 /**
  * 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`.
  *
  * Also see [documentation/UsingWaterproofEditor.md](../../documentation/UsingWaterproofEditor.md)
  */

src/codeview/code-plugin.ts

@@ -32,7 +32,7 @@ export const CODE_PLUGIN_KEY = new PluginKey<ICodePluginState>("waterproof-edito
  * Returns a function suitable for passing as a field in `EditorProps.nodeViews`.
  * @see https://prosemirror.net/docs/ref/#view.EditorProps.nodeViews
  */
-export function createCoqCodeView(completions: Array<Completion>, symbols: Array<Completion>, editorInstance: WaterproofEditor, initialThemeStyle: ThemeStyle, languageConfig?: LanguageConfiguration){
+export function createCodeBlockView(completions: Array<Completion>, symbols: Array<Completion>, editorInstance: WaterproofEditor, initialThemeStyle: ThemeStyle, languageConfig?: LanguageConfiguration){
 	return (node: ProseNode, view: EditorView, getPos: () => number | undefined): CodeBlockView => {
 		/** @todo is this necessary?
 		* Docs says that for any function proprs, the current plugin instance
@@ -52,7 +52,7 @@ export function createCoqCodeView(completions: Array<Completion>, symbols: Array
 }
 
 
-const CoqCodePluginSpec = (completions: Array<Completion>, symbols: Array<Completion>, editorInstance: WaterproofEditor, initialThemeStyle: ThemeStyle, languageConfig?: LanguageConfiguration) : PluginSpec<ICodePluginState> => { return {
+const codePluginSpec = (completions: Array<Completion>, symbols: Array<Completion>, editorInstance: WaterproofEditor, initialThemeStyle: ThemeStyle, languageConfig?: LanguageConfiguration) : PluginSpec<ICodePluginState> => { return {
 	key: CODE_PLUGIN_KEY,
 	state: {
 		init(config, instance){
@@ -118,7 +118,7 @@ const CoqCodePluginSpec = (completions: Array<Completion>, symbols: Array<Comple
 	},
 	props: {
 		nodeViews: {
-			"code" : createCoqCodeView(completions, symbols, editorInstance, initialThemeStyle, languageConfig)
+			"code" : createCodeBlockView(completions, symbols, editorInstance, initialThemeStyle, languageConfig)
 		}
 	}
 }};
@@ -130,6 +130,6 @@ export const codePlugin = (completions: Array<WaterproofCompletion>, symbols: Ar
 	const cmCompletions =  completions.map((value) => {
 		return snippetCompletion(value.template, value);
 	}); 
-	return new ProsePlugin(CoqCodePluginSpec(cmCompletions, symbols, editorInstance, initialThemeStyle, languageConfig));
+	return new ProsePlugin(codePluginSpec(cmCompletions, symbols, editorInstance, initialThemeStyle, languageConfig));
 };
 

src/codeview/color-scheme.ts

@@ -1,8 +1,8 @@
 import { EditorView } from "@codemirror/view";
-import coqTheme from "./coqTheme.json";
+import codeTheme from "./codeTheme.json";
 
 /**
  * Inspired by:
  * https://github.com/codemirror/theme-one-dark/blob/main/src/one-dark.ts
  */
-export const customTheme = EditorView.theme(coqTheme, {dark: true});
+export const customTheme = EditorView.theme(codeTheme, {dark: true});

src/codeview/index.ts

@@ -1,4 +1,4 @@
 // Export the CodeBlockView class.
 export { CodeBlockView } from "./nodeview";
-// Export the coq plugin and plugin key for use in the prosemirror editor.
+// Export the code plugin and plugin key for use in the prosemirror editor.
 export { CODE_PLUGIN_KEY, codePlugin } from "./code-plugin";

src/codeview/nodeview.ts

@@ -273,7 +273,7 @@ export class CodeBlockView extends EmbeddedCodeMirrorEditor {
 		// Editors outer node is dom
 		this.dom = this._codemirror.dom;
 
-		// Fix the coqblock not being selectable when editing the markdown blocks.
+		// Fix the code block not being selectable when editing the markdown blocks.
 		this.dom.addEventListener("click", () => {
 			this._codemirror?.focus();
 			this.setEditPermission();
@@ -415,7 +415,7 @@ export class CodeBlockView extends EmbeddedCodeMirrorEditor {
 	}
 
 	/**
-	 * Add a new coq error to this view
+	 * Add a new diagnostic to this view
 	 * @param from The from position of the error.
 	 * @param to The to postion of the error (should be larger than `from`).
 	 * @param message The message attached to this error.

src/document/blocks/schema.ts

@@ -19,7 +19,7 @@ export const markdown = (content: string): ProseNode => {
     return WaterproofSchema.nodes.markdown.create({}, text(content));
 }
 
-/** Construct coqcode prosemirror node. */
+/** Construct code prosemirror node. */
 export const code = (content: string): ProseNode => {
     return WaterproofSchema.nodes.code.create({}, text(content));
 }

src/editor.ts

@@ -34,7 +34,7 @@ import { deleteSelection } from "./commands/commands";
 import { Mapping } from "./mapping";
 import { ProgressBar } from "./progressBar";
 
-/** Type that contains a coq diagnostics object fit for use in the ProseMirror editor context. */
+/** Type that contains a diagnostics object fit for use in the ProseMirror editor context. */
 export type DiagnosticObjectProse = {message: string, start: number, end: number, severity: Severity};
 
 /**
@@ -430,7 +430,7 @@ export class WaterproofEditor implements MessageHandlerEditor {
 	public handleCompletions(completions: Array<Completion>) {
 		const state = this._view?.state;
 		if (!state) return;
-		// Apply autocomplete to all coq cells
+		// Apply autocomplete to all code cells
 		CODE_PLUGIN_KEY
 			.getState(state)
 			?.activeNodeViews
@@ -744,7 +744,7 @@ export class WaterproofEditor implements MessageHandlerEditor {
 
 	private informCodemirrorViews() {
 		if (this._view === undefined) return;
-        // Get the available coq views
+        // Get the available code views
 		const views = CODE_PLUGIN_KEY.getState(this._view.state)?.activeNodeViews;
 		if (views === undefined) return;
 		for (const view of views) view.dispatchEmpty();

src/embedded-codemirror/embeddedCodemirror.ts

@@ -8,7 +8,7 @@ import { keybindings } from "./embedded-codemirror-keymap";
 /**
  * A class implementing everything required to create an embedded codemirror editor for prosemirror.
  * Implements the `NodeView` prosemirror class. Can be extended to create custom codemirror editors like
- * the one used to edit markdown or coq.
+ * the one used to edit markdown or code.
  */
 export class EmbeddedCodeMirrorEditor implements NodeView {
     public _getPos: (() => number | undefined);
@@ -192,7 +192,7 @@ export class EmbeddedCodeMirrorEditor implements NodeView {
 
 			switch (unit) {
 				case MovementUnit.line:
-					// We are moving up and down within the coq cell.
+					// We are moving up and down within the code cell.
 					// We get the line the cursor is currently in:
 					{ const currentLine = _state.doc.lineAt(_mainSelection.head);
 					if (dir == MovementDirection.backward) {

src/markup-views/index.ts

@@ -1,2 +1,2 @@
-// Export the CoqdocView editor view.
+// Export the switchable view plugin.
 export { switchableViewPlugin, SWITCHABLE_VIEW_PLUGIN_KEY } from "./SwitchableViewPlugin";

src/markup-views/switchable-view/EditableView.ts

@@ -48,7 +48,7 @@ export class EditableView extends EmbeddedCodeMirrorEditor {
 				CodeMirror.updateListener.of(update => this.forwardUpdate(update)),
 				placeholder("Empty..."),
 				autocompletion({
-					// In the markdown / coqdoc editing add the symbol and emoji completions.
+					// In the markdown / code editing add the symbol and emoji completions.
 					// override: [symbolCompletionSource],
 					icons: false,
 					addToOptions: [renderIcon]

src/qedStatus.ts

@@ -66,15 +66,15 @@ const UpdateStatusPluginSpec = (editor: WaterproofEditor): PluginSpec<IUpdateSta
               const newStatusUpdate = statusUpdate[index];
               if (inputNode.node.attrs.status !== newStatusUpdate) {
                 // This is (probably) the place where we check for errors in the proof.
-                // A proof should not be accepted if it includes a faulty coq statement.
+                // A proof should not be accepted if it includes a faulty piece of code.
 
                 const start = inputNode.pos;
                 const end = start + inputNode.node.nodeSize;
                 const thingies = editor.getDiagnosticsInRange(start, end, 1);
                 let className = statusToDecoration(newStatusUpdate);
                 if (thingies.length > 0) {
                   if (thingies.find((value) => value.severity == Severity.Error)) {
-                    // Coq error in proof.
+                    // Error in code.
                     className += " contains-error";
                   } else {
                     className += " contains-warning";