| Age | Commit message (Collapse) | Author |
|---|
|
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]
|
|
|
|
|
|
|
|
|
|
This allows a smoother transition between various versions of CoqIDE, by
not erasing options which are unknown at the present time.
|
|
Fixes both bugs #4924 and #4437.
|
|
This appends the currently selected word to the query. Only queries
that end with this are supported, "..." inside the query will just
not work.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
2.14. Debian ships with lablgtk 2.16 only since a few months, so we apply the
fix to trunk instead.
This reverts commits:
490160d25d3caac1d2ea5beebbbebc959b1b3832.
ef8718a7fd3bcd960d954093d8c636525e6cc492.
6f9cc3aca5bb0e5684268a7283796a9272ed5f9d.
901a9b29adf507370732aeafbfea6718c1842f1b.
|
|
|
|
|
|
|
|
On most systems (including Windows, according to the bug report), shortcuts
Ctrl+Alt+Arrows are preempted by the window manager by default. So don't
use them for navigation in Coqide by default. Note that this change only
has an impact when installing on a fresh system; it won't change anything
for existing users.
|
|
|
|
|
|
|
|
|
|
|
|
There is no remaining hook in the preferences. In particular, the
refresh_editor_hook is gone.
|
|
There is no remaining global preference record anymore, every preference
is now defined in the new event-based style.
|
|
A lot of legacy code has been removed in the process in favour of
signal-based interactions.
|
|
We use uniform functions instead of code duplication.
Likewise, we disentangle the hook mechanisms by using
callbacks connected to preferences instead.
Only the easy hook bits were removed. The most awing one,
the editor refreshing hook, is still alive.
|
|
Some old style references remain because all type converters are not
implemented yet.
|
|
We use a class-based system instead of the old record-based system. This
allows for more uniformity and the possibility to define complex
interactions with preferences based on GTK signals. This will allow to
simplify some architectural choices.
|
|
Implement wish #3582.
|
|
Fixes bug #2762.
|
