| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
The error message was not only causing coqtop to exit, but also coqide to
crash, which led to a rather poor user experience. Since the code does not
actually care about the file extension, this commit just removes the test.
|
| | |
|
| |
|
|
| |
This brings a 10x speedup for going at the end of large .v files.
|
| |
|
|
|
|
|
| |
A "sentence" includes all the blank lines and all the comments that
precede a command. So its starting location might be far from any error it
contains. This patch changes error reporting so that it relies on the
location of errors rather than the location of erroneous sentences.
|
| |
|
|
|
|
|
|
|
|
| |
Commit 1774a87 increased the file to 1024x1024. This had two adverse
consequences. First, the icon was too large to be used as a window icon
("gdk_window_set_icon_list: icons too large"), so Coqide 8.5 no longer had
an icon at runtime. Second, the file was also used in the About message
box, which was thus exceeding the display size of any reasonably-priced
device. This commit reverts the file to a saner size (still larger than
the original 66x100 picture).
|
| |
|
|
|
|
| |
Rather than being isolated words, commands and tactics now extend till
dot separators. So bullets can be defined as living only at the top level
of proofs, which should make their detection much more robust.
|
| |
|
|
|
|
|
|
|
|
| |
We force the STM to finish after the initialization request so as to raise
exceptions that may have been generated by the initialization process. Likewise,
we simply die when the initialization request fails in CoqIDE instead of just
printing an error message.
This is the fix for the underlying issue of bug #4591, but it does not solve
the bug yet.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
bug #4477)
The bug was a bit subtle. Function process_cmd_line can be called in three
different ways:
1. tail-recursively to accumulate parsed options in reverse order,
2. directly to parse a file (coqide) or a command line (coq_makefile),
3. recursively to handle a "-f" option.
Once its execution finished, the function reversed its accumulator so
that the parsed options are in correct order. Due to the third case, this
means that the final local order of options was depending on the parity of
the depth of "-f" options. This commit fixes it by changing the function so
that the recursive call gets the actual accumulator rather than its
reversed version.
Warning: this will break all the projects that were inadvertently (or not)
relying on the bug. This might also require a further commit if
coq_makefile itself was relying on the bug.
|
| |
|
|
|
| |
Force failing when reaching end of file with unterminated comment when
parsing Make (project) file.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
| |
2.14. Debian ships with lablgtk 2.16 only since a few months, so we apply the
fix to trunk instead.
This reverts commits:
490160d25d3caac1d2ea5beebbbebc959b1b3832.
ef8718a7fd3bcd960d954093d8c636525e6cc492.
6f9cc3aca5bb0e5684268a7283796a9272ed5f9d.
901a9b29adf507370732aeafbfea6718c1842f1b.
|
| | |
|
| | |
|
| |
|
|
|
| |
These options can be set to a string value, but also unset.
Internal data is of type string option.
|
| |
|
|
|
|
|
|
| |
On most systems (including Windows, according to the bug report), shortcuts
Ctrl+Alt+Arrows are preempted by the window manager by default. So don't
use them for navigation in Coqide by default. Note that this change only
has an impact when installing on a fresh system; it won't change anything
for existing users.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Sorry so much.
Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
|
| |
|
|
| |
parsing Make (project) file.
|
| |
|
|
|
|
|
|
| |
File system.ml seemed like a better choice than util.ml for sharing the
code, but it was bringing a bunch of useless dependencies to the IDE.
There are presumably several other tools that would benefit from using
open_utf8_file_in instead of open_in, e.g. coqdoc.
|
| | |
|
| | |
|
| |
|
|
| |
Correct folding order over the named_list_context.
|
| | |
|
| |
|
|
|
| |
Ideally, the code should be shared between the various toplevels, but this
is a lot more work than just fixing a few strings.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
This grants wish #4194.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
- Arithmetic operators and brackets are no longer recognized as bullets,
unless they follow a stop or start a line.
- Most vernacular commands are no longer highlighted when used inside
proof scripts.
- Coqdoc comments now take precedence over regular comments.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This patch allows Coq terms to be extracted into the widely used JSON
format. This is useful in at least two cases:
- One might want to manipulate Coq values outside of Coq, but without
being forced to use one of the three existing extraction languages
(OCaml, Haskell, or Scheme), and without having to compile Coq's
extracted result. This is especially useful when a Coq evaluation
produces some data structure that needs to be moved out of Coq.
Having to invoke an OCaml/Haskell/Scheme compiler just to get a
data structure out of Coq is somewhat awkward.
- One might want to experiment with extracting Coq code into other
languages (Go, Javascript, etc), without having to write the whole
extraction logic in OCaml and recompile Coq's extraction plugin
each time. This makes it easy to quickly prototype extraction
in any language, without having to build Coq from source.
Extraction to JSON is implemented by adding the JSON "pseudo-language"
to the extraction facility. Thus, one can extract the JSON encoding
of a single term using:
Extraction Language JSON.
Extraction qualid.
and extract an entire Coq library "ident" into "ident.json" using:
Extraction Language JSON.
Extraction Library ident.
Nota (Pierre Letouzey) : this is an updated version of the original
PullRequest, updated to match recent changes in trunk
|
| |
|
|
|
|
|
|
|
|
| |
The old behavior was extremely annoying, especially when using coqide from
the command line, since the "open" box would then point to a seemingly
random point of the filesystem rather than to the directory of the files
currently being edited (since they were passed on the command line rather
than by point-and-click).
The new behavior matches the one of mainstream editors, e.g. emacs, gedit.
|
| |
|
|
|
|
|
|
|
|
|
| |
No "read-only" terminator. If no terminator is present the UI
complains. If the terminator is different, STM warns but
continues. The STM warns that the "check the document" button
will not honor the terminator change, and what to do to avoid
that.
Technically, one cannot turn (a posteriori) an axiom into a theorem
and vice versa. Could be done, but not with a small patch.
|
| | |
|
| |
|
|
| |
Admitted (like Qed) can be "partially executed", but is also unsafe.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
Guillaume Melquiond
Lionel Rieg
Pierre-Marie Pédrot
Enrico Tassi
Maxime Dénès
Hugo Herbelin
Matthieu Sozeau
Nickolai Zeldovich