| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
Fixes #3907: CoqIDE File->Revert all buffers does not work.
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
|
|
|
|
|
|
As suggested by Pierre-Marie Pédrot, this is a more conservative
version of #8771 .
In this commit, we replace Coq's custom backtrace type with OCaml
`Printexc.raw_backtrace`; this seems to already give some improvements
in terms of backtraces [see below] and removes quite a bit of code.
Main difference in terms of API is that backtraces become now
first-class in `Exninfo`, and we seek to consolidate thus the
exception-related APIs in that module.
We also fix a bug in `vernac.ml` where the backtrace captured was the
one of `edit_at`.
Closes #6446
Example with backtrace from https://github.com/coq/coq/issues/11366
Old:
```
raise @ file "stdlib.ml", line 33, characters 17-33
frame @ file "pretyping/coercion.ml", line 406, characters 24-68
frame @ file "list.ml", line 117, characters 24-34
frame @ file "pretyping/coercion.ml", line 393, characters 4-1004
frame @ file "pretyping/coercion.ml", line 450, characters 12-40
raise @ unknown
frame @ file "pretyping/coercion.ml", line 464, characters 6-46
raise @ unknown
frame @ file "pretyping/pretyping.ml", line 839, characters 33-95
frame @ file "pretyping/pretyping.ml", line 875, characters 50-94
frame @ file "pretyping/pretyping.ml", line 1280, characters 2-81
frame @ file "pretyping/pretyping.ml", line 1342, characters 20-71
frame @ file "vernac/vernacentries.ml", line 1579, characters 17-48
frame @ file "vernac/vernacentries.ml", line 2215, characters 8-49
frame @ file "vernac/vernacinterp.ml", line 45, characters 4-13
...
```
New:
```
Raised at file "stdlib.ml", line 33, characters 17-33
Called from file "pretyping/coercion.ml", line 406, characters 24-68
Called from file "list.ml", line 117, characters 24-34
Called from file "pretyping/coercion.ml", line 393, characters 4-1004
Called from file "pretyping/coercion.ml", line 450, characters 12-40
Called from file "pretyping/coercion.ml", line 464, characters 6-46
Called from file "pretyping/pretyping.ml", line 839, characters 33-95
Called from file "pretyping/pretyping.ml", line 875, characters 50-94
Called from file "pretyping/pretyping.ml" (inlined), line 1280, characters 2-81
Called from file "pretyping/pretyping.ml", line 1294, characters 21-94
Called from file "pretyping/pretyping.ml", line 1342, characters 20-71
Called from file "vernac/vernacentries.ml", line 1579, characters 17-48
Called from file "vernac/vernacentries.ml", line 2215, characters 8-49
Called from file "vernac/vernacinterp.ml", line 45, characters 4-13
...
```
|
|
dune-dbg depends on coqchk.bc and coqide_main.bc, and apparently they
now need explicit modes to be produced.
|
|
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
|
|
This is the minimal set of changes requires for Coq to build under 2.0
mode. We may likely take advantage of some more new features.
Note that Dune 2.0 requires OCaml >= 4.06.0, OPAM allows to use Dune
in older versions as it will install a secondary compiler.
|
|
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
```
|
|
size. (Fixes #10956)
Reviewed-by: ppedrot
|
|
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.
|
|
The bug was introduced by #10063, which eagerly added dots to identifier
without considering whether they are related to the identifier. Along the
way, this commit also prevents primes and digits from being added as
initial characters of identifiers. This works for both word selection and
queries.
Note that there is still a small issue with word selection, when the
current word starts with a digit. Indeed, when double-clicking, GTK will
already have extended the selection to it, so we have no way of preventing
the digit from being part of the selection.
This commit also fixes the unusual calling convention of
Gtk_parsing.end_words.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
They probably don't need to be executable
|
|
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.)
|
|
|
|
|
|
|
|
This concerns zooming, undoing, displaying preferences.
|
|
|
|
|
|
|
|
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
|
