| Age | Commit message (Collapse) | Author |
|---|
|
Just like the [Record] keyword allows only non-recursive records.
|
|
|
|
|
|
This revert somehow f5d7b2b1eda550f5bf0965286d449112acbbadde about "Hypotheses
don't respect Barendregt convention".
|
|
It's possible that I should have removed more "allows", as many
instances of "foo allows to bar" could have been replaced by "foo bars"
(e.g., "[Qed] allows to check and save a complete proof term" could be
"[Qed] checks and saves a complete proof term"), but not always (e.g.,
"the optional argument allows to ignore universe polymorphism" should
not be "the optional argument ignores universe polymorphism" but "the
optional argument allows the caller to instruct Coq to ignore universe
polymorphism" or something similar).
|
|
|
|
Sort of fixes bug #2765, but the file loading is broken and puts coqtop in
an inconsistent state, so that even the previous half-working patch was
actually not functionning at all. This should be fixed eventually.
|
|
died" when coqtop or coqtopide.cmxs are in inconsistent state.
|
|
|
|
|
|
reports errors also from stderr.
|
|
|
|
|
|
including bigger icons
|
|
|
|
|
|
The created bundle contains only coqide and gtk (no coqtop, no stdlib)
|
|
|
|
|
|
coqide --help.
|
|
|
|
|
|
lib/interface split into:
- lib/feedback
subscribe-based feedback bus (also used by coqidetop)
- ide/interface
definition of coqide protocol messages
lib/pp
structured info/err/warn messages
lib/serialize split into:
- lib/serialize
generic xml serialization (list, pairs, int, loc, ...)
used by coqide but potentially useful to other interfaces
- ide/xmlprotocol
serialization of protocol messages as in ide/interface
the only drawback is that coqidetop needs -thread
and I had to pass that option to all files in ide/
|
|
The fix is only partial, because dropping files only works over the menu
bar, the icon bar, the status bar, and so on. Editable boxes, such as the
script widget, catch dnd events, hence preventing this code from working
for these drop targets. Some (labl)gtk expert should be able to sort it
out.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
I added a .merlin in ide/ who inherits everything from the root .merlin and also
adds the dependency to lablgtk, which I removed from the root file. These way
people not working on that part of the code won't get bothered if they don't
have that package.
I removed the S/B entry for plugins which was useless, indeed there is no ML
file in that directory and merlin doesn't scan the subdirectories recursively
(as you know).
I also removed the S/B entry for checker since most of the files of this
directory are also present in kernel and that was the cause of a lot errors on
merlin's side (think "inconsistent assumptions").
On top of that, no part of the tree depends on checker (I back that assertion by
a grep of the *.d files of the tree) so these lines in the .merlin were actually
useless. The only part of the tree where you need to know what's in checker/ is
when you are working in checker/ itself, but since merlin automatically adds the
directory of the file under edition in its source and load paths nothing else is
needed.
There might still be problems after this patch, but they should be less of them.
Considering my poor knowledge of the codebase there might be other conflicts I
have missed.
|
|
|
|
|
|
Stm used to delegate every proof when it was possible, but this may
be a bad idea. Small proofs may take less time than the overhead
delegation implies (marshalling, etc...).
Now it delegates only proofs that take >= 1 second.
By default a proof takes 1 second (that may be wrong).
If the file was compiled before, it reuses the data stored in the .aux
file and assumes the timings are still valid.
After a proof is checked, Coq knows how long it takes for real, so it
wont predict it wrong again (when the user goes up and down in the
file for example).
CoqIDE now sends to Coq, as part of the init message, the file name
so that Coq can load the .aux file.
|
|
|
|
|
|
|
|
With ocaml 4.01, the 'unused open' warning also checks the mli :-)
Beware: some open are reported as useless when compiling with camlp5,
but are necessary for compatibility with camlp4. These open are now
marked with a comment.
|
|
|
|
|
|
|
|
|
|
|
|
When the worker fails, the master may need to recompute some states
the worker has already validates. In this case they are colored
accordingly.
|
|
Like the socket for the OCaml debugger
|
|
|
|
|
|
It is not possible to add shortcuts with arbitrary modifiers and to
save into a state some data, like the line offset for C-n and the
killed text for C-k and C-y.
If you see that your favorite Emacs/PG shortcut is missing,
please tell me!
Currently supported shortcuts:
C-_ Undo
C-g Esc
C-s Search
C-e Move to end of line
M-e Move to end of sentence
M-a Move to beginning of sentence
C-n Move to next line
C-p Move to previous line
C-f Forward char
C-b Backward char
M-f Forward word
M-b Backward word
C-k Kill untill the end of line
M-d Kill next word
M-k Kill until sentence end
M-DELBACK Kill word before cursor
C-d Delete next character
C-y Yank killed text back
C-c C-RET Go to
C-c C-n Advance 1 sentence
C-c C-u Retract 1 sentence
C-c C-b Advance
C-c C-r Restart
C-c C-c Stop
C-c C-a C-p Print
C-c C-a C-c Check
C-c C-a C-b About
C-c C-a C-a Search About
C-c C-a C-o Search Pattern
C-c C-a C-l Locate
C-c C-a C-RET match template
C-x C-s Save
C-x C-c Quit
C-x C-f Open
|
