| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-03-19 | [coqide] [ci] Update GTK toolchain to lablgtk3 | Emilio Jesus Gallego Arias | |
| - Update Docker images to install compatible version of lablgtk3 - We remove unnecesary variables from configure. - We fix path detection of GTK libs in makefile | |||
| 2019-03-19 | Fix for post-beta3 lablgtk3 changes about cairo (from Claudio). | Hugo Herbelin | |
| 2019-03-19 | CoqIDE: Adding configurable color for incompletely processed Qed. | Hugo Herbelin | |
| 2019-03-19 | CoqIDE: More informative message when failing editing/saving preferences. | Hugo Herbelin | |
| 2019-03-19 | CoqIDE: Ensuring that load/save windows are not hidden by their parent. | Hugo Herbelin | |
| 2019-03-19 | CoqIDE: Use modify_bg rather than modify_base to change background color. | Hugo Herbelin | |
| The effect of modify_base is told to be widget-dependent. It uses to change the background with gtk2 but not with gtk3. So we use the more explicit modify_bg. | |||
| 2019-03-19 | CoqIDE: Ensure that the main 3 windows do not shrink when w/o contents. | Hugo Herbelin | |
| This was automatic in gtk2 (apparently because of the specification not being granted). This is needed with gtk3. | |||
| 2019-03-19 | CoqIDE: Ensure that contents of the pref window expands as much as possible. | Hugo Herbelin | |
| This was not needed in gtk2 but is needed with gtk3. | |||
| 2019-03-19 | CoqIDE: Using Grid instead of Table. | Hugo Herbelin | |
| This is not mandatory for gtk+3 since it is deprecated from only gtk 3.4. This would be needed for gtk+4 though. | |||
| 2019-03-19 | CoqIDE: Adapting to new interface of GPack.notebook. | Hugo Herbelin | |
| 2019-03-19 | CoqIDE: Replacing deprecated color_of_string with color_parse. | Hugo Herbelin | |
| 2019-03-19 | CoqIDE: No more explicit activation of tooltips on toolbar. | Hugo Herbelin | |
| 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. | |||
| 2019-03-19 | CoqIDE: Stippling using bitmap no more supported for incomplete Qed. | Hugo Herbelin | |
| Was formerly displaying a stippled ("pointillé") light blue. Now only a light blue. | |||
| 2019-03-19 | CoqIDE: wm_name and wm_class are now packed into wmclass. | Hugo Herbelin | |
| 2019-03-19 | CoqIDE: Now calling destroy signal via widget_signals. | Hugo Herbelin | |
| Thanks to J. Garrigue for the hint. | |||
| 2019-03-19 | CoqIDE: Deactivation pixmap-based progression bar (wg_Segment.ml). | Hugo Herbelin | |
| Indeed, gtk3 has no more Pixmap, it should use Cairo instead. We also deactivate the functions in the graph of dependency. In particular, this also blocks coqOps.ml. | |||
| 2019-03-19 | CoqIDE: Moving last use of gtk2-only FileSelection to FileChooserDialog. | Hugo Herbelin | |
| 2019-03-19 | CoqIDE: Deactivating the user queries and wizard tactics configuration. | Hugo Herbelin | |
| They rely on list and strings from configwin which themselves rely on gtk2 only widgets. | |||
| 2019-03-19 | CoqIDE: Deactiving the list and string configuration tools. | Hugo Herbelin | |
| They rely on gtk2 clist and would need to be changed to list_store. | |||
| 2019-03-19 | CoqIDE: Ensuring that gtk is initialized before other inits done in ideutils.ml. | Hugo Herbelin | |
| This seems fragile: does it depend on the order files are loaded? (It was working for gtk2 when gtk initialization was in coqide_main.ml but it does not work anymore for CoqIDE built on gtk3). Eventually, it might be needed to centralize all initialization side effects in one place. | |||
| 2019-03-19 | CoqIDE: Change name of module: Sourceview2 -> Sourceview3 | Hugo Herbelin | |
| 2019-03-19 | CoqIDE: Adapt configuration to require lablgtk3 and gtksourceview3. | Hugo Herbelin | |
| 2019-03-19 | CoqIDE: Replacing Tooltips with gtk+3 compliant Tooltip. | Hugo Herbelin | |
| 2019-03-04 | [dune] [ide] Don't install the internal CoqIDE UI library. | Emilio Jesus Gallego Arias | |
| This library is unstable and not meant to be consumed by anyone. We thus make it private. | |||
| 2019-02-28 | Merge PR #9621: [ide] only use Coq_config for the URL of the manual | Pierre-Marie Pédrot | |
| Ack-by: JasonGross Reviewed-by: ejgallego Ack-by: gares Reviewed-by: ppedrot | |||
| 2019-02-27 | [ide] only use Coq_config for the URL of the manual | Enrico Tassi | |
| 2019-02-27 | [ide] coqtop -> coqidetop in user messages | Enrico Tassi | |
| 2019-02-11 | [ide] fix unconditional goto-point on editing an error (fix #9488) | Enrico Tassi | |
| 2019-02-05 | [parsing] Use AST node for main parsing entry. | Emilio Jesus Gallego Arias | |
| Before #9263 this type was returned by the STM's `parse_sentence`, but the type was lost on the generalization to entries. | |||
| 2019-02-01 | [toplevel] Split interactive toplevel and compiler binaries. | Emilio Jesus Gallego Arias | |
| We make `coqc` a truly standalone binary, whereas `coqtop` is restricted to interactive use. Thus, `coqtop -compile` will emit a warning and call `coqc`. We have also refactored `Coqargs` into a common `Coqargs` module and a compilation-specific module `Coqcargs`. This solves problems related to `coqc` having its own argument parsing, and reduces the number of strange argument combinations a lot. | |||
| 2019-01-27 | [fake_ide] infrastructure to test the failure of an ADD | Enrico Tassi | |
| 2019-01-27 | [ide] fail on unavailable commands before adding to the document | Enrico Tassi | |
| 2019-01-24 | [STM] explicit handling of parsing states | Enrico Tassi | |
| DAG nodes hold now a system state and a parsing state. The latter is always passed to the parser. This paves the way to decoupling the effect of commands on the parsing state and the system state, and hence never force to interpret, say, Notation. Handling proof modes is now done explicitly in the STM, not by interpreting VernacStartLemma. Similarly Notation execution could be split in two phases in order to obtain a parsing state without fully executing it (that requires executing all commands before it). Co-authored-by: Maxime Dénès <maxime.denes@inria.fr> Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org> | |||
| 2018-12-18 | Merge PR #9178: CoqIDE: Restoring configuration of default width/height of ↵ | Pierre-Marie Pédrot | |
| main window. | |||
| 2018-12-17 | Merge PR #9206: [stm] join the tip of the document even when fixing a proof ↵ | Emilio Jesus Gallego Arias | |
| (fix #9204) | |||
| 2018-12-17 | CoqIDE: Restoring configuration of default width/height of main window. | Hugo Herbelin | |
| Also removing dead code about show_toolbar: this is governed by an item of the view menu rather than by the preference panel since aa357d601 (Dec 2003). | |||
| 2018-12-14 | [proof] Rework proof interface. | Emilio Jesus Gallego Arias | |
| - deprecate the old 5-tuple accessor in favor of a view record, - move `name` and `kind` proof data from `Proof_global` to `Proof`, this will prove useful in subsequent functionalizations of the interface, in particular this is what abstract, which lives in the monads, needs in order no to access global state. - Note that `Proof.t` and `Proof_global.t` are redundant anyways. | |||
| 2018-12-13 | [test] for join when error resiliency on and async-proofs off | Enrico Tassi | |
| 2018-12-13 | [test] for #9204 | Enrico Tassi | |
| 2018-12-12 | Merge PR #9101: Fix 8922 again | Hugo Herbelin | |
| 2018-12-10 | Treat unmatched goals as new for diffs (highlighted) | Jim Fehrle | |
| Improve debug output | |||
| 2018-12-09 | [doc] Enable Warning 50 [incorrect doc comment] and fix comments. | Emilio Jesus Gallego Arias | |
| 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 :) | |||
| 2018-11-28 | coqide: Remove unused win32_kill C function | Gaëtan Gilbert | |
| Unused since b0da879dc6abfca6b4e233b7469265a5cf52ce15 (see also followup 4f554c88aa). | |||
| 2018-11-24 | [toplevel] Allow to specify default options. | Emilio Jesus Gallego Arias | |
| In some cases, toplevel ML clients may want to modify the default set of flags that is passed to the main initalization routine. This is for example useful for `idetop` to suppress some undesired printing at startup. I would say that clients ought to have more control, but I do expect that PRs such as #8690 will help providing a better separation thus a mode orthogonal API. | |||
| 2018-11-22 | Merge PR #8967: Fix #8922 (uncaught pp_diff exception) | Hugo Herbelin | |
| 2018-11-20 | Merge PR #8959: [dune] [ide] Install data files. | Enrico Tassi | |
| 2018-11-17 | Merge PR #8992: put protocol/ in ide/.merlin | Pierre-Marie Pédrot | |
| 2018-11-17 | Merge PR #8914: [CoqProject] Abstract warning function for CoqProject readers. | Pierre-Marie Pédrot | |
| 2018-11-17 | Merge PR #8968: Miscellaneous CoqIDE fixes | Pierre-Marie Pédrot | |
| 2018-11-17 | [CoqProject] Abstract warning function for CoqProject readers. | Emilio Jesus Gallego Arias | |
| `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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |