aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/utils/configwin_ihm.ml
Commit message (Collapse)AuthorAge
* [ide] Move common protocol library to its own folder/object.Gravatar Emilio Jesus Gallego Arias2018-05-24
| | | | | | | | | | | | | | | | | The `ide` folder contains two different binaries, the language server `coqidetop` and `coqide` itself. Even if these binaries are in the same folder, the only thing they have in common is that they link to the protocol files. In the OCaml world, having "doubly" linked files in the same project is considered a bit of an ugly practice, and some build tools such as Dune disallow it.q Thus, to clean up the build, we move the common protocol files to its own library `ideprotocol`. This helps towards Dune integration and towards having an IDE standalone target, such as the one that was implemented here: https://github.com/ejgallego/coqide-exp
* 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 ```
* Removing dead code in CoqIDE.Gravatar Pierre-Marie Pédrot2016-09-21
| | | | | There was a pile of dead code inherited from Cameleon just sitting around and not used at all. This code was introduced in 2003 and never actually used.
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
| | | | | | | | | | | It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar).
* Coqide: use labels for all labelled functionsGravatar letouzey2012-12-08
| | | | | | | | This isn't mandatory, but it's a good practice. For instance it allows to easily locate all ~callback arguments. Cf. warning 6 of OCaml 4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16051 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaned prerr_endline use.Gravatar ppedrot2012-05-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15354 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert commit 15287 : the env variables are indeed access at launch-timeGravatar letouzey2012-05-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15331 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed access to environment variables in CoqIDE. Up to now, thoseGravatar ppedrot2012-05-08
| | | | | | variables where set at compile time... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15287 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed the CoqIDE preference widthGravatar ppedrot2012-04-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15217 85f007b7-540e-0410-9357-904b9bb8a0f7
* A revolution has come: CoqIDE, now in color. Fixes bug #2704 btw.Gravatar ppedrot2012-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15101 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix configuration box bug in recursive callGravatar pboutill2011-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14618 85f007b7-540e-0410-9357-904b9bb8a0f7
* Icons in CoqIdE preference panelGravatar pboutill2011-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14590 85f007b7-540e-0410-9357-904b9bb8a0f7
* Configuration window of CoqIdE looks more like other Gtk one.Gravatar pboutill2011-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14589 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide: GEdit.combo is deprecated since Gtk2.4! We now use ↵Gravatar pboutill2011-07-27
| | | | | | GEdit.combo_box_entry_text git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14306 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix function applications without labels (OCaml warning 6)Gravatar glondu2010-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change the customization of modifiers (bug #2210)Gravatar vgross2010-02-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12771 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove dubious call to Obj.magic (and dead code, by the way)Gravatar glondu2009-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12522 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove useless call to Obj.magicGravatar glondu2009-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12521 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques amendements liées à la compilation des packages.Gravatar herbelin2008-06-01
| | | | | | | | | | | | | | | | | | | | | - typo du configure; - warnings variables non utilisées dans ide/utils; - suppression des variables vides COQINSTALLPREFIX et OLDROOT parce que l'option -e que l'on aurait pu en principe utiliser pour les surcharger ne fonctionne pas lorsqu'il y a plusieurs niveaux d'imbrication de makefiles (comme c'est le cas quand on vient du makefile servant à faire les packages qui appelle le makefile principal qui appelle les makefile.stage); - utilisation de ALLVO plutôt qu'un find pour trouver les .v sur lesquels appliquer coqdep (permet d'éviter des warning sur les fichiers de test, non prévus pour faire partie de la biblio standard); - utilisation de -custom sur les bytecode qui ne l'étaient pas encore (coqchk et coqmktop) pour être indépendant de ocamlrun à l'installation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11029 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix a bug which sometimes made coqide crash after changingGravatar glondu2007-04-16
| | | | | | | preferences (first fixed in rev. 9716). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9773 85f007b7-540e-0410-9357-904b9bb8a0f7
* r8623@thot: notin | 2006-03-08 12:40:57 +0100Gravatar notin2006-03-08
| | | | | | | Passage à la version LGPL de Configwin dans le trunk git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8618 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage suite à la détection par défaut des variables inutilisées par ↵Gravatar herbelin2005-11-08
| | | | | | ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage a la version 1.3 sous GPL des outils okey et configwin de cameleon ↵Gravatar herbelin2004-04-13
| | | | | | en remplacement de la version 1.2 qui etait sous QPL git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5670 85f007b7-540e-0410-9357-904b9bb8a0f7
* ameliorations coqideGravatar coq2003-12-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5161 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqide : ported to lablgtk2 snapshot of 2003/07/07Gravatar monate2003-07-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4221 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: load/save file encoding support/Gravatar monate2003-05-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4021 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: toolbar/autosaveGravatar monate2003-05-07
| | | | | | | | | Hugo: Suppression du type dans les notations == et <> entre Suppression du type dans les notations == et <> entre volution second traducteur selon discussion TYPES git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3993 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: corrections pour utf8 de coq. highlight synchrone=repare le bug ↵Gravatar monate2003-03-07
| | | | | | autorepeat des paste. configuration des accel rateurs. les chaines peuvent contenir des points. Bug: les phrases ne peuvent pas contenir .\sep. Or c'est permis par les Notation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3750 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIde: Install.ide Revert bugfix.Gravatar monate2003-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3741 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqide: preferences support and optimizationsGravatar monate2003-03-03
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3724 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-18 13:22:01 +0000