aboutsummaryrefslogtreecommitdiff
path: root/ide
AgeCommit message (Collapse)Author
2013-10-22Wg_Find: regex + case insensitive find/replace supportgareuselesinge
It uses Str, hence it also supports captures \(..\) and \1 .. \n git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16904 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22wg_Detachable: move out of wg_Commandgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16903 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22Wg_Commands: fix warning "widget not within a GtkWindow"gareuselesinge
The constructor was calling indirectly grab_default that requires the widget to be anchored. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16902 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22Wg_Commands: when detached display the buffer namegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16901 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22CoqIDE: display in the errors window also the slaves statusgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16900 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22wg_Commands: smaller icons in tabsgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16897 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22ideutils: support custom size for stock iconsgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16896 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-11CoqIDE: make error background configurablegareuselesinge
#FFCCCC is quite dark on some beamers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16881 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-11CoqIDE: single underline for errorsgareuselesinge
The double underline has some bugs, sometimes the lower line is not correctly cleared. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16875 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-10CoqIDE: error reporting fixedgareuselesinge
Many things were wrong. Error tags were deleted by mistake, the screen was recentered on `INSERT using the wrong function (that cause some horizontal scrolling even if it was not needed), the cursor not advanced to the end of the wrong sentence. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16874 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-10Document: undoing inside a focused zone does not require unfocusinggareuselesinge
To test this fake_ide has also been improved with the GOALS command. As for CoqIDE, ADDing a sentence does not force its evaluation. The "advance 1 sentence" button is an ADD + GOALS. If one of the ADDed sentences is wrong, GOALS receives the error. The GUI then backtracks to a safe state id (sent by Coq). fake_ide has GOALS (asserts that the goals call was OK) and FAILGOALS to assert it fails and backtrack to a valid state. see unfdo022.fake. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16873 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-10CoqIDE: ported to Documentgareuselesinge
The code is simpler, but there is still room for improvement. In particular find_id (implemented in both coqOps and fake_id) should be part of Document. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16872 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-10CoqIDE: move cmd_stack to a separate module: Documentgareuselesinge
The idea is to move the logic related to document handling to a separate module that can be tested by fake_ide too. CoqOps should "only" interface Document with the GtkTextBuffer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16870 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-10CoqIDE: a comment is not a sentencegareuselesinge
This simplifies the whole document business: the document on the Coq side has the very same nodes as the CoqIDE document, there are no "fake" nodes in the CoqIDE document to be skipped over. We keep the comment tag stamped by the coq_lexer module, since we may want to allow edits in there without telling Coq (as proof general does). Not implemented yet, but doable thanks to the comment tag. Pierre Boutillier suggested that this makes back-1-sentence ugly, since it moves the cursor far away if the sentence begins with a comment. While this is true, *today*, there is no need to undo the last sentence with the button to edit the text. One can just move the cursor where he likes and edit. In this case the sentence is backtracked automatically and the cursor is left where it is. Hence considering initial comments as part of the following sentence should not be an usability issue anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16866 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07CoqIDE: fix jumpig out of a focused proofgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16857 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-07CoqIDE: cStack -> Documentgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16856 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-03CoqIDE: when jumping to an error also move the cursorgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16842 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01CoqIDE: when checking the whole document, center script view on errorgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16835 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01CoqIDE: fixed advance_until wrt unfocusinggareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16834 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01CoqIDE: do not print cmd_stack too oftengareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16831 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01CoqIDE: do not fail hard if a message is asynchronousgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16826 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-01CoqIDE: fix reset initialgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16824 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30CoqIDE: use #present to raise error windowgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16823 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30Backtrace.record_backtrace in CoqIDE toogareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16822 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30CoqIDE: wg_Tooltip removed, new tooltip handlinggareuselesinge
- tooltips are attached to sentences - to find the tooltip text one goes back until the first start of sentence mark, finds the corresponding sentence and displays the tooltip - focused editing does not invalidate tooltips this way, since the text, its tags and marks is moved around consistently git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16821 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30ideutils: stock_to_widget was ignoring the ~size argumentgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16818 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30wg_Command: detachable, less "from the 80s", query panegareuselesinge
- Tabs have labels derived from the query (e.g. "About eq_ind" will have "eq_ind" as its label, that is better than "Page 1" ;-) - Tabs have a [x] close icon - Icon to create a new tab in in the notebook - Dispotically grab the F1 key to open/close the query pane (alt-esc is grabbed by windows managers these days) - Esc hides the query pane (like the search pane) - F1 puts a detached query pane in front - Tab switches from the combo-box to the entry on its right - Detaching is taken-over, and the query pane is reparented in a regular window that can be resized - A detached query pane can be put back by closing the window git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16817 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30wg_Session: fix copy/paste of tagged textgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16816 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-30CoqIDE ported to the revides protocolgareuselesinge
- the zone to be edited is now between the marks start_of_input and stop_of_input - when -debug is given, the edit zone is underlined - the cmd_stack is focused/unfocused according to the new protocol - read only tag resurrected and used to block the "Qed" ending a focused zone git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16814 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-13When Coq is reset-initialed by CoqIDE, do reset jobs countersgareuselesinge
Coq is not going to send any feedback message for the brute-force canceled jobs, given that the process was killed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16780 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-13fix error reporting window size calculationgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16779 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-13CoqIDE: new async error reporting window and slaves statusgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16778 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-13Do no compage wg_Notebook terms with (=)gareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16775 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-12CoqIDE: show number of proofs being checked in backgroundgareuselesinge
good test: Nijmegen/QArithSternBrocot/Zaux.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16773 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-06Moving Searchstack to CStack, and normalizing names a bit.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16765 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-04More robust argument setter in CoqIDE. It does not crash anymore on badppedrot
arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16761 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-20CoqIDE: fixed detection of edits in the locked zonegareuselesinge
Trying to understand if the edit concernes the processed zone from the begin_user_action callback was a bad idea, the callback cannot reliably know where the edit takes place (E.g. insert mark means nothing: one can copy from the insert point but paste elsewhere). The callbacks delete_range and insert_text do know where the edit is and can ask coq to backtrack if needed. If coq is busy, the user action is cancelled (the locked zone cannot be unlocked). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16715 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-19Modulification and removing of structural equality in Stateid.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16705 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-19Tooltips can be augmented with custom widgets, still not clickablegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16701 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-12Setting tooltip font monospace.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16700 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-11Automatic backtracking if locked zone is editedgareuselesinge
That is pretty tricky, and is not as nice I would like for to_process text (that is still considered as locked). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16698 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-09Adding the processed tag to comments in CoqIDE.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16693 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Gtk check_buttons do have a labelgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16687 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Add a (very minimal) Proof General mode to CoqIDEgareuselesinge
documentation available in the help menu git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16685 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08stm: (initial) support for -coq-slavesgareuselesinge
Stm contains many TODO items to improve the thing, but it should be already possible to play with it (but not use it in production). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16684 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Coqide ported to STMgareuselesinge
Main changes for STM: 1) protocol changed to carry edit/state ids 2) colouring reflects the actual status of every span (evaluated or not) 3) button to force the evaluation of the whole buffer 4) cmd_stack and backtracking completely changed to use state numbers instead of counting sentences 5) feedback messages are completely asynchronous, and the whole protocol could be made so with a minor effort, but there is little point in it right now. Left as a future improvement. Missing bit: add sentence-id to responses of interp command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16677 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-08Fixing a warning in CoqIDE compilation.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16668 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-30Granting wish #1781:ppedrot
Parenthesis matching on click in all term displays. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16643 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-27Protecting every call to current_term in CoqIDE so that callbackppedrot
will not raise an exception if there is no opened tab. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16637 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-07-27Added a way to change dynamically coqtop arguments in CoqIDE.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16636 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 20:39:22 +0000