| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
Before #9263 this type was returned by the STM's `parse_sentence`, but
the type was lost on the generalization to entries.
|
|
We make `coqc` a truly standalone binary, whereas `coqtop` is
restricted to interactive use.
Thus, `coqtop -compile` will emit a warning and call `coqc`.
We have also refactored `Coqargs` into a common `Coqargs` module and a
compilation-specific module `Coqcargs`.
This solves problems related to `coqc` having its own argument
parsing, and reduces the number of strange argument combinations a
lot.
|
|
|
|
|
|
DAG nodes hold now a system state and a parsing state.
The latter is always passed to the parser.
This paves the way to decoupling the effect of commands on the parsing
state and the system state, and hence never force to interpret, say,
Notation.
Handling proof modes is now done explicitly in the STM, not by interpreting
VernacStartLemma.
Similarly Notation execution could be split in two phases in order to obtain a
parsing state without fully executing it (that requires executing all
commands before it).
Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
|
main window.
|
|
(fix #9204)
|
|
Also removing dead code about show_toolbar: this is governed by an
item of the view menu rather than by the preference panel since
aa357d601 (Dec 2003).
|
|
- deprecate the old 5-tuple accessor in favor of a view record,
- move `name` and `kind` proof data from `Proof_global` to `Proof`,
this will prove useful in subsequent functionalizations of the
interface, in particular this is what abstract, which lives in the
monads, needs in order no to access global state.
- Note that `Proof.t` and `Proof_global.t` are redundant anyways.
|
|
|
|
|
|
|
|
Improve debug output
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
Unused since b0da879dc6abfca6b4e233b7469265a5cf52ce15 (see also
followup 4f554c88aa).
|
|
In some cases, toplevel ML clients may want to modify the default set
of flags that is passed to the main initalization routine. This is for
example useful for `idetop` to suppress some undesired printing at
startup.
I would say that clients ought to have more control, but I do expect
that PRs such as #8690 will help providing a better separation thus a
mode orthogonal API.
|
|
|
|
|
|
|
|
|
|
|
|
`CoqProject_file` uses the feedback system, however this is not very
convenient in some scenarios such as `coqdep` that has to be run very
early in the build process [and thus in "boot" mode].
We thus make the warning function a paramater.
Should fix #8913.
|
|
|
|
Fix #8989.
This adds an option -topfile taking a path so that inferring the right
dirpath is done by the toplevel after processing -Q/-R instead of the
client having to do it.
|
|
Allow for new goals that don't map to old goals
Include background_goals in all_goals return value
Fix incorrect change to raw diffs in shorten_diff_span
Fixes #8922
|
|
This is to ensure that the corresponding question boxes remains in
front of the main window, consistently with the fact that they are
blocking actions on the main window.
|
|
The "parent" option allows to attach the box to the parent box. This
ensures that the dialog box, which blocks action on the main window,
does not get hidden by the main window.
Idem for the message_box.
|
|
We do it by passing the name of the main window in the "parent"
option. Formerly, the window could be hidden but nevertheless blocking
any action on the main window. With the change, it can be moved
aside, but never hidden by the main window.
Tested on MacOS X.
|
|
This was obsolete since new completion in 945d7db9 (then a07359f6).
|
|
First, they already work by default. Second, by rebinding them, they
cannot be used any longer in the completion menu, which is a bit
annoying.
|
|
We should install the files in `share/coqide` instead of the current
`coq` location; but we defer this change until we are more advanced in
the make-phase out.
Fixes: #8953
|
|
This is a bit more portable.
|
|
|
|
gtk_scrolled_window_add_with_viewport)
|
|
When opening the query pane, do not try to focus on a query tab that no
longer exists.
|
|
Gtk complains that we are not using gtk_scrolled_window_add_with_viewport,
so let us do.
|
|
- `CString.strip -> String.trim`
- `CString.split -> String.split_on_char`
As noted by @ppedrot there are some small differences on semantics:
> OCaml's `trim` also takes line feeds (LF) into account. Similarly,
> OCaml's `split` never returns an empty list whereas Coq's `split`
> does on the empty string.
|
|
Lintian found some spelling errors in the Debian packaging for coq. Fix
them most places they appear in the current source. (Don't change
documentation anchor names, as that would invalidate external
deeplinks.)
This also fixes a bug in coqdoc: prior to this commit, coqdoc would
highlight `instanciate` but not `instantiate`.
|
|
|
|
Even if `fake_ide` was under tools, it depended on libraries from
`ide`. Thus, we move `fake_ide` to `ide`, and make it "private" to the
test-suite [this means `test-suite` depends on the `ide` folder then].
In the Dune side, we reorganize libraries so `fake_ide` doesn't depend
on GTK anymore, this allows to run the test-suite when GTK is not
available.
In order to achieve this, we had to split the `coqide` package in a
server and client version.
|
|
After some discussion upstream, I think that for the current a
multi-package setup in a single repository this setup saves a bit
work.
The most problematic bit is the `-rectypes` flag; its status is not
saved per-library so we must either duplicate the flags in the coqide
scope (scope == dune-project file), or unify its scope with Coq. We do
this last option as this seems like the easiest thing for now.
Changes:
- Move coqide.opam file to the root, use a single scope/`dune-project` file.
- Remove `dune-workspace`, this should be owned by the developer / user.
|
|
The Dune `release` profile is used by OPAM so that should cover the
testing.
We also update the dependencies:
- camlp5: 7.01 had some bugs regarding grammar; we could use 7.02,
however this version it is not in OPAM. So I guess that leaves us
with 7.03 again.
- lablgtk < 2.18.5 does not support OCaml >= 4.05.0.
|
|
|
|
These are unused and not likely to come back.
|
|
|
|
As noted by @anton-trunov, this is more useful for development and
debug.
|
|
info
|
