Trimming whitespace fix

.github/workflows/unit-tests.yml

@@ -14,7 +14,7 @@ jobs:
 
     strategy:
       matrix:
-        os: [ubuntu-latest, macos-latest, windows-latest]
+        os: [ubuntu-latest]
         node-version: [16.x]
 
     steps:

.gitignore

@@ -5,8 +5,10 @@ node_modules/
 editor_output
 .DS_store
 .vscode-test
+.vscode-test-web
 test_out/
 .ui-test/
 __tests_output__/
 **/*.cache
 ExampleFiles/
+/cypress/screenshots/

.vscode/settings.json

@@ -1,3 +1,15 @@
 {
-    "js/ts.implicitProjectConfig.target": "ESNext"
+    "js/ts.implicitProjectConfig.target": "ESNext",
+    "files.exclude": {
+        "**/*.vo": true,
+        "**/*.vok": true,
+        "**/*.vos": true,
+        "**/*.aux": true,
+        "**/*.glob": true,
+        "**/.git": true,
+        "**/.svn": true,
+        "**/.hg": true,
+        "**/.DS_Store": true,
+        "**/Thumbs.db": true
+    }
 }

.vscodeignore

@@ -21,4 +21,6 @@ tsconfig-base.json
 tsconfig.json
 .github/
 ExampleFiles/
-developer-resources/
+developer-resources/
+scripts/
+docs/

README.md

@@ -2,6 +2,10 @@
 
 The Waterproof vscode extension helps students learn how to write mathematical proofs.
 
+1. [Automatic Installation](#quick-install-instructions-for-windows)
+2. [Manual Installation](#more-extensive-installation-instructions)
+3. [Getting Started](#getting-started)
+
 # Quick install instructions for Windows
 
 Install this extension and follow the installation instructions that pop up.
@@ -104,9 +108,7 @@ If vscode cannot detect the installation, set the coq-lsp path to the output of
 using ctrl+shift+p and selecting "Waterproof: Change Waterproof path".
 Alternatively, make sure that the `PATH` available to vscode contains the coq-lsp binary.
 
-## Manual Installation on Mac
-
-If the above method did not work for Mac, it is possible to instead install the dependencies manually using opam.
+## Installation on Mac
 
 ### Step 1: Install this [Waterproof vscode extension](https://marketplace.visualstudio.com/items?itemName=waterproof-tue.waterproof)
 
@@ -132,3 +134,14 @@ eval $(opam env)
 opam install coq-lsp.0.2.2+8.17
 opam install coq-waterproof
 ```
+
+# Getting Started
+
+### Tutorial
+To get started with Waterproof, we recommend going through the tutorial. The tutorial can be accessed in VS Code by pressing `Ctrl-Shift-P` (this opens the command palette), typing `open tutorial` until you find the option `Waterproof: Open Tutorial`.
+
+### Tactics
+Waterproof makes use of 'tactics', information on the available tactics, together with explanations and examples can be accessed via the extension or through the repository:
+
+* From the Waterproof extension: Navigate to the Waterproof sidebar (accessible via the droplet icon on the left) and click on the `Tactics` button. The panel that now opens shows all available tactics.
+* From the repository: The repository contains a [Markdown](/docs/tactics-sheet.md) version of the tactics sheet.

__tests__/editor-content-construction.test.ts

@@ -1,4 +1,4 @@
-import { checkPrePost, fixLessThanBug } from "../editor/src/kroqed-editor/file-utils";
+import { checkPrePost, fixLessThanBug } from "../editor/src/waterproof-editor/file-utils";
 import { Message, MessageType } from "../shared";
 
 class PostManager {
@@ -38,10 +38,10 @@ test("TEMP: Add space between '<' and characters following it #4", () => {
     const pm = new PostManager();
     expect(fixLessThanBug("```coq\n10<10\n```", (msg) => pm.post(msg))).toBe("```coq\n10< 10\n```");
     expect(pm.storage).toStrictEqual<Array<Message>>([{
-        type: MessageType.docChange, 
+        type: MessageType.docChange,
         body: {
             startInFile: 10,
-            endInFile: 10, 
+            endInFile: 10,
             finalText: " "
         }
     }]);
@@ -51,10 +51,10 @@ test("TEMP: Add space between '<' and characters following it #5", () => {
     const pm = new PostManager();
     expect(fixLessThanBug("<input-area>\n10<z\n</input-area>", (msg) => pm.post(msg))).toBe("<input-area>\n10< z\n</input-area>");
     expect(pm.storage).toStrictEqual<Array<Message>>([{
-        type: MessageType.docChange, 
+        type: MessageType.docChange,
         body: {
-            startInFile: 16, 
-            endInFile: 16, 
+            startInFile: 16,
+            endInFile: 16,
             finalText: " "
         }
     }]);
@@ -84,8 +84,8 @@ test("TEMP: Leave <br> in markdown untouched #2", () => {
     expect(pm.storage).toStrictEqual<Array<Message>>([{
         type: MessageType.docChange,
         body: {
-            startInFile: 19, 
-            endInFile: 19, 
+            startInFile: 19,
+            endInFile: 19,
             finalText: " "
         }
     }]);
@@ -103,8 +103,8 @@ test("TEMP: Leave <hr> in markdown untouched #2", () => {
     expect(pm.storage).toStrictEqual<Array<Message>>([{
         type: MessageType.docChange,
         body: {
-            startInFile: 19, 
-            endInFile: 19, 
+            startInFile: 19,
+            endInFile: 19,
             finalText: " "
         }
     }]);

__tests__/mathinline.test.ts

@@ -1,4 +1,4 @@
-import { toMathInline } from "../editor/src/kroqed-editor/translation/toProsemirror/parser"
+import { toMathInline } from "../editor/src/waterproof-editor/translation/toProsemirror/parser"
 
 
 test("Replace $ inside of markdown", () => {

__tests__/mv-mapping.test.ts

@@ -1,9 +1,9 @@
 /* eslint-disable @typescript-eslint/ban-ts-comment */
 // Disable because the @ts-expect-error clashes with the tests
-import { TextDocMappingMV as TextDocMapping } from "../editor/src/kroqed-editor/mappingModel/mvFile";
+import { TextDocMappingMV as TextDocMapping } from "../editor/src/mapping/mvFile";
 import { ReplaceStep } from "prosemirror-transform";
-import { WaterproofSchema } from "../editor/src/kroqed-editor/schema";
-import { translateMvToProsemirror } from "../editor/src/kroqed-editor/translation/toProsemirror";
+import { WaterproofSchema } from "../editor/src/waterproof-editor/schema";
+import { translateMvToProsemirror } from "../editor/src/waterproof-editor/translation/toProsemirror";
 import { expect } from "@jest/globals";
 
 test("Normal coqdown", () => {

__tests__/mvFileToProsemirror.test.ts

@@ -1,6 +1,6 @@
 /* eslint-disable no-useless-escape */
 // Disable due to test data including latex code
-import { translateMvToProsemirror } from "../editor/src/kroqed-editor/translation/toProsemirror/mvFileToProsemirror";
+import { translateMvToProsemirror } from "../editor/src/waterproof-editor/translation/toProsemirror/mvFileToProsemirror";
 import { expect } from "@jest/globals";
 
 test("Expect empty input to return empty output", () => {
@@ -72,7 +72,7 @@ test("entire document", () => {
 })
 
 test("entire document2", () => {
-    const docString = `# This is a header. 
+    const docString = `# This is a header.
 
 This is a paragraph. Paragraphs support inline LaTeX like $5+3=22$. Underneath you'll find a math display block.
 $$
@@ -102,7 +102,7 @@ Proof.
   - simpl. rewrite IHl. simpl. reflexivity.
 Qed.
 \`\`\``
-    const predict = `<markdown># This is a header. 
+    const predict = `<markdown># This is a header.
 
 This is a paragraph. Paragraphs support inline LaTeX like $5+3=22$. Underneath you'll find a math display block.
 </markdown><math-display>

__tests__/parser.test.ts

@@ -1,4 +1,4 @@
-import { translateCoqDoc } from "../editor/src/kroqed-editor/translation/toProsemirror/parser";
+import { translateCoqDoc } from "../editor/src/waterproof-editor/translation/toProsemirror/parser";
 
 
 /*
@@ -82,12 +82,12 @@ test("Preserves whitespace inside coq code cell.", () => {
 
 
 test("From indented list in Coqdoc comments, make markdown list", () => {
-    
+
     expect(translateCoqDoc("- First item\n- Second item\n  - Indented item\n  - Second indented item\n- Third item"))
     .toBe(`- First item\n- Second item\n    - Indented item\n    - Second indented item\n- Third item`);
 });
 
-/* TEMPLATE 
+/* TEMPLATE
 test("name", () => {
     expect(translateCoqDoc("input")).toBe("expected output");
 });

__tests__/prosedoc-construction/block-extractions.test.ts

@@ -1,5 +1,5 @@
-import { extractCoqBlocks, extractCoqDoc, extractHintBlocks, extractInputBlocks, extractMathDisplayBlocks, extractMathDisplayBlocksCoqDoc } from "../../editor/src/kroqed-editor/prosedoc-construction/block-extraction";
-import { isCoqBlock, isCoqDocBlock, isHintBlock, isInputAreaBlock, isMathDisplayBlock } from "../../editor/src/kroqed-editor/prosedoc-construction/blocks/typeguards";
+import { extractCoqBlocks, extractCoqDoc, extractHintBlocks, extractInputBlocks, extractMathDisplayBlocks, extractMathDisplayBlocksCoqDoc } from "../../editor/src/document-construction/block-extraction";
+import { isCoqBlock, isCoqDocBlock, isHintBlock, isInputAreaBlock, isMathDisplayBlock } from "../../editor/src/waterproof-editor/document/blocks/typeguards";
 
 test("Identify input blocks", () => {
     const document = "# Example\n<input-area>\n# Test input area\n</input-area>\n";

__tests__/prosedoc-construction/inner-blocks.test.ts

@@ -1,10 +1,10 @@
-import { createCoqDocInnerBlocks, createCoqInnerBlocks, createInputAndHintInnerBlocks } from "../../editor/src/kroqed-editor/prosedoc-construction/blocks/inner-blocks";
-import { isCoqCodeBlock, isCoqDocBlock, isCoqMarkdownBlock, isMathDisplayBlock } from "../../editor/src/kroqed-editor/prosedoc-construction/blocks/typeguards";
+import { createCoqDocInnerBlocks, createCoqInnerBlocks, createInputAndHintInnerBlocks } from "../../editor/src/document-construction/inner-blocks";
+import { isCoqCodeBlock, isCoqDocBlock, isCoqMarkdownBlock, isMathDisplayBlock } from "../../editor/src/waterproof-editor/document/blocks/typeguards";
 import { expect } from "@jest/globals";
 
 test("Inner input area (and hint) blocks", () => {
     const inputAreaContent = "$$1028 + 23 = ?$$\n```coq\nCompute 1028 + 23.\n```";
-    
+
     const blocks = createInputAndHintInnerBlocks(inputAreaContent);
 
     expect(blocks.length).toBe(2);
@@ -28,7 +28,7 @@ test("Inner coq blocks", () => {
     // One block for the coq content and one block for the comment.
     expect(blocks.length).toBe(2);
     expect(isCoqCodeBlock(blocks[0])).toBe(true);
-    
+
     expect(blocks[0].stringContent).toBe("Compute 1 + 1.");
     expect(blocks[0].range.from).toBe(0);
     expect(blocks[0].range.to).toBe(14);
@@ -37,7 +37,7 @@ test("Inner coq blocks", () => {
     expect(blocks[1].stringContent).toBe("* Header ");
     expect(blocks[1].range.from).toBe(14);
     expect(blocks[1].range.to).toBe(coqContent.length);
-    
+
     expect(blocks[1].innerBlocks?.length).toBe(1);
     expect(isCoqMarkdownBlock(blocks[1].innerBlocks![0])).toBe(true);
 });

__tests__/prosedoc-construction/top-level-construction.test.ts

@@ -1,9 +1,9 @@
 /* eslint-disable no-useless-escape */
 // Disable due to latex code in sample data
-import { topLevelBlocksMV, topLevelBlocksV } from "../../editor/src/kroqed-editor/prosedoc-construction";
+import { blocksFromMV, blocksFromV } from "../../editor/src/document-construction/construct-document";
 import { expect } from '@jest/globals';
-import { MarkdownBlock } from "../../editor/src/kroqed-editor/prosedoc-construction/blocks/blocktypes";
-import { isHintBlock, isInputAreaBlock, isMarkdownBlock, isMathDisplayBlock, isCoqBlock } from "../../editor/src/kroqed-editor/prosedoc-construction/blocks/typeguards";
+import { MarkdownBlock } from "../../editor/src/waterproof-editor/document/blocks";
+import { isHintBlock, isInputAreaBlock, isMarkdownBlock, isMathDisplayBlock, isCoqBlock } from "../../editor/src/waterproof-editor/document/blocks/typeguards";
 
 const inputDocumentMV = `# Example document
 <hint title="example hint (like for imports)">
@@ -31,27 +31,27 @@ Random Markdown list:
 
 // FIXME: Add checks for prewhite and postwhite here.
 test("Parse top level blocks (MV)", () => {
-    const blocks = topLevelBlocksMV(inputDocumentMV);
+    const blocks = blocksFromMV(inputDocumentMV);
     expect(blocks.length).toBe(8);
 
     expect(isMarkdownBlock(blocks[0])).toBe(true);
     expect(blocks[0].stringContent).toBe("# Example document\n");
-    
+
     expect(isHintBlock(blocks[1])).toBe(true);
     expect(blocks[1].stringContent).toBe("\n```coq\nRequire Import ZArith.\n```\n");
-    
+
     expect(isMarkdownBlock(blocks[2])).toBe(true);
     expect((blocks[2] as MarkdownBlock).isNewLineOnly).toBe(true);
 
     expect(isInputAreaBlock(blocks[3])).toBe(true);
     expect(blocks[3].stringContent).toBe("\n$$1028 + 23 = ?$$\n```coq\nCompute 1028 + 23.\n```\n");
-    
+
     expect(isMarkdownBlock(blocks[4])).toBe(true);
     expect(blocks[4].stringContent).toBe("\n#### Markdown content\n");
-    
+
     expect(isMathDisplayBlock(blocks[5])).toBe(true);
     expect(blocks[5].stringContent).toBe(" \int_0^2 x dx ");
-    
+
     expect(isCoqBlock(blocks[6])).toBe(true);
     expect(blocks[6].stringContent).toBe("Compute 1 + 1.");
 
@@ -74,7 +74,7 @@ Qed.
 `;
 
 test("Parse top level blocks (V)", () => {
-    const blocks = topLevelBlocksV(inputDocumentV);
+    const blocks = blocksFromV(inputDocumentV);
     // coqblock, hint, input, coqblock
 
     expect(blocks.length).toBe(4);

__tests__/prosedoc-construction/utils.test.ts

@@ -1,6 +1,6 @@
-import { Block } from "../../editor/src/kroqed-editor/prosedoc-construction/blocks";
-import { text } from "../../editor/src/kroqed-editor/prosedoc-construction/blocks/schema";
-import { extractInterBlockRanges, iteratePairs, maskInputAndHints, sortBlocks } from "../../editor/src/kroqed-editor/prosedoc-construction/utils";
+import { Block } from "../../editor/src/waterproof-editor/document/blocks";
+import { text } from "../../editor/src/waterproof-editor/document/blocks/schema";
+import { extractInterBlockRanges, iteratePairs, maskInputAndHints, sortBlocks } from "../../editor/src/waterproof-editor/document/utils";
 
 const toProseMirror = () => text("null");
 const debugPrint = () => null;
@@ -9,7 +9,7 @@ test("Sort blocks #1", () => {
     const stringContent = "";
 
     const testBlocks = [
-        {type: "second", range: {from: 1, to: 2}, stringContent, toProseMirror, debugPrint}, 
+        {type: "second", range: {from: 1, to: 2}, stringContent, toProseMirror, debugPrint},
         {type: "first", range: {from: 0, to: 1}, stringContent, toProseMirror, debugPrint}
     ];
 
@@ -23,7 +23,7 @@ test("Sort blocks #2", () => {
     const stringContent = "";
 
     const testBlocks = [
-        {type: "second", range: {from: 1, to: 2}, stringContent, toProseMirror, debugPrint}, 
+        {type: "second", range: {from: 1, to: 2}, stringContent, toProseMirror, debugPrint},
         {type: "first", range: {from: 0, to: 1}, stringContent, toProseMirror, debugPrint},
         {type: "third", range: {from: 2, to: 3}, stringContent, toProseMirror, debugPrint}
     ];
@@ -40,7 +40,7 @@ test("Sort blocks #2", () => {
 //     const stringContent = "";
 //     const toProseMirror = () => null;
 //     const testBlocks = [
-//         {type: "second", range: {from: 0, to: 1}, stringContent, toProseMirror}, 
+//         {type: "second", range: {from: 0, to: 1}, stringContent, toProseMirror},
 //         {type: "first", range: {from: 0, to: 1}, stringContent, toProseMirror}
 //     ];
 

cypress/e2e/basic.cy.ts

@@ -13,8 +13,8 @@ describe('Basic tests', () => {
   it('Editor opens, contains all parts and displays file', () => {
     // Editor is visible
     cy.get("#editor").should("be.visible");
-    // Menubar is visible
-    cy.get(".menubar").should("be.visible");
+    // Menubar is not visible by default
+    cy.get(".menubar").should("not.be.visible");
 
     // Progress bar is visible
     // TODO: Progress bar only appears after clicking in the editor?
@@ -32,7 +32,9 @@ describe('Basic tests', () => {
 
     // TODO: This also immediately opens the markdown editor for the H1
     cy.window().then((win) => { win.postMessage({type: MessageType.teacher, body: true}) });
-    cy.get('coqblock > .cm-editor > .cm-scroller > .cm-content').click(); // to reset h1
+    // now that we are in teacher mode the menubar should be visible
+    cy.get(".menubar").should("be.visible");
+    cy.get("coqblock > .cm-editor > .cm-scroller > .cm-content").click(); // to reset h1
     cy.get("#editor h1").should("be.visible");
     cy.get("#editor h1").click();
     cy.get(".markdown-view").should("be.visible");
@@ -42,7 +44,7 @@ describe('Basic tests', () => {
     cy.window().then((win) => { win.postMessage({type: MessageType.teacher, body: true}) });
     cy.get(".markdown-view").type("\n## Hello World");
     cy.get(".markdown-view").should("contain.text", "Hello World");
-    cy.nthCoqCode(0).click(); // to reset h1
+    cy.nthCode(0).click(); // to reset h1
     cy.get("H2").should("exist");
 
     // We record edits in the 'edits' global variable

cypress/e2e/line-numbers.cy.ts

@@ -4,7 +4,7 @@ import { MessageType } from "../../shared";
 import { setupTest } from "./util";
 
 const edits = [];
-const initialDocument = "# Title\n<input-area>\n```coq\nDefinition foo := 42.\n```\n</input-area>\n";
+const initialDocument = "# Title\n```coq\nDefinition foo := 42.\n```\n";
 
 const callbacks = {
     [MessageType.lineNumbers]: (data: { linenumbers: number[]; }) => {
@@ -29,7 +29,9 @@ describe('Line numbers', () => {
   beforeEach(() => { setupTest(initialDocument, edits, callbacks); });
 
   it("Toggle display of line numbers", () => {
+    // CodeMirror Editor should exist
     cy.get('.cm-content').should("exist");
+    // The line number gutter should not exist
     cy.get('.cm-gutter').should("not.exist");
     cy.window().then((win) => {
         win.postMessage({
@@ -39,7 +41,8 @@ describe('Line numbers', () => {
     });
     cy.wait(1);
     cy.get('.cm-gutter').should("exist");
-    cy.get('.cm-gutter').should("contain", "4");
+    // Third line contains the coq code
+    cy.get('.cm-gutter').should("contain", "3");
     cy.window().then((win) => {
         win.postMessage({
             type: MessageType.setShowLineNumbers,