| Age | Commit message (Collapse) | Author |
|---|
|
This hopefully fix the segfaults we observe with completion.
|
|
Reviewed-by: ppedrot
|
|
It was previously only applied to the script buffer.
|
|
|
|
We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]
Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.
|
|
The iterator of the completion context does not seem trustable.
|
|
Let's see if it fixes #11943. See there for explanations about the
related segfault.
|
|
parsing of coqtop arguments in coqide
Reviewed-by: ejgallego
|
|
The completion proposals need to be ordered by length first for usability.
I aknowledge that it's too easy to mess up when refactoring, but here there was
a clear comment that this change should not have been performed.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Ack-by: ppedrot
|
|
|
|
Reviewed-by: ppedrot
|
|
Add headers to a few files which were missing them.
|
|
This is at least to be able to use spaces in file names (#11595).
In practice it protects also \, ', ", and many other symbols.
|
|
This encodes/decodes a list of string into a string in a way
compatible with shell interpretation. On the contrary of
Filename.quote which is for computer consumption, it introduces quotes
for human consumption.
The strategy is to split each string into substrings separated by
simple quotes. Each substring is surrounted by single quotes if it
contains a space. Otherwise, each backslash in the substring is
doubled. The substrings are concatenated separated by
backslash-protected single quote. The strings are then concatenated
separated with spaces. The decoding is shell-like in the sense that it
follows the rules of single quote, backslash and space.
|
|
|
|
This behaviour happens as a sub-bug of #10169 for instance.
|
|
Reviewed-by: Matafou
Reviewed-by: ppedrot
|
|
This PR refactors the handling of ML loadpaths to get it closer to
what (as of 2020) the standard OCaml toolchain (ocamlfind, dune) does.
This is motivated as I am leaning toward letting the standard OCaml
machinery handle OCaml includes; this has several benefits [for
example plugins become regular OCaml libs] It will also help in
improving dependency handling in plugin dynload.
The main change is that "recursive" ML loadpaths are no longer
supported, so Coq's `-I` option becomes closer to OCaml's semantics.
We still allow `-Q` to extend the OCaml path recursively, but this may
become deprecated in the future if we decide to install the ML parts
of plugins in the standard OCaml location.
Due to this `Loadpath` still hooks into `Mltop`, but other than that
`.v` location handling is actually very close to become fully
independent of Coq [thus it can be used in other tools such coqdep,
the build system, etc...]
In terms of vernaculars the changes are:
- The `Add Rec ML Path` command has been removed,
- The `Add Loadpath "foo".` has been removed. We now require that the
form with the explicit prefix `Add Loadpath "foo" as Prefix.` is used.
We did modify `fake_ide` as not to add a directory with the empty
`Prefix`, which was not used. This exposed some bugs in the
implementation of the document model, which relied on having an
initial sentence; we have workarounded them just by adding a dummy one
in the two relevant cases.
|
|
The current CoqIDE bindings include an invisible U+FE00 variation selector
immediately following a number of symbols. For example, \empty maps to
U+2205 U+FE00 (UTF-8 encoding E2 88 85 EF B8 80), where U+2205 is the
expected Unicode point for "EMPTY SET".
This variation selector is difficult to work with in CoqIDE. If some
notation is defined to expect a U+2205 symbol, then a U+2205 U+FE00
expression does not match that notation, even though it is visually
identical. As a concrete example, this makes it difficult to use CoqIDE
to type the U+2205 EMPTY SET symbol for use with Iris, which expects a
U+2205 without a U+FE00. Pressing "backspace" at the right point deletes
the U+FE00 variation selector, even though visually nothing appears to
happen, which is also confusing.
This commit removes the U+FE00 invisible variation selectors from any
symbols in the default bindings for CoqIDE (it appeared in 35 symbols
out of 1400+ symbols; I have no theory for why those 35 symbols were
special in this way). This change was generated using:
sed -e s,$(printf '\xef\xb8\x80'),,
|
|
We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.
At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.
|
|
Compile buffer, and with building from a path containing spaces.
Updated CHANGES.md
Now using Filename.quote instead of enclosing in single quotes.
Fixed rebasing problems.
|
|
Reviewed-by: ejgallego
|
|
This was redundant with `iraise`; exceptions in the logic monad now
are forced to attach `info` to `Proofview.NonLogical.raise`
|
|
|
|
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
Ack-by: Zimmi48
Reviewed-by: herbelin
|
|
Reviewed-by: ppedrot
|
|
Fixes #3907: CoqIDE File->Revert all buffers does not work.
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
Partial fix of #11219: CoqIDE tactics and templates menus are out of sync.
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.
|
