aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
Commit message (Collapse)AuthorAge
* Fix bug #2191 : Serious "undo" performance degradation since 8.2pl1Gravatar vgross2009-12-03
| | | | | | | | | This reverts commit 12537 This reverts commit 12199 This reverts commit 12198 This reverts commit 12172 (introduced the bug) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12559 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ergonomy and robustness fixGravatar vgross2009-11-23
| | | | | | | | Sentences are locked up to the period, and it's now possible to eval when there is no final whitespace. CoqIde will refuse to evaluate further if there is no whitespace, though. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12539 85f007b7-540e-0410-9357-904b9bb8a0f7
* Refactoring of coqide backtrack code, with the intent to put everythingGravatar vgross2009-11-19
| | | | | | | | into coqtop. Also, some cleaning in ide/gtk_parsing.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12537 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
* scripting area now grabs focus at startup.Gravatar vgross2009-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12518 85f007b7-540e-0410-9357-904b9bb8a0f7
* new handling for lexical structures.Gravatar vgross2009-11-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | Sentence extraction and proof folding is now done with tags. The lexer has been modified to use a callback to "stamp" the lexical constructs that must be distinguished. new funcs in ide/coqide.ml : apply_tag : GText.buffer -> GText.iter -> (int -> int) -> int -> int -> CoqLex.token -> unit remove_tags : GText.buffer -> GText.iter -> GText.iter -> unit tag_slice : GText.buffer -> GText.iter -> GText.iter -> (GText.buffer -> GText.iter -> GText.iter) -> unit get_sentence_bounds : GText.iter -> GText.iter * GText.iter end_tag_present : GText.iter -> bool tag_on_insert : GText.buffer -> unit force_retag : GText.buffer -> unit toggle_proof_visibility : GText.buffer -> GText.iter -> unit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12517 85f007b7-540e-0410-9357-904b9bb8a0f7
* lexing refactoringGravatar vgross2009-11-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12516 85f007b7-540e-0410-9357-904b9bb8a0f7
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12485 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed 'Toplevel' language from extraction documentation, since it is not ↵Gravatar gmelquio2009-11-04
| | | | | | currently supported. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12467 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added Coqide highlighting for extraction vernacular.Gravatar gmelquio2009-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12448 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed 'dest' from keyword highlighting.Gravatar gmelquio2009-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12447 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integrate a few improvements on typeclasses and Program from the equations ↵Gravatar msozeau2009-10-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | branch and remove equations stuff which moves to a separate plugin. Classes: - Ability to define classes post-hoc from constants or inductive types. - Correctly rebuild the hint database associated to local hypotheses when they are changed by a [Hint Extern] in typeclass resolution. Tactics and proofs: - Change [revert] so that it keeps let-ins (but not [generalize]). - Various improvements to the [generalize_eqs] tactic to make it more robust and produce the smallest proof terms possible. Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with [generalize_eqs]. - A few new general purpose tactics in Program.Tactics like [revert_until] - Make transitive closure well-foundedness proofs transparent. - More uniform testing for metas/evars in pretyping/unification.ml (might introduce a few changes in the contribs). Program: - Better sorting of dependencies in obligations. - Ability to start a Program definition from just a type and no obligations, automatically adding an obligation for this type. - In compilation of Program's well-founded definitions, make the functional a separate definition for easier reasoning. - Add a hint database for every Program populated by [Hint Unfold]s for every defined obligation constant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
| | | | | | | | | | | | | variables with syntax: [Local?|Global] Generalizable Variable(s)? [all|none|id1 idn]. By default no variable is generalizable, so this patch breaks backward compatibility with files that used implicit generalization (through Instance declarations for example). To get back the old behavior, one just needs to use [Global Generalizable Variables all]. Make coq_makefile more robust using [mkdir -p]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12428 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added syntactic coloration for 'Function'.Gravatar gmelquio2009-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12403 85f007b7-540e-0410-9357-904b9bb8a0f7
* note for later : when the tag table is shared, never, ever create twoGravatar vgross2009-10-16
| | | | | | tags with the same name. This fixes file opening. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12396 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revert "kills the old backtracking framework and replaces it with"Gravatar vgross2009-10-05
| | | | | | This reverts commit 33545cc88bf4b4e19b222afd2d1d264bcba97838. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12373 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removal of trailing spaces.Gravatar serpyc2009-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12371 85f007b7-540e-0410-9357-904b9bb8a0f7
* kills the old backtracking framework and replaces it withGravatar vgross2009-09-29
| | | | | | ProofGeneral-like "Backtrack". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12364 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
* removed the double-click / proof hiding association.Gravatar vgross2009-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12328 85f007b7-540e-0410-9357-904b9bb8a0f7
* tags refactoringGravatar vgross2009-09-14
| | | | | | | all tags are isolated in tags.ml, and all tags are accessed directly, not through their names. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12327 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de la gestion de Local et Global pour les options (au sens deGravatar aspiwack2009-08-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | Goptions). - Local Set/Unset ... change la valeur de l'option pour la section en cours (ou le module si il n'y a pas de section), l'option est restaurée à sa valeur précédente au sortir de la section. - Set/Unset ... survit aux sections mais pas aux modules. - Global Set/Unset ... survit aux sections et aux modules. Il y a une légère source d'incompatibilité là, Set avait le comportement de Local Set. Ça n'apparaît pas dans la lib standard, mais sait-on jamais. Les étapes suivantes : - Supprimer la notion d'option asynchrone, je n'en vois vraiment pas l'intérêt. Changer le type de retour de declare_option à unit aussi serait probablement une bonne idée. - Ajouter le support Local/Global à d'autres commandes sur le même modèle. Conflicts: parsing/g_vernac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12280 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tried to make F1 documentation tool working in CoqIDE.Gravatar herbelin2009-08-14
| | | | | | | | | | | | | | | | | | | | | | | In trunk: New strategy for compiling and finding index_url.txt. After all, this file is not specific to CoqIDE but to the documentation. Hence, it seems better to install it close to the documentation. If the documentation is locally installed, it is easy to find the file index_url.txt but what to do if the documentation is remote? We would need a http getter. Does this mean we have to rely on wget or so? In the absence of answer to this question, it seems reasonable, first to assume the doc to be locally installed, second to have a local copy of index_url.txt ready in the installation directory of CoqIDE. Also added an "automatic" field in the CoqIDE url preference to prevent the user to have to update his preference file every time a new version of Coq is out and the link to the doc change. In 8.2: Added a minima the installation of index_urls.txt but the user will have to update its preferences because the links "http://coq.inria.fr/doc/Reference-Manual010.html#..." do not longer exist. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12278 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added "etransitivity".Gravatar herbelin2009-08-03
| | | | | | | | | | | | Added support for "injection" and "discriminate" on JMeq. Seized the opportunity to update coqlib.ml and to rely more on it for finding the equality lemmas. Fixed typos in coqcompat.ml. Propagated symmetry convert_concl fix to transitivity (see 11521). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
| | | | | | | | | | | | | | | - add coqtop option "-compat X.Y" so as to provide compatibility with previous versions of Coq (of course, this requires to take care of providing flags for controlling changes of behaviors!), - add support for option names made of an arbitrary length of words (instead of one, two or three words only), - add options for recovering 8.2 behavior for discriminate, tauto, evar unification ("Set Tactic Evars Pattern Unification", "Set Discriminate Introduction", "Set Intuition Iff Unfolding"). Update of .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
* Completing support for F5=About by adding About to the state-preserving ↵Gravatar herbelin2009-07-08
| | | | | | command list git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12225 85f007b7-540e-0410-9357-904b9bb8a0f7
* Miscellaneous practical commits: Gravatar herbelin2009-06-29
| | | | | | | | | | | | - theories: made a hint database with the constructor of eq_true - coqide: binding F5 to About dans coqide + made coqide aware of string interpretation inside comments - lexer: added warning when ending comments inside a strings itself in a comment - xlate: completed patten-matching on IntroForthComing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12217 85f007b7-540e-0410-9357-904b9bb8a0f7
* remove some unused functions (which are part of a soon-to-be obsoleteGravatar vgross2009-06-22
| | | | | | framework anyway) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12199 85f007b7-540e-0410-9357-904b9bb8a0f7
* clearing unused functionsGravatar vgross2009-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12198 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplifying the call to print_no_goals and not calling it when no goalGravatar herbelin2009-06-11
| | | | | | | | is ongoing. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12184 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change in UI behaviour : proof folding is now done by double clicking. Delay isGravatar vgross2009-06-08
| | | | | | | | configurable through preferences. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12174 85f007b7-540e-0410-9357-904b9bb8a0f7
* Partial simplification of undo mechanism, relying only on Courtieu'sGravatar herbelin2009-06-07
| | | | | | | marks and no longer on old-fashioned reset to id. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12172 85f007b7-540e-0410-9357-904b9bb8a0f7
* sane behaviour for copy/paste operations (the code is still insane, though)Gravatar vgross2009-05-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12145 85f007b7-540e-0410-9357-904b9bb8a0f7
* keeping interface synch'edGravatar vgross2009-05-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12144 85f007b7-540e-0410-9357-904b9bb8a0f7
* dead code pruningGravatar vgross2009-05-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12143 85f007b7-540e-0410-9357-904b9bb8a0f7
* minor bugfixes. CoqIde development will resume soon now ...Gravatar vgross2009-05-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12124 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de la révision #12104 (Maj lien site web de Coq)Gravatar notin2009-04-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12105 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove unused mli filesGravatar letouzey2009-03-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12023 85f007b7-540e-0410-9357-904b9bb8a0f7
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
| | | | | | | | | | | | | | | | | | | | | | | | * generalize the use of .mllib to build all cma, not only in plugins/ * the .mllib in plugins/ now mention Bruno's new _mod.ml files * lots of .cmo enumerations in Makefile.common are removed, since they are now in .mllib * the list of .cmo/.cmi can be retreive via a shell script line, see for instance rule install-library * Tolink.core_objs and Tolink.ide now contains ocaml _modules_, not _files_ * a -I option to coqdep_boot allows to control piority of includes (some files with the same names in kernel and checker ...) This is quite a lot of changes, you know who to blame / report to if something breaks. ... and last but not least I've started playing with ocamlbuild. The myocamlbuild.ml is far from complete now, but it already allows to build coqtop.{opt,byte} here. See comments at the top of myocamlbuild.ml, and don't hesitate to contribute, either for completing or simplifying it ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12002 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleanup: remove 3 unused files in ide/Gravatar letouzey2009-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11972 85f007b7-540e-0410-9357-904b9bb8a0f7
* - per session coq command stackGravatar vgross2009-03-07
| | | | | | | | | | | - removed circular dependency between record and class used to keep track of sessions => no need for mutable option in record. - more 'a option ref pruning - more code splitting - more alpha-rewriting git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11968 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixed groebner as a plugin + pattern matching TimeoutGravatar barras2009-03-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11967 85f007b7-540e-0410-9357-904b9bb8a0f7
* Temporary hack to make coqide.byte work (backport r11948) (see #2062)Gravatar glondu2009-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11957 85f007b7-540e-0410-9357-904b9bb8a0f7
* fixes to typecheck with old lablgtk.Gravatar vgross2009-03-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11956 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hack to fix compilation problems. will be removed on lablgtk upgrade.Gravatar vgross2009-03-03
| | | | | | | Also, added copyright headers and stuff git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11955 85f007b7-540e-0410-9357-904b9bb8a0f7
* Heavy modifications on the widget and edition tab creation mechanism.Gravatar vgross2009-03-02
| | | | | | | | Overloading of GPack.notebook => Vector no longer needed git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11952 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle icône pour CoqGravatar notin2009-02-11
| | | | | | (cherry picked from commit 89ba1ca851637fa45b6c52f2a95e37e688fcbf3a) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11920 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report des revisions #11826, #11828 et #11829 de v8.2 vers trunkGravatar notin2009-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11915 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'ancien logo (problèmes de droits)Gravatar notin2009-01-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11854 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-17 02:20:25 +0000