aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
Commit message (Collapse)AuthorAge
* Fix typo.Gravatar Guillaume Melquiond2015-10-30
|
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
|
* Goptions: new value type: optional stringGravatar Enrico Tassi2015-10-08
| | | | | These options can be set to a string value, but also unset. Internal data is of type string option.
* Change the default modifiers for navigation. (Fix bug #4295)Gravatar Guillaume Melquiond2015-09-21
| | | | | | | | On most systems (including Windows, according to the bug report), shortcuts Ctrl+Alt+Arrows are preempted by the window manager by default. So don't use them for navigation in Coqide by default. Note that this change only has an impact when installing on a fresh system; it won't change anything for existing users.
* Removing a warning in CoqOps.Gravatar Pierre-Marie Pédrot2015-09-15
|
* Fixing bug #2498: Coqide navigation preferences delayed effect.Gravatar Pierre-Marie Pédrot2015-09-12
|
* Extending the grammar for CoqIDE preferences so as to match trunk.Gravatar Pierre-Marie Pédrot2015-09-10
|
* Highlighting of the "Next Obligation" command in CoqIDE.Gravatar Pierre-Marie Pédrot2015-08-17
|
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| | | | | | | | | | | | | | | | | | | | | | Sorry so much. Reverted: 707bfd5719b76d131152a258d49740165fbafe03. 164637cc3a4e8895ed4ec420e300bd692d3e7812. b9c96c601a8366b75ee8b76d3184ee57379e2620. 21e41af41b52914469885f40155702f325d5c786. 7532f3243ba585f21a8f594d3dc788e38dfa2cb8. 27fb880ab6924ec20ce44aeaeb8d89592c1b91cd. fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c. d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962. 6737055d165c91904fc04534bee6b9c05c0235b1. 342fed039e53f00ff8758513149f8d41fa3a2e99. 21525bae8801d98ff2f1b52217d7603505ada2d2. b78d86d50727af61e0c4417cf2ef12cbfc73239d. 979de570714d340aaab7a6e99e08d46aa616e7da. f556da10a117396c2c796f6915321b67849f65cd. d8226295e6237a43de33475f798c3c8ac6ac4866. fdab811e58094accc02875c1f83e6476f4598d26.
* Failing when reaching end of file with unterminated comment whenGravatar Hugo Herbelin2015-08-02
| | | | parsing Make (project) file.
* Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)Gravatar Guillaume Melquiond2015-07-28
| | | | | | | | File system.ml seemed like a better choice than util.ml for sharing the code, but it was bringing a bunch of useless dependencies to the IDE. There are presumably several other tools that would benefit from using open_utf8_file_in instead of open_in, e.g. coqdoc.
* CoqIDE: recenter on backtrack (Close: #4277)Gravatar Enrico Tassi2015-07-11
|
* Highlighting Universe in CoqIDE.Gravatar Hugo Herbelin2015-07-10
|
* Ide: fix bug #4284 for goodGravatar Matthieu Sozeau2015-07-08
| | | | Correct folding order over the named_list_context.
* Bug 4284: Tentative bugfix for detyping exception.Gravatar Matthieu Sozeau2015-07-08
|
* Make end-of-proof output consistent across toplevels.Gravatar Guillaume Melquiond2015-06-19
| | | | | Ideally, the code should be shared between the various toplevels, but this is a lot more work than just fixing a few strings.
* Fix by Enrico on CoqIDE not locating errors anymore since 550da87456a.Gravatar Hugo Herbelin2015-06-16
|
* Fixing bug #4233: The command Restart is not fontified correctly.Gravatar Pierre-Marie Pédrot2015-06-07
|
* coqide: don't require ocaml >= 4Gravatar Enrico Tassi2015-05-29
|
* Jump to error line in CoqIDE grabs focus of the textview.Gravatar Pierre-Marie Pédrot2015-05-26
|
* CoqIDE columns in error and job panels can be sorted.Gravatar Pierre-Marie Pédrot2015-05-25
| | | | This grants wish #4194.
* Compatibility ocaml 3.12.Gravatar Hugo Herbelin2015-05-05
|
* Granting wish #4221.Gravatar Pierre-Marie Pédrot2015-05-05
|
* Improve syntax highlighting.Gravatar Guillaume Melquiond2015-04-27
| | | | | | | | - Arithmetic operators and brackets are no longer recognized as bullets, unless they follow a stop or start a line. - Most vernacular commands are no longer highlighted when used inside proof scripts. - Coqdoc comments now take precedence over regular comments.
* Open the file chooser even if there is no current session. (Fix bug #4206)Gravatar Guillaume Melquiond2015-04-26
|
* Add extraction to JSON.Gravatar Nickolai Zeldovich2015-04-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This patch allows Coq terms to be extracted into the widely used JSON format. This is useful in at least two cases: - One might want to manipulate Coq values outside of Coq, but without being forced to use one of the three existing extraction languages (OCaml, Haskell, or Scheme), and without having to compile Coq's extracted result. This is especially useful when a Coq evaluation produces some data structure that needs to be moved out of Coq. Having to invoke an OCaml/Haskell/Scheme compiler just to get a data structure out of Coq is somewhat awkward. - One might want to experiment with extracting Coq code into other languages (Go, Javascript, etc), without having to write the whole extraction logic in OCaml and recompile Coq's extraction plugin each time. This makes it easy to quickly prototype extraction in any language, without having to build Coq from source. Extraction to JSON is implemented by adding the JSON "pseudo-language" to the extraction facility. Thus, one can extract the JSON encoding of a single term using: Extraction Language JSON. Extraction qualid. and extract an entire Coq library "ident" into "ident.json" using: Extraction Language JSON. Extraction Library ident. Nota (Pierre Letouzey) : this is an updated version of the original PullRequest, updated to match recent changes in trunk
* Use the directory of the current session for selecting files to open.Gravatar Guillaume Melquiond2015-04-03
| | | | | | | | | | The old behavior was extremely annoying, especially when using coqide from the command line, since the "open" box would then point to a seemingly random point of the filesystem rather than to the directory of the files currently being edited (since they were passed on the command line rather than by point-and-click). The new behavior matches the one of mainstream editors, e.g. emacs, gedit.
* CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)Gravatar Enrico Tassi2015-04-02
| | | | | | | | | | | 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.
* CoqIDE: load first _CoqProject file found and notify the userGravatar Enrico Tassi2015-03-11
|
* CoqIDE: fix tag colors to support superposing unsafe and partialGravatar Enrico Tassi2015-03-11
| | | | Admitted (like Qed) can be "partially executed", but is also unsafe.
* CoqIDE: restore module/proof name in info barGravatar Enrico Tassi2015-03-11
|
* CoqIDE: do not lose tag on Qed ending focused proofGravatar Enrico Tassi2015-03-11
|
* Simplify grammar for syntax highlighting by removing extraneous parentheses.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Print/Reset Extraction.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Extraction Inline and add Separate Extraction.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Extraction Language.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Typeclasses Opaque.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Module (Type).Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Extract Inductive.Gravatar Guillaume Melquiond2015-03-06
|
* Add syntax highlighting for Declare Module.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Import and Export.Gravatar Guillaume Melquiond2015-03-06
|
* Add syntax highlighting for Declare ML Module.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Require.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Scheme.Gravatar Guillaume Melquiond2015-03-06
|
* Do not highlight "using" as a constr keyword.Gravatar Guillaume Melquiond2015-03-06
|
* Add syntax highlighting for About.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Save.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of Hypothesis, Axiom, Variable, Parameter, and Context.Gravatar Guillaume Melquiond2015-03-06
|
* Add syntax highlighting for Coercion.Gravatar Guillaume Melquiond2015-03-06
|
* Fix syntax highlighting of "Require multiple libraries".Gravatar Guillaume Melquiond2015-03-06
|