aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-05-15Coqide: in win32 command given to cmd.exe should be more quotedletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15328 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-15when cross-compiling with mingw32, let's fix the Filename.dir_sepletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15327 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-15Makefile: Really avoid locales in $(DATE)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15326 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-15Coqide: display initial connection errors in popups instead of on stderrletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15325 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-15Notations are back in the "in" clause of pattern matching.pboutill
Fixes the test-suite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15324 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-13Added semantic completion in CoqIDE. (Should also add an option for that...)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15317 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-13Tweaking options of CoqIDE.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15316 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-13Some cosmetic changes w.r.t. the previous commit.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15315 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-13Heavily rewritten the coqtop management process of coqide. The coqtopppedrot
object is now responsible for restarting itself, and handles unexpected crashes. Fixes a lot of errors in file descriptor management, but may introduce lurking deadlocks and nasty bugs waiting to be discovered. Only (quickly) tested under Linux, any callbacks from Windows are welcome. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15314 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-13Added a SearchAbout-like primitive in coqtop interface.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15313 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-13Added an interface primitive to ask coqtop for its internal versions.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15312 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-11Vectors takes advantage of pattern matching compiler fixuppboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15308 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-11Impossible branches inference fixup (bug 2761)pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15307 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-11Makefile.build typo in echopboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15306 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-11Slightly modified the coqtop interface by adding an identifier inppedrot
goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15303 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-11Tentative and very experminental support for typerex. Enabled withaspiwack
./configure -typerex . It causes (non-fatal) errors when compiling files without a .mli (the problem seems to have something to do with the flag -intf-suffix .cmi). In practice, most typerex functionalities don't work well because typerex fails its lookup into files compiled with -rectypes. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15302 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-11Coqide awful coqtop options parsing fixuppboutill
(back to the future) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15301 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-10Addedum to documentation of bullets: I now use the dedicated coq_exampleaspiwack
environment to display the example. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15295 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-10Documentation for Unfocused, braces and bullets.aspiwack
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15293 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-09Little bit of code refactoring in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15292 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-09Bug 2767pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15291 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-09Tactic unfold always asks for comma between names.pboutill
Else the parser takes "at" as a constant to unfold in "unfold plus at ...". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15290 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-09End of Gtksourceview switch clean.pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15289 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-08Removing dead code in CoqIDE made useless by the GtkSourceView switch.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15288 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-05-08Rephrasing section on Sorts in CIC chapter, accordingly to discussionsherbelin
with Assia and Guillaume. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15284 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-08Ref. man., ch. CIC: clarifying the redundancy coming from having bothherbelin
Prop <= Type(i) and the conjunction of Prop <= Set and Set <= Type(i). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15283 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-08Rewritten the autocompletion mechanism of CoqIDE, and stuffed itppedrot
into the ScriptView widget. The autocompletion algorithm may be a bit too greedy, so there are tests to do on huge buffers to check whether it is too slow and therefore we should fine-tune it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15282 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-06Cleanly rewritten the undo manager, which did not support redo and hadppedrot
a lot of deprecated code. Trying to be nicer with the built-in undo manager of GtkSourceView btw. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15281 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-05Renamed Undo to conform to CoqIDE widget naming convention. In addition,ppedrot
made various hack to handle GtkSourceView built-in undo/redo and made method types and names more compliant with the one of Gtk. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15280 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-05Hack to handle trailing whitespace display in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15279 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-03Fixup r15251 second timepboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15275 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Added a bunch of new options relative to editor.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15274 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Better style handling in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15273 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Fixed previous commitppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15272 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Removed the useless use of a reference in preference handling.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15271 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Quick workaround to handle badly designed Sourceview package.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15270 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Coqide highligthing is back (done by gtksourceview).pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15269 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Coqide coq lexer put one tag at the end of a sentence.pboutill
And that's all ! It erase the possibility of code folding... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15268 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Source language and style are preferencespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15267 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02undoable_view is a source_viewpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15266 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Always add the Coq_config.dirs to xdg_dirspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15265 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Fixed #2769ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15264 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02Added an interface call to exit Coqtop nicely.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15263 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-02A notion of permutation for lists modulo a setoid equalityletouzey
Contribution by Robbert Krebbers (Nijmegen University). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15261 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-01Cleaned the interface of analyzed_view in CoqIDE. A lot of methodsppedrot
have been made private, for the sake of readability and conciseness. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15260 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-30This is a tentative bugfix for the numerous GText.iter erros occuring in CoqIDE.ppedrot
Because of the previous highlighting process, whenever this process would fail on an unterminated phrase, a thread would wait 1.5s and retry once. This thread conflicted in particular with any subsequent non-atomic use of iters. Actually, this seems pretty useless, so until using SourceView, this sould do the work. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15259 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-30Fixed an accelerator parsing error in CoqIDE introduced in r15254ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15258 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-28Fix make install after emacs mode troll (r15251)pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15256 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-04-27Configure asks for lablgtk >= 2.12 with gtksourceview2pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15255 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-01 11:59:44 +0000