| Age | Commit message (Collapse) | Author |
|---|
|
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
|
|
The parsing rules defining classes of lexemes in language
configuration expect a Coq document and are not relevant in the
message and proof window. Thus backtracking on this part of #12169.
Keeping the highlighting style though.
|
|
It was previously only applied to the script buffer.
|
|
parsing of coqtop arguments in coqide
Reviewed-by: ejgallego
|
|
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 behaviour happens as a sub-bug of #10169 for instance.
|
|
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.
|
|
|
|
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
...
```
|
|
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.
|
|
|
|
This concerns zooming, undoing, displaying preferences.
|
|
|
|
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.
|
|
|
|
This is to be consistent with what the preference panel displays (namely μpG).
We keep the nanoPG name in the preference file by compatibility.
|
|
Reviewed-by: Zimmi48
Ack-by: charguer
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
According to
https://developer.gnome.org/gtk2/stable/GtkToolbar.html#gtk-toolbar-set-tooltips,
tooltips are now managed globally by gtk-enable-tooltips which is true by default.
|
|
Was formerly displaying a stippled ("pointillé") light blue. Now only
a light blue.
|
|
|
|
Thanks to J. Garrigue for the hint.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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 :)
|
|
|
|
|
|
`CoqProject_file` uses the feedback system, however this is not very
convenient in some scenarios such as `coqdep` that has to be run very
early in the build process [and thus in "boot" mode].
We thus make the warning function a paramater.
Should fix #8913.
|
|
Fix #8989.
This adds an option -topfile taking a path so that inferring the right
dirpath is done by the toplevel after processing -Q/-R instead of the
client having to do it.
|
|
This is to ensure that the corresponding question boxes remains in
front of the main window, consistently with the fact that they are
blocking actions on the main window.
|
|
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.
|
|
This was obsolete since new completion in 945d7db9 (then a07359f6).
|
|
- `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.
|
