aboutsummaryrefslogtreecommitdiff
path: root/ide
AgeCommit message (Collapse)Author
2012-08-24Modification of the unjustified tag.aspiwack
It seemed to intrusive to have it display the text underlined and red. The goal of this tag is to notify the user when Coq doesn't guarantee correctness, not to make the command look like an error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15759 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23No more states/initial.coq, instead coqtop now requires Prelude.voletouzey
For starting a bare coqtop, the recommended option is now "-noinit" that skips the load of Prelude.vo. Option "-nois" is kept for compatibility, it is now an alias to "-noinit". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-10Fixes bug #2857.aspiwack
Coqide used the wrong escape sequence to delimit coq phrases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15720 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-25Bug 2706: Coqide and layout that use special modifierspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15649 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-16Added abstration layer to goal display in CoqIDE, and cleaned partsppedrot
of the code altogether. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15623 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-16Fixing goal display when still focussing but no more goals.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15622 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-13Display the "unjustified" information returned by coqtop.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15620 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-13Fixes r15610 (A new status Unsafe in Interface).aspiwack
Two warnings had passed my sensors. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15619 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-12A new status Unsafe in Interface. Meant for commands such as Admitted.aspiwack
Currently : - only Admitted uses the Unsafe return status - the status is ignored in coqtop - Coqide sees the status but apparently doesn't use it for colouring (I'm not sure why, but then again, it's not as if I understood coqide's code or anything) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15610 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-10Adapting the IDE interface with the focussed display.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15579 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-29Various small display improvementppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15505 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-29Reversed message display order in CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15504 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-29Now CoqIDE separates answer and messages. This should hopefullyppedrot
be backward compatible... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15501 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-26Added the show_margin_right option to CoqIDEppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15496 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-26Fixing awkward copy & paste mechanism in CoqIDE.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15495 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-26Now CoqIDE auto-sets the printing width of the goal display.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15494 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-25Small code compaction and factoring in CoqIDE.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15491 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-24Cosmetic changesppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15489 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-24Made the message view of CoqIDE abstract.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15488 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-23Fixed cursor reset in CoqIDE backtrack.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15485 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-23Factorized bactracking code in CoqIDE. This fixes bug #2821 btw.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15484 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-23Fixing a potential bug of coqtop management in CoqIDE due to appedrot
careless exception catching. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15483 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-21Fixed #2821.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15471 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-21Fixing accelerator dynamic modification in CoqIDE.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15465 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-15Fix coqide vernac lexerpboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15442 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-13Fixing annoying autocompletion when deleting text.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15437 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-06-04Fixing #2803.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15419 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29Fixed an error display bug in CoqIDE.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15396 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-25Bugs revealed by playing with contribspboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15364 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-25Fix r15259 to get rid of bug 2783pboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15363 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-25Fixed #2769.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15362 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-23Rewritten the handling of coq sentence processing, hopefully beingppedrot
smarter and more asynchronous-friendly. Some aditional cleaning is needed to factorize other parts of the code, but this is a first milestone. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15359 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-23Fixed #2538 by adding an option to reset coqtop on tab switch, as suggested.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15355 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-23Revert copy/pasted function in to minilib thanks to clib.cmapboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15352 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-23Fixed #2782.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15351 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-23Reducing CoqIDE start option queries.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15344 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-22Minilib: Always add the Coq_config.dirs to xdg_dirs (again)letouzey
Sorry, my last commit in Minilib annihilated by mistake commit 15265. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15342 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-16Fixed bug #2781... (We hope so.)ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15335 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-16Trying to fix bug #2780, by short-circuiting the Gtk signals. A bit hackish.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15334 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-16Coqide: make some paths win32-compliantletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15332 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-15Coqide: minor formatting improvement of an error messageletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15329 85f007b7-540e-0410-9357-904b9bb8a0f7
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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-20 06:51:47 +0000