| Age | Commit message (Collapse) | Author |
|---|
|
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
|
|
This hopefully fix the segfaults we observe with completion.
|
|
Add headers to a few files which were missing them.
|
|
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
```
|
|
This should fix the issue when creating new session panes. The initial
session panes, however, might still be wrongly sized, as we do not yet
know, at the time they are created, if the window manager will respect the
user settings fixing the window size.
|
|
G. Melquiond noticed that the size_allocate event is emitted in the
Layout step of the Events-Update-Layout-Paint gtk+ loop so that it is
actually processed only when a further event arrived. In some
circonstances, this next event has to be an action from the user. So,
in some circonstances, at initialization of Coqide, the handle, whose
positioning was precisely governed by the size_allocate event, was
only set at its expected position after a first action of the
user. Before this first action of the user, the handle separating the
buffer and the pair of goal and message windows, as well as the handle
separating the goal window and the message window were located in the
leftmost uppermost corner, which gave an impression of non-usability
of CoqIDE.
To prevent this, we early set the position of the handle at an
estimated value depending on the width and height of the whole coqide
windows in the preferences.
(Also removing a previous temporary setting of the handle position to
- strangely - value 1 but this was anyway overwritten by the
size_allocate event.)
|
|
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.
|
|
|
|
|
|
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.
|
|
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 is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
We systematically use Wg_MessageView for both the message panel and each
Query tab; we register all MessageView in a RoutedMessageViews where the
default route (0) is the message panel. Queries from the Query panel pick
a non zero route to have their feedback message delivered to their MessageView
|
|
|
|
|
|
|
|
|
|
We again remove another user of Stateid.dummy. However, we need to
adapt the protocol so `Coq.query` takes the `route_id` and we can
redirect the output properly to the subwindow.
|
|
When inserting a character in an already processed buffer, a message is
sent to Coq so that the proof is backtracked and the character is
inserted. If a second character is inserted while Coq is still busy with
the first message, the action is canceled, but the signal is no longer
dropped so that the second character is properly inserted.
|
|
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
|
|
|
|
|
|
|
|
|
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.
|
|
Some old style references remain because all type converters are not
implemented yet.
|
|
|
|
|
|
This grants wish #4194.
|
|
No "read-only" terminator. If no terminator is present the UI
complains. If the terminator is different, STM warns but
continues. The STM warns that the "check the document" button
will not honor the terminator change, and what to do to avoid
that.
Technically, one cannot turn (a posteriori) an axiom into a theorem
and vice versa. Could be done, but not with a small patch.
|
|
|
|
Instead of setting the last modified part of the text to be the insert point,
we register all modifications to the buffer between to user actions and take
the last modified point to be the least offset of all those modifications.
|
|
We make the deletion callback not to regenerate a task id, as the insertion
callback does. I can't find a particular reason for this dissymetry, and it
was indeed causing trouble.
|
|
Also fixes bug #4030.
|
|
|
|
This allows a nifty display of the current state of the document through
a dedicated progress bar.
Also closes bug #3764.
|
|
|
|
This way a user *can* use coqide with -debug
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This should fix Arnaud's bug (reported by private email) that makes
coq eat two sentences at once (and process only the first one).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16907 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It uses Str, hence it also supports captures \(..\) and \1 .. \n
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16904 85f007b7-540e-0410-9357-904b9bb8a0f7
|
