| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
|
|
- Update Docker images to install compatible version of lablgtk3
- We remove unnecesary variables from configure.
- We fix path detection of GTK libs in makefile
|
|
|
|
|
|
|
|
|
|
The effect of modify_base is told to be widget-dependent. It uses to
change the background with gtk2 but not with gtk3. So we use the more
explicit modify_bg.
|
|
This was automatic in gtk2 (apparently because of the specification
not being granted). This is needed with gtk3.
|
|
This was not needed in gtk2 but is needed with gtk3.
|
|
This is not mandatory for gtk+3 since it is deprecated from only gtk
3.4. This would be needed for gtk+4 though.
|
|
|
|
|
|
According to
https://developer.gnome.org/gtk2/stable/GtkToolbar.html#gtk-toolbar-set-tooltips,
tooltips are now managed globally by gtk-enable-tooltips which is true by default.
|
|
Was formerly displaying a stippled ("pointillé") light blue. Now only
a light blue.
|
|
|
|
Thanks to J. Garrigue for the hint.
|
|
Indeed, gtk3 has no more Pixmap, it should use Cairo instead.
We also deactivate the functions in the graph of dependency. In
particular, this also blocks coqOps.ml.
|
|
|
|
They rely on list and strings from configwin which themselves rely on
gtk2 only widgets.
|
