| Age | Commit message (Collapse) | Author |
|---|
|
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
|
|
Add headers to a few files which were missing them.
|
|
Partial fix of #11219: CoqIDE tactics and templates menus are out of sync.
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
|
|
|
|
|
|
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
|
|
complained (fixes #10580).
|
|
|
|
This is to be consistent with what the preference panel displays (namely μpG).
We keep the nanoPG name in the preference file by compatibility.
|
|
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.
|
|
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.
|
|
Reviewed-by: Zimmi48
Ack-by: charguer
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
This is not mandatory for gtk+3 since it is deprecated from only gtk
3.4. This would be needed for gtk+4 though.
|
|
|
|
Thanks to J. Garrigue for the hint.
|
|
They rely on list and strings from configwin which themselves rely on
gtk2 only widgets.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Ack-by: JasonGross
Reviewed-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
|
|
|
|
|
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).
|
|
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.
|
|
- `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.
|
|
|
|
|
|
2) Changing the diff setting from the menu should reprint the proof.
3) Generate a warning message if the user enters a "Set Diffs xx" command.
4) Tweak display names for diffs in View menu.
|
|
Proof General requires minor changes to make the diffs visible, but this code
shouldn't break the existing version of PG.
Diffs are computed for the hypotheses and conclusion of the first goal between
the old and new proofs. Strings are split into tokens using the Coq lexer,
then the list of tokens are diffed using the Myers algorithm. A fixup routine
(Pp_diff.shorten_diff_span) shortens the span of the diff result in some cases.
Diffs can be enabled with the Coq commmand "Set Diffs on|off|removed." or
"-diffs on|off|removed" on the OS command line. The "on" option shows only the
new item with added text, while "removed" shows each modified item twice--once
with the old value showing removed text and once with the new value showing
added text.
The highlights use 4 tags to specify the color and underline/strikeout.
These are "diffs.added", "diffs.removed", "diffs.added.bg" and "diffs.removed.bg".
The first two are for added or removed text; the last two are for
unmodified parts of a modified item.
Diffs that span multiple strings in the Pp are tagged with "start.diff.*" and
"end.diff.*", but only on the first and last strings of the span.
|
|
|
|
|
|
|
|
This fixes bug #5380 in particular.
More generally, tags were not updated to the correct default value
if the corresponding line in the configuration file was missing.
|
|
|
|
more uniform
|
|
This allows to share the test for possible relocalisation done in envars.ml.
|
|
Deprecations which can't be fixed in 4.02.3 are locally wrapped with
[@@@ocaml.warning "-3"]. The only ones encountered are
- capitalize to capitalize_ascii and variants. Changing to ascii would
break coqdoc -latin1 and maybe other things though.
- external "noalloc" to external [@@noalloc]
|
|
|
|
|
|
|
