| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
Indeed, one can change each item locally, but the preference menu is
only for changing the modifiers of a whole menu at once.
|
|
Otherwise, probably for the reason suspected in [1], loading the
preference file (coqiderc) is interpreted as a change of the
modifiers, and this overrides what the more fine-grained preferences
(coqide.keys) was telling.
[1] https://github.com/coq/coq/issues/8269#issuecomment-415971367
|
|
We place control attributes on their own, datatype, similarly to
regular attributes.
This is a step towards fixing #10452 , as we can now decouple control
attributes from the vernac AST itself, allowing to pass them
independently.
|
|
Ack-by: maximedenes
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
complained (fixes #10580).
|
|
Underscores are used as prefix for accelerators in gtk. In particular,
double underscores are used to escape them. So, when applying a template,
underscores should be cleaned from the inserted text.
|
|
The hang is caused by a failure in the interpretation by coqtop of the
command line option "-topfile filename" (this happens before a proper
XML communication is set up between coqtop and coqide).
The fix is a bit ad hoc. We copy in coqide the code for checking the
validity of a filename. We copy it to avoid adding a dependency in
either Names.check_valid or Stm.dirpath_of_file. We do a minimal check
(on the basename) while (if it hadn't added extra depencencies or code
duplication) it would have been more consistent to do the exact same
check as in Stm.dirpath_of_file.
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
The changes are large due to `Pervasives` deprecation:
- the `Pervasives` module has been deprecated in favor of `Stdlib`, we
have opted for introducing a few wrapping functions in `Util` and
just unqualified the rest of occurrences. We avoid the shims as in
the previous attempt.
- a bug regarding partial application have been fixed.
- some formatting functions have been deprecated, but previous
versions don't include a replacement, thus the warning has been
disabled.
We may want to clean up things a bit more, in particular
w.r.t. modules once we can move to OCaml 4.07 as the minimum required
version.
Note that there is a clash between 4.08.0 modules `Option` and `Int`
and Coq's ones. It is not clear if we should resolve that clash or
not, see PR #10469 for more discussion.
On the good side, OCaml 4.08.0 does provide a few interesting
functionalities, including nice new warnings useful for devs.
|
|
|
|
|
|
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.
|
