aboutsummaryrefslogtreecommitdiff
path: root/ide/coqOps.ml
AgeCommit message (Collapse)Author
2016-03-18Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-15CoqIDE is more resilient to initialization errors.Pierre-Marie Pédrot
We force the STM to finish after the initialization request so as to raise exceptions that may have been generated by the initialization process. Likewise, we simply die when the initialization request fails in CoqIDE instead of just printing an error message. This is the fix for the underlying issue of bug #4591, but it does not solve the bug yet.
2016-02-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-20Fixing bug #4540: CoqIDE bottom progress bar does not update.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-10-30Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-30Fix typo.Guillaume Melquiond
2015-09-20Rich printing of CoqIDE protocol failure.Pierre-Marie Pédrot
2015-09-20Rich printing of messages.Pierre-Marie Pédrot
2015-09-20Adding rich printing primitives.Pierre-Marie Pédrot
2015-09-17Merge branch 'v8.5' into trunkMaxime Dénès
2015-09-15Removing a warning in CoqOps.Pierre-Marie Pédrot
2015-08-26Replacing old-style preferences in CoqIDE.Pierre-Marie Pédrot
There is no remaining global preference record anymore, every preference is now defined in the new event-based style.
2015-08-16Using the new preference mechanism for colors in CoqIDE.Pierre-Marie Pédrot
A lot of legacy code has been removed in the process in favour of signal-based interactions.
2015-08-16Turning CoqIDE preferences into new style.Pierre-Marie Pédrot
Some old style references remain because all type converters are not implemented yet.
2015-07-11CoqIDE: recenter on backtrack (Close: #4277)Enrico Tassi
2015-06-16Fix by Enrico on CoqIDE not locating errors anymore since 550da87456a.Hugo Herbelin
2015-04-02CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)Enrico Tassi
No "read-only" terminator. If no terminator is present the UI complains. If the terminator is different, STM warns but continues. The STM warns that the "check the document" button will not honor the terminator change, and what to do to avoid that. Technically, one cannot turn (a posteriori) an axiom into a theorem and vice versa. Could be done, but not with a small patch.
2015-03-11CoqIDE: fix tag colors to support superposing unsafe and partialEnrico Tassi
Admitted (like Qed) can be "partially executed", but is also unsafe.
2015-03-11CoqIDE: do not lose tag on Qed ending focused proofEnrico Tassi
2015-02-25CoqIDE: correclty unfocus (remove all tags) when jumping out of a proofEnrico Tassi
2015-02-15Fixing bug #4037.Pierre-Marie Pédrot
2015-01-29Made the CoqIDE progress gutter clickable.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2015-01-05Implementing a segment-viewer in CoqIDE.Pierre-Marie Pédrot
This allows a nifty display of the current state of the document through a dedicated progress bar. Also closes bug #3764.
2014-12-17CoqIDE: better messagesEnrico Tassi
2014-11-27Feedback: API cleaned up, documented and made user extensibleEnrico Tassi
2014-09-09IDE: escape popup text (close: 3600)Enrico Tassi
2014-08-12Quick fix for avoiding infinitely many respawning and Warning "CoqHugo Herbelin
died" when coqtop or coqtopide.cmxs are in inconsistent state.
2014-08-05STM: code restructured to reuse task queue for tacticsEnrico Tassi
2014-06-25all coqide specific files moved into ide/Enrico Tassi
lib/interface split into: - lib/feedback subscribe-based feedback bus (also used by coqidetop) - ide/interface definition of coqide protocol messages lib/pp structured info/err/warn messages lib/serialize split into: - lib/serialize generic xml serialization (list, pairs, int, loc, ...) used by coqide but potentially useful to other interfaces - ide/xmlprotocol serialization of protocol messages as in ide/interface the only drawback is that coqidetop needs -thread and I had to pass that option to all files in ide/
2014-03-26CoqIDE: better error reporting for Qed on incomplete proofEnrico Tassi
2014-03-12Stm: smarter delegation policyEnrico Tassi
Stm used to delegate every proof when it was possible, but this may be a bad idea. Small proofs may take less time than the overhead delegation implies (marshalling, etc...). Now it delegates only proofs that take >= 1 second. By default a proof takes 1 second (that may be wrong). If the file was compiled before, it reuses the data stored in the .aux file and assumes the timings are still valid. After a proof is checked, Coq knows how long it takes for real, so it wont predict it wrong again (when the user goes up and down in the file for example). CoqIDE now sends to Coq, as part of the init message, the file name so that Coq can load the .aux file.
2014-01-30STM + CoqIDE: stop_worker message and UIEnrico Tassi
2014-01-30STM: tell the user if the master is recomputing states validated by workersEnrico Tassi
When the worker fails, the master may need to recompute some states the worker has already validates. In this case they are colored accordingly.
2014-01-06CoqIDE: do not unfocus if not needed on errors (closes: 3197)Enrico Tassi
2013-12-24CoqIDE: new feedback "incomplete" to signal partial QedEnrico Tassi
2013-11-27CoqIDE: show error message for parsing errorsEnrico Tassi
2013-10-31CoqIDE: scroll to the right position if there is an interp errorgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16962 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-24CoqIDE: fix coloring bug when jumping back to the first phrasegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16928 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-22CoqIDE: do not try to backtrack to a dummy idgareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16906 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-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-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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 06:26:51 +0000