| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This library is unstable and not meant to be consumed by anyone. We
thus make it private.
|
|
Ack-by: JasonGross
Reviewed-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
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.
|
