aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
Commit message (Collapse)AuthorAge
* Fix BZ#5687: Coqtop died badly modal message box from CoqIDE.Gravatar Pierre-Marie Pédrot2017-08-23
| | | | | We let the user choose the most appropriate action to do if coqtop decides to go berserk.
* Set detachable windows type hint to dialog.Gravatar Olivier Marty2017-08-08
| | | | | Windows such as Search & Replace are dialogs. For some window managers, the hint changes how the window is displayed.
* Merge PR #919: Remove a few useless evar-normalizations in printing code.Gravatar Maxime Dénès2017-08-01
|\
* \ Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \
* \ \ Merge PR #823: Async off in Windows by default in CoqIDEGravatar Maxime Dénès2017-07-28
|\ \ \
| | * | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| |/ / |/| |
| | * Remove a few useless evar-normalizations in printing code.Gravatar Pierre-Marie Pédrot2017-07-26
| |/ |/|
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\ \
* | | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| | |
| | * disable async on Windows by defaultGravatar Paul Steckler2017-06-26
| |/ |/|
* | [ide] Correct more merging errors.Gravatar Emilio Jesus Gallego Arias2017-06-21
| | | | | | | | This file doesn't want to leave us.
| * Default colors for CoqIDE are actually applied.Gravatar Cyprien Mangin2017-06-20
| | | | | | | | | | | | 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.
* | Merge PR#774: [ide] Add route_id parameter to query call.Gravatar Maxime Dénès2017-06-20
|\ \
* \ \ Merge PR#795: [ide] Better exn printing. [fixes BZ#5524]Gravatar Maxime Dénès2017-06-19
|\ \ \
| | | * Change CoqIDE-specific to neutral wordingGravatar Paul Steckler2017-06-19
| | | |
| | * | [ide] Add route_id parameter to query call.Gravatar Emilio Jesus Gallego Arias2017-06-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is necessary in order for clients to identify the results of queries. This is a minor breaking change of the protocol, affecting only this particular call. This change is necessary in order to fix bug ####.
| * | | [ide] Better exn printing. [fixes BZ#5524]Gravatar Emilio Jesus Gallego Arias2017-06-18
| |/ / | | | | | | | | | | | | | | | | | | | | | Due to the situation explained in bug 5360, error printing in ide_slave results in an anomaly. We fix that by properly processing the error. This fixes BZ#5524, however BZ#5525 , still applies.
* / / Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
|/ /
* | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
| * Bump year in headers.Gravatar Maxime Dénès2017-06-01
| |
* | [ide] Correct merging error.Gravatar Emilio Jesus Gallego Arias2017-05-30
| | | | | | | | | | | | | | There was a mistake in the conflict resolution of merge 6f2c19a1054ce58927dfa5b33131c3665fd5fdf8 which wrongly undid the the deletion of the file `ide/texmacspp.ml` in 6a412da , fixing here and sorry for the problem.
* | Merge PR#356: Making management of installation directories more structured, ↵Gravatar Maxime Dénès2017-05-30
|\ \ | | | | | | | | | more uniform
| * | Relying on computation done in Envars to discover the installation directories.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | This allows to share the test for possible relocalisation done in envars.ml.
| * | Configuration: always giving a value to configdir and datadir.Gravatar Hugo Herbelin2017-05-29
| | | | | | | | | | | | | | | | | | | | | They were not used for looking for coqide files in the situation when the effective installation path happens to be exactly the installation path proposed by default, while relevant files were however (possibly) installed in these directories.
* | | Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Gaëtan Gilbert2017-05-28
|/ / | | | | | | | | | | | | | | 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]
* | Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\ \
* \ \ Merge PR#406: coq makefile2Gravatar Maxime Dénès2017-05-25
|\ \ \
* \ \ \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \ \ \
| | | * | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which this PR solves, I propose to remove support for non-synchronous options. It seems the few uses of `optsync = false` we legacy and shouldn't have any impact. Moreover, non synchronous options may create particularly tricky situations as for instance, they won't be propagated to workers.
| | * | | CoqProject_file: API and code cleanup (tuples -> records)Gravatar Enrico Tassi2017-05-23
| | | | |
| | * | | ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mliGravatar Enrico Tassi2017-05-23
| | | | | | | | | | | | | | | | | | | | The .mli only acknowledges the current API. I'm not guilty your honor!
| | * | | ide/project_fie.ml4: include standard banner with copyrightGravatar Enrico Tassi2017-05-23
| | |/ /
| * / / [vernac] Remove `Save.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
| |/ / | | | | | | | | | It has been deprecated for a while in favor of `Qed`.
| * | [ide] Disable `print_ast` call.Gravatar Emilio Jesus Gallego Arias2017-05-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | So far this part of the system has shown little utility other than having developers put time to fix it every time they change something in the system. I have never seen this functionality used in the wild, and a large part of the vernac was marked TODO. Given that we have automatic methods to provide this functionality these days (PPX), we remove Texmacspp.
| * | labelizing argumentsGravatar Pierre Courtieu2017-05-04
| | |
| * | Adding an option "Printing Unfocused".Gravatar Pierre Courtieu2017-05-04
| | | | | | | | | | | | | | | | | | Off by default. + small refactoring of emacs hacks in printer.ml.
| * | Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
| |\ \
| * \ \ Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of ↵Gravatar Maxime Dénès2017-04-28
| |\ \ \ | | | | | | | | | | | | | | | let-ins
| | | * | Remove uses of [Flags.make_silent]Gravatar Gaetan Gilbert2017-04-27
| | | | |
| | | * | Warning 29: non escaped end of line may be non portableGravatar Gaetan Gilbert2017-04-27
| | | | |
| | | * | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | | | |
| | | * | Use [method!] to override methods (warning 7)Gravatar Gaetan Gilbert2017-04-27
| | | | |
| | | * | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| | |/ / | |/| |
* | | | [location] [ast] Switch Constrexpr AST to an extensible node type.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Following @gasche idea, and the original intention of #402, we switch the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast` which is private and record-based. This provides significantly clearer code for the AST, and is robust wrt attributes.
* | | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
* | | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | | | | | | | | | Now it is a private field, locations are optional.
* | | | [location] Use located in misctypes.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | |
* | | | [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is the second patch, which is a bit more invasive. We reasoning is similar to the previous patch. Code is not as clean as it could as we would need to convert `glob_constr` to located too, then a few parts could just map the location.
* | | | [constrexpr] Make patterns use Loc.located for location informationGravatar Emilio Jesus Gallego Arias2017-04-24
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is first of a series of patches, converting `constrexpr` pattern data type from ad-hoc location handling to `Loc.located`. Along Coq, we can find two different coding styles for handling objects with location information: one style uses `'a Loc.located`, whereas other data structures directly embed `Loc.t` in their constructors. Handling all located objects uniformly would be very convenient, and would allow optimizing certain cases, in particular making located smarter when there is no location information, as it is the case for all terms coming from the kernel. `git grep 'Loc.t \*'` gives an overview of the remaining work to do. We've also added an experimental API for `located` to the `Loc` module, `Loc.tag` should be used to add locations objects, making it explicit in the code when a "located" object is created.
* | | Merge PR#565: Remove VernacErrorGravatar Maxime Dénès2017-04-24
|\ \ \