aboutsummaryrefslogtreecommitdiff
path: root/ide/utils/configwin_ihm.ml
AgeCommit message (Collapse)Author
2018-05-24[ide] Move common protocol library to its own folder/object.Emilio Jesus Gallego Arias
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
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
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 ```
2016-09-21Removing dead code in CoqIDE.Pierre-Marie Pédrot
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.
2014-08-25"allows to", like "allowing to", is improperJason Gross
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).
2012-12-08Coqide: use labels for all labelled functionsletouzey
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
2012-05-23Cleaned prerr_endline use.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15354 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-16Revert commit 15287 : the env variables are indeed access at launch-timeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15331 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-08Fixed access to environment variables in CoqIDE. Up to now, thoseppedrot
variables where set at compile time... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15287 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-18Fixed the CoqIDE preference widthppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15217 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-28A revolution has come: CoqIDE, now in color. Fixes bug #2704 btw.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15101 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-26Fix configuration box bug in recursive callpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14618 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25Icons in CoqIdE preference panelpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14590 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-25Configuration window of CoqIdE looks more like other Gtk one.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14589 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-07-27Coqide: GEdit.combo is deprecated since Gtk2.4! We now use ↵pboutill
GEdit.combo_box_entry_text git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14306 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-28Fix function applications without labels (OCaml warning 6)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13469 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-15Change the customization of modifiers (bug #2210)vgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12771 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-13Remove dubious call to Obj.magic (and dead code, by the way)glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12522 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-11-13Remove useless call to Obj.magicglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12521 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-01Quelques amendements liées à la compilation des packages.herbelin
- 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
2007-04-16Fix a bug which sometimes made coqide crash after changingglondu
preferences (first fixed in rev. 9716). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9773 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-08 r8623@thot: notin | 2006-03-08 12:40:57 +0100notin
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
2005-11-08Nettoyage suite à la détection par défaut des variables inutilisées par ↵herbelin
ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-13Passage a la version 1.3 sous GPL des outils okey et configwin de cameleon ↵herbelin
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
2003-12-30ameliorations coqidecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5161 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-07-07Coqide : ported to lablgtk2 snapshot of 2003/07/07monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4221 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14coqide: load/save file encoding support/monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4021 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-07coqide: toolbar/autosavemonate
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
2003-03-07coqide: corrections pour utf8 de coq. highlight synchrone=repare le bug ↵monate
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
2003-03-05CoqIde: Install.ide Revert bugfix.monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3741 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-03coqide: preferences support and optimizationsmonate
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.25.1) at 2026-02-01 21:56:38 +0000