| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Incidentally fix some missing newline in coqc help, and give proper
help for coqidetop and the "coq*worker"s.
|
|
- Binding coqc execution to the generic support for Coq binaries
(i.e. to start_coq).
- Moving init_toploop to the init part of coq executables so that coqc
can avoid to call it. By the way, it is unclear what workerloop
should do with it. Also, it is unclear how much the -l option should
be considered an coqidetop or coq*worker option. In any case, it
should be disallowed in coqc, I guess?
- Moving the custom init part at the end of the initialization
phase. Seems ok, despites the few involved side effects.
|
|
We lose track of it at some time in "known_state" and assume that the
reference cur_opt has not been modified in between the time it was set
(in "new_doc") and "known_state".
|
|
In particular, method init does not do parsing any more.
This allows for instance to let coqidetop treats itself the
"-filteropts" option.
|
|
|
|
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: ppedrot
|
|
This reverts commit 6d0083bb07528d7cd7ad2f8815d06a4e41deb16c.
|
|
These were found with the following command:
$ git grep "1999-" | grep -v "2019"
|
|
|
|
Reviewed-by: ppedrot
|
|
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
The main idea of this PR is to distinguish the types of "proof object"
`Proof_global.t` and the type of "proof object associated to a
constant, the new `Lemmas.t`.
This way, we can move the terminator setup to the higher layer in
`vernac`, which is the one that really knows about constants, paving
the way for further simplification and in particular for a unified
handling of constant saving by removal of the control inversion here.
Terminators are now internal to `Lemmas`, as it is the only part of
the code applying them.
As a consequence, proof nesting is now handled by `Lemmas`, and
`Proof_global.t` is just a single `Proof.t` plus some environmental
meta-data.
We are also enable considerable simplification in a future PR, as this
patch makes `Proof.t` and `Proof_global.t` essentially the same, so we
should expect to handle them under a unified interface.
|
|
|
|
|
|
Typically instead of [start_proof : ontop:Proof_global.t option -> bla ->
Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and
the pstate is pushed on the stack by a caller around the
vernacentries/mlg level.
Naming can be a bit awkward, hopefully it can be improved (maybe in a
followup PR).
We can see some patterns appear waiting for nicer combinators, eg in
mlg we often only want to work with the current proof, not the stack.
Behaviour should be similar modulo bugs, let's see what CI says.
|
|
|
|
|
|
than files.
|
|
+ adding a go-to-end binding + improving documentation
Reviewed-by: gares
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
Fixes coq/coq#10062.
The implementation is rough, and does not deal with leading,
trailing, or doubled periods, but the same can be said of the current
handling of leading numbers or primes.
|
|
This is to be consistent with what the preference panel displays (namely μpG).
We keep the nanoPG name in the preference file by compatibility.
|
|
On MacOS X: Ctrl-Cmd-Left and Ctrl-Cmd-Right
Elsewhere: Meta-Left and Meta-Right
See issue #9899 (moving cursor to beginning and end of file).
|
|
More precisely, GTK+ uses Pango rules which follows the standard Unicode
text segmentation rules (see http://www.unicode.org/reports/tr29/).
|
|
|
|
In practice, most of Alt modified keys are used on MacOS X keyboards
for special characters and many Command modified keys are used for
MacOS standard actions.
So, we propose to use Ctrl-Command- as a prefix for the Meta-based
nano-PG shortcuts. E.g. Ctrl-Command-e would go the end of the
sentence.
|
|
Not only will this be clearer but it prepares to describing action on
MacOS which shall use Cmd and which cannot be abbreviated w/o
introducing a confusion with the abbreviation C- of Control-.
|
|
For instance, Ctrl-Meta-e was behaving like Ctrl-e.
|
|
Reviewed-by: CohenCyril
Ack-by: Zimmi48
Ack-by: erikmd
Ack-by: gares
Ack-by: jfehrle
|
|
not to be used.
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: maximedenes
|
|
There is no more uses of "old style preferences" but the comment was
still there.
|
|
This avoids the modifiers keys to overwrite changes made in
coqide.keys.
|
|
This has been a mess for quite a while, we try to improve it.
|
|
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
|
|
Not sure if the idetop.set_options was correctly changed, ocaml types
pass at least.
|
|
We alert users that `Vernacstate.Proof_global` is a Coq internal
module and should not be used to workaround lack of state threading.
|
|
Unfortunately, the only sane fix I was able to hack was to deactivate
the possibility to change the background colour altogether. Trying to
do otherwise is a real Pandora's box which is ultimately triggered by
the lack of lablgtk3 bindings for the GtkStyleContext class.
I tried a lot of alternative approaches, to no avail. This includes
catching the selection signal, reimplementing selection by hand in
GtkTextView, and even reading the internal details of the GTK
implementation turned not that helpful.
For the time being (8.10 beta) I think we do not have much choice.
|
|
This is necessary to prevent Coq from sending ill-formed output in some
scenarios involving `Timeout`.
Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
Ack-by: charguer
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
