Add Gist sharing support #330
Conversation
Signed-off-by: Elad Kinsbruner <kinsbruner@campus.technion.ac.il>
CHANGES.md
Outdated
| -------------- | ||
|
|
||
| - Add support for saving and loading scratchpad snippets using Gist (@Eladkay) | ||
|
|
||
| # jsCoq 0.17.0 |
There was a problem hiding this comment.
Actually 0.17.0 was never released so this is going to be part of 0.17.0
| description: 'jsCoq exported file', | ||
| 'public': false, | ||
| files: { | ||
| 'scratch.v': { |
There was a problem hiding this comment.
Note: we can probably use the filename from the editor if it exists (but for now scratch.v is fine).
There was a problem hiding this comment.
You can, but keep in mind that it doesn't matter for literally anything because we're just saving and loading
There was a problem hiding this comment.
In the Flèche-based branch of jsCoq, there is a notion of workspace server-side, as LSP requires.
Indeed I wonder how to map the notion of "file(s) in a Coq workspace", (where the Coq workspace is just the set of visible .vo files for Require) to the Gist namespace.
But indeed didOpen LSP call requires an URI identifier for the document, so that can be IMHO assumed to exist on the client side.
There was a problem hiding this comment.
You can, but keep in mind that it doesn't matter for literally anything because we're just saving and loading
yes this would be just for posterity so that when you load you can also "know" what the original filename was.
|
Would close #311 |
This is a merge of #328.