- Nov 10, 2020
-
-
Shachar Itzhaky authored
-
- Nov 02, 2020
-
-
Shachar Itzhaky authored
UI improvements + slight refactoring of backend commands to support detection of proof mode.
-
Shachar Itzhaky authored
-
- Oct 30, 2020
-
-
Shachar Itzhaky authored
Following SerAPI, 'Query' now handles requesting for goals and running vernac queries (`Check`, `Print`). It also handles 'Inspect', and a new query, 'Mode', is used to detect proof mode. This removes the need for the previous hack where mode is returned with Feedback(Processed) messages.
-
- Oct 20, 2020
-
-
Shachar Itzhaky authored
Coq standard library is now bundled in the `'coq'` package bundle. Fixes #210.
-
- Oct 03, 2020
-
-
Shachar Itzhaky authored
`catch { }` causes syntax error in older Node.js?
-
- Oct 02, 2020
-
-
Shachar Itzhaky authored
Does not make sense to highlight vernac statements if hitting 'Ctrl' is not going to have any effect.
-
Shachar Itzhaky authored
When statements are reported as processed, as part of the Feedback message.
-
- Oct 01, 2020
-
-
Shachar Itzhaky authored
Also, support for importing legacy `_CoqProject` definitions.
-
- Sep 30, 2020
-
-
Shachar Itzhaky authored
Because offsets returned from Coq are in bytes, whereas CodeMirror uses chars. This assumes that all strings sent to Coq are utf-8-encoded.
-
Shachar Itzhaky authored
-
- Sep 29, 2020
-
-
Shachar Itzhaky authored
As long as all of a module's dependencies have compiled successfully. (Also, some unrelated cleanup in file-view.)
-
- Sep 28, 2020
-
-
Shachar Itzhaky authored
Currently, only stores recently opened projects and files, and only applies to physical directories (when running in NW.js/Electron).
-
Shachar Itzhaky authored
-
Emilio Jesús Gallego Arias authored
[readme] mailing list -> Zulip
-
- Sep 27, 2020
-
-
Emilio Jesus Gallego Arias authored
Thanks to enjoysmath, closes #206
-
Shachar Itzhaky authored
Closes #204
-
- Sep 26, 2020
-
-
Shachar Itzhaky authored
They are no longer considered part of the statement following them. Going forward skips comments to get the next statement.
-
Shachar Itzhaky authored
This allows for the use of Vue's template compiler at build time, reducing package footprint.
-
- Sep 21, 2020
-
-
Shachar Itzhaky authored
Keyboard shortcuts are added via a CodeMirror.keyMaps entry. In literate mode (snippets), PgUp/PgDn are not bound, to allow scrolling.
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
More features and cleanup of project pane functionality.
-
Shachar Itzhaky authored
-
- Sep 19, 2020
-
-
Shachar Itzhaky authored
'Init' does not create the document anymore. The client calls both when it starts.
-
- Sep 18, 2020
-
-
Shachar Itzhaky authored
For batch compilation, compile with `Stm.VoDoc` type. Terminate worker after batch finishes up.
-
Shachar Itzhaky authored
Introduced a new command, 'Start', for use in multi-file compilation.
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
Mostly, to allow building in physical directories (in subprocess mode).
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
-
Shachar Itzhaky authored
-
- Sep 14, 2020
-
-
Shachar Itzhaky authored
In fact there was a typo in some dead code.
-
Shachar Itzhaky authored
Lib.init() resets the global env. So all the flags etc. must be set after it. Fixes #201.
-
- Sep 09, 2020
-
-
Emilio Jesús Gallego Arias authored
[travis] Don't use incorrect git submodule call
-
- Sep 08, 2020
-
-
Emilio Jesus Gallego Arias authored
This is updating not to the pinned module but to the remote, which will make CI fail. Travis should take care of the submodules already via ``` git: submodules: true ``` which IIANM is the default.
-
- Sep 07, 2020
-
-
Shachar Itzhaky authored
-
- Sep 01, 2020
-
-
Shachar Itzhaky authored
^^
-
- Aug 29, 2020
-
-
Shachar Itzhaky authored
-