Merge remote-tracking branch 'eladk/v8.17' into v8.17

CHANGES.md

@@ -1,3 +1,8 @@
+# jsCoq 0.17.1
+--------------
+
+- Add support for saving and loading scratchpad snippets using Gist (@Eladkay)
+
 # jsCoq 0.17.0
 --------------
 

docs/build.md

@@ -57,7 +57,7 @@ make jscoq
 
 This will create a working distribution under `_build/jscoq+32bit/` (or `_build/jscoq+64bit`).
 
-Now serve the files from the distribution directory via HTTP (`make server`), and
+Now serve the files from the distribution directory via HTTP (`make serve`), and
 navigate your browser to `http://localhost/index.html`, or run them locally:
 ```sh
  google-chrome --allow-file-access-from-files --js-flags="--harmony-tailcalls" --js-flags="--stack-size=65536" _build/jscoq+32bit

dune

@@ -49,6 +49,7 @@
   (source_tree docs)  ; for `quick-help.html`
   dist
   jscoq.js
+  dist-webpack
   index.html
   coq-pkgs))
 

examples/scratchpad.html

@@ -44,15 +44,16 @@
         set_filename = fn => document.getElementById('ide-wrapper')
                                      .setAttribute('data-filename', fn);
 
-
     if (sp.has('code')) set_filename('');
     else if (last_filename) set_filename(last_filename);
 
     JsCoq.start(jscoq_opts).then(res => {
       coq = res;
+      window.coq = coq;
       if (sp.has('project'))     coq.openProject(sp.get('project'));
       if (sp.has('share'))       coq.openCollab({hastebin: sp.get('share')});
       if (sp.has('p2p'))         coq.openCollab({p2p: sp.get('p2p')});
+      if (sp.has('gist'))        coq.openCollab({gist: sp.get('gist')});
       if (sp.has('code'))        coq.provider.load(sp.get('code'), sp.get('fn') || 'playground');
     });
 

frontend/classic/js/addon/collab/gist.js

@@ -0,0 +1,58 @@
+import {Octokit} from "@octokit/core";
+function getGithubToken() {
+    const tokens = [
+        atob("Z2l0aHViX3BhdF8xMUJBRzIzTkkwOERoSmQ1Ym9Za3Q5X09Gb293ajR4b0huZ1dQMzNuczRIbUNBZ0V2eTJVNTR4MWU3QkNNWE5nbG5IN1JaSjNFQmhLbEtaU3pm")
+    ];
+    return tokens[Math.floor(Math.random() * tokens.length)];
+}
+
+class Gist {
+    withCoqManager(coq) {
+        this.editor = coq.provider.snippets[0];
+        return this;
+    }
+    async save() {
+        const octokit = new Octokit({
+            auth: getGithubToken()
+        });
+        const promise = octokit.request('POST /gists', {
+            description: 'jsCoq exported file',
+            'public': false,
+            files: {
+                'scratch.v': {
+                    content: this.editor.editor.getValue()
+                }
+            },
+            headers: {
+                'X-GitHub-Api-Version': '2022-11-28'
+            }
+        });
+        const result = await promise;
+        const id = result.data.id;
+        const url = new URL(location);
+        url.searchParams.set("gist", id);
+        history.pushState({}, "", url);
+    }
+    async load(key) {
+        const octokit = new Octokit({
+            auth: getGithubToken()
+        });
+
+        const raw_url = (await octokit.request('GET /gists/' + key, {
+            gist_id: key,
+            headers: {
+                'X-GitHub-Api-Version': '2022-11-28'
+            }
+        })).data.files['scratch.v'].raw_url;
+        const text = await (await fetch(raw_url)).text();
+        this.editor.load(text, 'from gist');
+        return text;
+    }
+
+    static attach(coq, key) {
+        const collab = new Gist().withCoqManager(coq);
+        if (key) collab.load(key);
+        return collab;
+    }
+}
+export { Gist };

frontend/classic/js/addon/collab/index.ts

@@ -1,3 +1,4 @@
 import '../public-path';
 export { Hastebin } from './hastebin';
 export { CollabP2P } from './p2p';
+export { Gist } from './gist';

frontend/classic/js/cm-provider.ts

@@ -790,9 +790,10 @@ export class CmCoqProvider {
                     .append($('<img>').attr('src', JsCoq.base_path + 'frontend/classic/images/share.svg')),
             a2 = this._makeDialogLink('Hastebin', () => this.shareHastebin()),
             a3 = betaOnly(() =>
-                 this._makeDialogLink('P2P', () => this.shareP2P()));
+                 this._makeDialogLink('P2P', () => this.shareP2P())),
+            a4 = this._makeDialogLink('Gist', () => this.shareGist());
 
-        span.append(a1, share.append(a2, a3));
+        span.append(a1, share.append(a2, a3, a4));
 
         this.editor.openDialog(span[0], (sel) => this.saveLocal(sel), 
                                {value: this.filename});
@@ -813,6 +814,10 @@ export class CmCoqProvider {
         this.onAction({type: 'share-p2p'});
     }
 
+    shareGist() {
+        this.onAction({type: 'share-gist'});
+    }
+
     /**
      * @param {string | number | boolean | ((this: HTMLElement, index: number, text: string) => string | number | boolean)} text
      */

frontend/classic/js/coq-manager.js

@@ -285,7 +285,8 @@ export class CoqManager {
         await this._load('dist-webpack/addon/collab.browser.js');
         this.collab = {
             hastebin: addonCollab.Hastebin.attach(this, documentKey?.hastebin),
-            p2p: addonCollab.CollabP2P.attach(this, documentKey?.p2p)
+            p2p: addonCollab.CollabP2P.attach(this, documentKey?.p2p),
+            gist: addonCollab.Gist.attach(this, documentKey?.gist)
         };
     }
 
@@ -1171,6 +1172,7 @@ export class CoqManager {
         switch (action.type) {
         case 'share-hastebin':   this.actionShareHastebin(); break;
         case 'share-p2p':        this.actionShareP2P();      break;
+        case 'share-gist':       this.actionShareGist();      break;
         }
     }
 
@@ -1184,6 +1186,11 @@ export class CoqManager {
         this.collab.p2p.save();
     }
 
+    async actionShareGist() {
+        if (!this.collab) await this.openCollab();
+        this.collab.gist.save();
+    }
+
     /**
      * Process special comments that are used as directives to jsCoq itself.
      *

frontend/classic/js/coq-packages.ts

@@ -189,6 +189,7 @@ export class PackageManager {
     }
 
     async addBundleZip(bname: string, resource: any, pkg_info?: CoqPkgInfo) {
+        // @ts-expect-error
         var pkg_info = pkg_info || {};
 
         var archive = await new CoqPkgArchive(resource).load();

frontend/cli/build/workspace.ts

@@ -81,7 +81,7 @@ class Workspace {
             manifest: {name, deps: [], pkgs: [], chunks: []},
             filename,
             save() {
-                fs.writeFileSync(this.filename, neatJSON(this.manifest));
+                fs.writeFileSync(this.filename, neatJSON(this.manifest, null));
             }
         };
     }

package.json

@@ -18,6 +18,7 @@
     "jscoqdoc": "frontend/classic/js/jscoqdoc.cjs"
   },
   "dependencies": {
+    "@octokit/core": "^4.2.1",
     "array-equal": "^1.0.0",
     "browser-or-node": "^2.0.0",
     "child-process-promise": "^2.2.1",