[jscoq] Add markdown preview to document, connect to button.

We add a rich markdown preview for the document.

Makefile

@@ -179,7 +179,8 @@ distclean: clean
 dist: dist-npm dist-tarball
 
 BUILDOBJ = ${addprefix $(BUILDDIR)/./, \
-	jscoq.js coq-pkgs frontend backend dist examples docs}
+	jscoq.js coq-pkgs frontend backend dist examples docs \
+	node_modules/ocaml-wasm node_modules/@ocaml-wasm }
 DISTOBJ = README.md index.html package.json package-lock.json $(BUILDOBJ)
 DISTDIR = _build/dist
 
@@ -234,6 +235,9 @@ dist-npm-wacoq:
 # is absolutely bothersome. I could not conjure a more sustainable way to emit
 # two separate NPM packages from the same source tree, though.
 
+# I think in our case makes sense to have a single package, that
+# includes both workers build, and is selectable, as for editors.
+
 ########################################################################
 # Externals
 ########################################################################

backend/wasm/wacoq_worker.ts

@@ -9,7 +9,7 @@ function postMessage(msg) {
 
 async function main() {
     /** @note when serving from source tree, the `node_modules` ref works by chance */
-    var icoq = new IcoqPod('../backend/wasm', '../../../node_modules');
+    var icoq = new IcoqPod('../backend/wasm', '../node_modules');
 
     postMessage(['Starting']);
     icoq.on('message', postMessage);

esbuild.mjs

@@ -65,7 +65,10 @@ var frontend = esbuild
     format: "esm",
     loader: {
       '.png': 'binary',
-      '.svg': 'dataurl'
+      '.svg': 'dataurl',
+      '.ttf': 'dataurl',
+      '.woff': 'dataurl',
+      '.woff2': 'dataurl',
     },
     metafile: enableMeta,
     outdir: "dist/frontend",

frontend/classic/js/coq-editor-mdview.tsx

@@ -0,0 +1,44 @@
+import { ICoqEditor, ICoqEditorConstructor } from "./coq-editor";
+import React from 'react';
+import MarkdownPreview from '@uiw/react-markdown-preview';
+import { Diagnostic } from "../../../backend";
+import { Root, createRoot } from 'react-dom/client';
+import { CoqDocument } from "./coq-manager";
+import rehypeKatex from 'rehype-katex';
+import remarkMath from 'remark-math';
+import 'katex/dist/katex.css';
+
+export class CoqMdViewEditor implements ICoqEditor {
+    root : Root;
+
+    constructor(doc : CoqDocument, options)  {
+        this.root = createRoot(doc.container);
+        this.root.render(<MarkdownPreview source={doc.area.value}
+            remarkPlugins={[remarkMath]}
+            rehypePlugins={[rehypeKatex]} />);
+    }
+    destroy(): void {
+        this.root.unmount();
+    }
+    getValue(): string {
+        return "";
+    }
+    getCursorOffset(): number {
+        return 0;
+    }
+    clearDiagnostics(): void {
+
+    }
+    markDiagnostic(diag: Diagnostic): void {
+
+    }
+    configure(opts: any): void {
+
+    }
+    openFile(file: File): void {
+
+    }
+    focus(): void {
+
+    }
+}

frontend/classic/js/coq-manager.ts

@@ -31,6 +31,7 @@ import { CoqIdentifier } from '../../../backend/coq-identifier';
 // Addons
 // import { CoqContextualInfo } from './contextual-info.js';
 import { CompanyCoq }  from './addon/company-coq.js';
+import { CoqMdViewEditor } from './coq-editor-mdview';
 
 /**
  * Coq Document Manager, client-side.
@@ -44,7 +45,7 @@ import { CompanyCoq }  from './addon/company-coq.js';
 export interface ManagerOptions {
     backend: backend,
     content_type: 'plain' | 'markdown',
-    frontend: 'cm5' | 'cm6' | 'pm',
+    frontend: 'cm5' | 'cm6' | 'pm' | 'mdview',
     prelaunch: boolean,
     prelude: boolean,
     debug: boolean,
@@ -158,7 +159,7 @@ class ManagerEditor {
     connect() {
 
         // Setup the Coq editor.
-        const eIdx = { 'pm': CoqProseMirror, 'cm6': CoqCodeMirror6, 'cm5': CoqCodeMirror5 };
+        const eIdx = { 'pm': CoqProseMirror, 'cm6': CoqCodeMirror6, 'cm5': CoqCodeMirror5, 'mdview': CoqMdViewEditor };
         const CoqEditor : ICoqEditorConstructor = eIdx[this.options.frontend];
 
         if (!CoqEditor)
@@ -207,7 +208,7 @@ export class CoqManager {
             content_type: 'markdown',
             prelaunch:  false,
             prelude:    true,
-            debug:      true,
+            debug:      false,
             show:       true,
             replace:    false,
             wrapper_id: 'ide-wrapper',
@@ -557,7 +558,7 @@ export class CoqManager {
         let init_opts : CoqInitOptions = {
                 implicit_libs: this.options.implicit_libs,
                 coq_options: this._parseOptions(this.options.coq || {}),
-                debug: true,
+                debug: this.options.debug,
                 lib_path: this.getLoadPath(),
                 lib_init: this.options.prelude ? [PKG_ALIASES.prelude] : []
             };
@@ -791,7 +792,7 @@ export class CoqManager {
 
         case 'editor':
             this.editor.disconnect();
-            this.editor.options.frontend = (this.editor.options.frontend === 'cm5') ? 'cm6' : 'cm5';
+            this.editor.options.frontend = (this.editor.options.frontend === 'cm5') ? 'mdview' : 'cm5';
             this.editor.connect();
             break;
         }

index.html

@@ -68,6 +68,14 @@ <h3>Welcome to the <span class="jscoq-name">jsCoq</span> Interactive Online Syst
 - Coq will recognize the code snippets as Coq
 - You will be able to save the document and link to other documents soon
 
+We can also add some random math:
+
+$$
+\sum_i a_i * b_i
+$$
+
+I *love* random math $x \cdot y \approx y \cdot x$.
+
 ```coq
 From Coq Require Import List.
 Import ListNotations.
@@ -113,12 +121,12 @@ <h3>Welcome to the <span class="jscoq-name">jsCoq</span> Interactive Online Syst
 
     var jscoq_ids  = ['coqCode'];
     var jscoq_opts = {
-        backend:   sp.get('backend'),
-        frontend:  sp.get('frontend'),
-        content_type:  sp.get('content_type'),
+        backend:   sp.get('backend') || "wa",
+        frontend:  sp.get('frontend') || "cm5",
+        content_type:  sp.get('content_type') || "markdown",
         implicit_libs: false,
         focus: false,
-        debug: true,
+        debug: false,
         editor: { mode: { 'company-coq': false } },
         init_pkgs: ['init', 'coq-base', 'coq-collections', 'coq-arith'],
         all_pkgs: ['coq', 'mathcomp']