Containers + bugfixes

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

@@ -185,28 +185,29 @@ test("Parse top level blocks (Lean)", () => {
     const blocks = topLevelBlocksLean(inputDocumentLean);
     expect(blocks.length).toBe(8);
 
-    const [preamble, md1, code, nl2, input, md2, math, md3] = blocks;
+    const [preamble, md1, nl1, container, nl2, md2, math, md3] = blocks;
 
     expect(typeguards.isHintBlock(preamble)).toBe(true);
     expect(preamble.stringContent).toBe("import Some.Library\n#doc (Genre) \"Title\" =>\n");
 
-    // TODO: After we have come up with a solution for the multilean tags,
-    // we should check the \n here very carefully.
     expect(typeguards.isMarkdownBlock(md1)).toBe(true);
-    expect(md1.stringContent).toBe("# A Header\n");
+    expect(md1.stringContent).toBe("# A Header");
 
-    expect(typeguards.isCodeBlock(code)).toBe(true);
-    expect(code.stringContent).toBe("def fortyTwo :=\n  30 +");
+    expect(typeguards.isNewlineBlock(nl1)).toBe(true);
 
-    expect(typeguards.isNewlineBlock(nl2)).toBe(true);
+    expect(typeguards.isContainerBlock(container)).toBe(true);
+    expect(container.innerBlocks!.length).toBe(3);
+    const [innerCode, innerNl, innerInput] = container.innerBlocks!;
+    expect(typeguards.isCodeBlock(innerCode)).toBe(true);
+    expect(innerCode.stringContent).toBe("def fortyTwo :=\n  30 +");
+    expect(typeguards.isNewlineBlock(innerNl)).toBe(true);
+    expect(typeguards.isInputAreaBlock(innerInput)).toBe(true);
+    expect(innerInput.stringContent).toBe("```lean\n  12\n```");
 
-    expect(typeguards.isInputAreaBlock(input)).toBe(true);
-    expect(input.stringContent).toBe("```lean\n  12\n```");
+    expect(typeguards.isNewlineBlock(nl2)).toBe(true);
 
-    // TODO: After we have come up with a solution for the multilean tags,
-    // we should check the \n here very carefully.
     expect(typeguards.isMarkdownBlock(md2)).toBe(true);
-    expect(md2.stringContent).toBe("\n## Markdown Content\n");
+    expect(md2.stringContent).toBe("## Markdown Content\n");
 
     expect(typeguards.isMathDisplayBlock(math)).toBe(true);
     expect(math.stringContent).toBe("x^2 + y = z");
@@ -216,34 +217,12 @@ test("Parse top level blocks (Lean)", () => {
         .toBe("\nA list:\n  1. *Italicized* text\n  2. $`y = z - x^2`\n  3. `Inline code`\n");
 })
 
-// TODO: The serialization logic should account for the multilean tags, which it doesnt at the moment.
 test("Parse and serialize document (Lean)", () => {
     const doc = constructDocument(topLevelBlocksLean(inputDocumentLean));
     const out = new LeanSerializer().serializeDocument(doc);
 
-    const outputDocumentLean = `import Some.Library
-#doc (Genre) "Title" =>
-# A Header
-\`\`\`lean
-def fortyTwo :=
-  30 +
-\`\`\`
-:::input
-\`\`\`lean
-  12
-\`\`\`
-:::
-## Markdown Content
-$$\`x^2 + y = z\`
-A list:
-  1. *Italicized* text
-  2. $\`y = z - x^2\`
-  3. \`Inline code\`
-`;
-
-    // We would want this operation to be the identity, i.e.
-    // expect(out).toBe(inputDocumentLean);
-    expect(out).toBe(outputDocumentLean);
+    // Serialization is the identity: multilean tags are preserved.
+    expect(out).toBe(inputDocumentLean);
 })
 
 test("Markdown and Code (Lean)", () => {

editor/src/document-construction/lean.ts

@@ -1,4 +1,4 @@
-import { Block, BlockRange, CodeBlock, HintBlock, InputAreaBlock, MarkdownBlock, MathDisplayBlock, NewlineBlock, WaterproofDocument } from "@impermeable/waterproof-editor";
+import { Block, BlockRange, CodeBlock, ContainerBlock, HintBlock, InputAreaBlock, MarkdownBlock, MathDisplayBlock, NewlineBlock, WaterproofDocument } from "@impermeable/waterproof-editor";
 
 enum Kind {
     Text,
@@ -61,7 +61,7 @@ const regexes: [RegExp, Kind][] = [
     [/(?<=\n)```lean\n/,                  Kind.CodeOpen       ],
     [/\n```(?=\n|$)/,                     Kind.CodeClose      ],
     [/(?<=\n):::input\n/,                 Kind.InputOpen      ],
-    [/(?<=\n):::hint "(?<HintTitle>[\s\S]*?)"(?=\n)/, Kind.HintOpen       ],
+    [/(?<=\n):::hint "(?<HintTitle>[\s\S]*?)"\n/,     Kind.HintOpen       ],
     [/\n:::(?=\n|$)/,                     Kind.Close          ],
     [/\$`[\s\S]*?`/,                      Kind.MathInline     ],
     [/\$\$`[\s\S]*?`/,                    Kind.MathDisplay    ],
@@ -101,8 +101,8 @@ function expect(token: Token | undefined, kinds?: Kind[]): Token {
 function handle(doc: string, token: Token, blocks: Block[]): Token | undefined {
     const isSignificantNewline = (token: Token) =>
         token.kind === Kind.Newline
-        && (token.prev?.isOneOf([Kind.Close])
-            || token.next?.isOneOf([Kind.CodeOpen, Kind.InputOpen, Kind.HintOpen]));
+        && (token.prev?.isOneOf([Kind.Close, Kind.CodeClose, Kind.MultileanClose])
+            || token.next?.isOneOf([Kind.CodeOpen, Kind.InputOpen, Kind.HintOpen, Kind.MultileanOpen]));
 
     if (token.kind === Kind.Preamble) {
         const range = token.range;
@@ -182,9 +182,22 @@ function handle(doc: string, token: Token, blocks: Block[]): Token | undefined {
         blocks.push(new MathDisplayBlock(content, range, innerRange, token.line));
 
         return token.next;
-    } else if (token.isOneOf([Kind.MultileanOpen, Kind.MultileanClose])) {
-        // We skip to the next token as we don't want the multilean tags to be shown in the editor.
-        return token.next;
+    } else if (token.kind === Kind.MultileanOpen) {
+        const expected: Kind[] = [
+            Kind.MultileanClose,
+            Kind.Text, Kind.MathInline, Kind.MathDisplay,
+            Kind.CodeOpen, Kind.InputOpen, Kind.HintOpen, Kind.Newline,
+        ];
+        let head: Token = expect(token.next, expected);
+        const innerBlocks: Block[] = [];
+        while (head && head.kind !== Kind.MultileanClose) {
+            head = expect(handle(doc, head, innerBlocks));
+        }
+        const range = { from: token.range.from, to: head.range.to };
+        const innerRange = { from: token.range.to, to: head.range.from };
+        const content = doc.substring(innerRange.from, innerRange.to);
+        blocks.push(new ContainerBlock(content, "multilean", range, innerRange, token.line, innerBlocks));
+        return head.next;
     } else {
         throw Error(`Unexpected token ${token.kind}`);
     }

editor/src/index.ts

@@ -1,5 +1,5 @@
 import { FileFormat, Message, MessageType } from "../../shared";
-import { defaultToMarkdown, markdown, ThemeStyle, WaterproofEditor, WaterproofEditorConfig } from "@impermeable/waterproof-editor";
+import { defaultToMarkdown, markdown, ThemeStyle, WaterproofEditor, WaterproofEditorConfig, wrapInContainer } from "@impermeable/waterproof-editor";
 // TODO: The tactics completions are static, we want them to be dynamic (LSP supplied and/or configurable when the editor is running)
 import waterproofTactics from "../../completions/tactics.json";
 import leanTactics from "../../completions/tacticsLean.json";
@@ -29,9 +29,9 @@ interface VSCodeAPI {
 	postMessage: (message: Message) => void;
 }
 
-function createConfiguration(format: FileFormat, codeAPI: VSCodeAPI) {
-	let formatConf: Pick<WaterproofEditorConfig, 
-		"completions" | "documentConstructor" | "toMarkdown" | "markdownName" | "tagConfiguration" | "languageConfig" | "disableMarkdownFeatures" | "serializer" >;
+function createConfiguration(format: FileFormat, codeAPI: VSCodeAPI, editorRef: { current?: WaterproofEditor }) {
+	let formatConf: Pick<WaterproofEditorConfig,
+		"completions" | "documentConstructor" | "toMarkdown" | "markdownName" | "tagConfiguration" | "languageConfig" | "disableMarkdownFeatures" | "serializer" | "menubarEntries" >;
 
 	// Set format-specific configuration
 	switch (format) {
@@ -77,6 +77,17 @@ function createConfiguration(format: FileFormat, codeAPI: VSCodeAPI) {
 					highlightLight: langVerbose.highlight_light,
 					languageSupport: langVerbose.verbose(),
 				},
+				menubarEntries: [
+					{
+						title: "M...",
+						hoverText: "Wrap selection in a container (groups math evaluation)",
+						callback: () => {
+							editorRef.current?.executeProsemirrorCommand(wrapInContainer(tagConfigurationLean, "multilean"));
+						},
+						isActive: (state) => wrapInContainer(tagConfigurationLean, "multilean")(state, undefined),
+						buttonVisibility: { teacherModeOnly: true },
+					}
+				],
 			}
 			break;
 	}
@@ -130,8 +141,11 @@ window.onload = () => {
 	}
 	const format = document.body.getAttribute("format") as FileFormat;
 
+	// Create a ref so that menubar callbacks can dispatch commands after the editor is constructed.
+	const editorRef: { current?: WaterproofEditor } = {};
+
 	// Create the editor, passing it the vscode api and the editor and content HTML elements.
-	const cfg = createConfiguration(format, codeAPI);
+	const cfg = createConfiguration(format, codeAPI, editorRef);
 	// Retrieve the current theme style from the attribute 'data-theme-kind'
 	// attached to the editor element. This allows us to set the initial theme kind
 	// rather than waiting for the themestyle message to arrive.
@@ -148,6 +162,7 @@ window.onload = () => {
 		}
 	})();
 	const editor = new WaterproofEditor(editorElement, cfg, themeStyle);
+	editorRef.current = editor;
 
 	//@ts-expect-error For now, expose editor in the window. Allows for calling editorInstance methods via the debug console.
 	window.editorInstance = editor;

editor/src/leanFileConfiguration.ts

@@ -6,7 +6,7 @@ export const tagConfigurationLean: TagConfiguration = {
 		openRequiresNewline: true, closeRequiresNewline: true
 	},
 	hint: {
-		openTag: (title) => `:::hint ${title}\n`,
+		openTag: (title) => `:::hint "${title}"\n`,
 		closeTag: "\n:::",
 		openRequiresNewline: true,
 		closeRequiresNewline: true,
@@ -26,5 +26,10 @@ export const tagConfigurationLean: TagConfiguration = {
 	math: {
 		openTag: "$$`", closeTag: "`",
 		openRequiresNewline: false, closeRequiresNewline: false,
-	}
+	},
+	container: {
+		openTag: (name: string) => `::::${name}\n`,
+		closeTag: "\n::::",
+		openRequiresNewline: true, closeRequiresNewline: true,
+	},
 }

editor/src/leanSerializer.ts

@@ -50,4 +50,11 @@ export class LeanSerializer extends DocumentSerializer {
     ): string {
         return this.tagSerializer.serializeMath(mathNode);
     }
+
+    serializeContainer(
+        containerNode: Node, _parentNode: string | null,
+        _neighbors: (skipNewlines: boolean) => Neighborhood
+    ): string {
+        return this.tagSerializer.serializeContainer(containerNode);
+    }
 }

editor/src/vFileConfiguration.ts

@@ -26,5 +26,10 @@ export const tagConfigurationV: TagConfiguration = {
 	math: {
 		openTag: "$", closeTag: "$",
 		openRequiresNewline: false, closeRequiresNewline: false,
-	}
+	},
+	container: {
+		openTag: (_name: string) => "",
+		closeTag: "",
+		openRequiresNewline: false, closeRequiresNewline: false,
+	},
 }

esbuild.mjs

@@ -2,6 +2,16 @@
 import process from "process";
 import * as esbuild from "esbuild";
 import copy from "esbuild-plugin-copy";
+import path from "path";
+import { existsSync } from "fs";
+
+// Resolve a package to its root directory, following npm workspace hoisting.
+// Checks the local node_modules first, then walks up to the workspace root.
+const resolvePackage = (pkg) => {
+  const local = path.resolve("./node_modules", pkg);
+  if (existsSync(local)) return local;
+  return path.resolve("../node_modules", pkg);
+};
 
 const watch = process.argv.includes("--watch");
 const minify = process.argv.includes("--minify");
@@ -43,12 +53,12 @@ const editorConfig = {
     ".grammar": "file"
 	},
   alias: {
-    '@codemirror/autocomplete': './node_modules/@codemirror/autocomplete',
-    '@codemirror/commands': './node_modules/@codemirror/commands',
-    '@codemirror/language': './node_modules/@codemirror/language',
-    '@codemirror/lint': './node_modules/@codemirror/lint',
-    '@codemirror/state': './node_modules/@codemirror/state',
-    '@codemirror/view': './node_modules/@codemirror/view',
+    '@codemirror/autocomplete': resolvePackage('@codemirror/autocomplete'),
+    '@codemirror/commands': resolvePackage('@codemirror/commands'),
+    '@codemirror/language': resolvePackage('@codemirror/language'),
+    '@codemirror/lint': resolvePackage('@codemirror/lint'),
+    '@codemirror/state': resolvePackage('@codemirror/state'),
+    '@codemirror/view': resolvePackage('@codemirror/view'),
   },
   minify,
   plugins: [watchPlugin("editor")]