aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqOps.ml
Commit message (Collapse)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\
| * Use the actual location of an error in the error pane (bug #4169).Gravatar Guillaume Melquiond2016-05-09
| | | | | | | | | | | | | | A "sentence" includes all the blank lines and all the comments that precede a command. So its starting location might be far from any error it contains. This patch changes error reporting so that it relies on the location of errors rather than the location of erroneous sentences.
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-18
|\|
| * CoqIDE is more resilient to initialization errors.Gravatar Pierre-Marie Pédrot2016-03-15
| | | | | | | | | | | | | | | | | | | | 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.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-21
|\|
| * Fixing bug #4540: CoqIDE bottom progress bar does not update.Gravatar Pierre-Marie Pédrot2016-02-20
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-30
|\|
| * Fix typo.Gravatar Guillaume Melquiond2015-10-30
| |
* | Rich printing of CoqIDE protocol failure.Gravatar Pierre-Marie Pédrot2015-09-20
| |
* | Rich printing of messages.Gravatar Pierre-Marie Pédrot2015-09-20
| |
* | Adding rich printing primitives.Gravatar Pierre-Marie Pédrot2015-09-20
| |
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-09-17
|\|
| * Removing a warning in CoqOps.Gravatar Pierre-Marie Pédrot2015-09-15
| |
* | Replacing old-style preferences in CoqIDE.Gravatar Pierre-Marie Pédrot2015-08-26
| | | | | | | | | | There is no remaining global preference record anymore, every preference is now defined in the new event-based style.
* | Using the new preference mechanism for colors in CoqIDE.Gravatar Pierre-Marie Pédrot2015-08-16
| | | | | | | | | | A lot of legacy code has been removed in the process in favour of signal-based interactions.
* | Turning CoqIDE preferences into new style.Gravatar Pierre-Marie Pédrot2015-08-16
|/ | | | | Some old style references remain because all type converters are not implemented yet.
* CoqIDE: recenter on backtrack (Close: #4277)Gravatar Enrico Tassi2015-07-11
|
* Fix by Enrico on CoqIDE not locating errors anymore since 550da87456a.Gravatar Hugo Herbelin2015-06-16
|
* CoqIDE: simpler way of reopening/reclosing a proof (Close: 4168)Gravatar Enrico Tassi2015-04-02
| | | | | | | | | | | 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.
* CoqIDE: fix tag colors to support superposing unsafe and partialGravatar Enrico Tassi2015-03-11
| | | | Admitted (like Qed) can be "partially executed", but is also unsafe.
* CoqIDE: do not lose tag on Qed ending focused proofGravatar Enrico Tassi2015-03-11
|
* CoqIDE: correclty unfocus (remove all tags) when jumping out of a proofGravatar Enrico Tassi2015-02-25
|
* Fixing bug #4037.Gravatar Pierre-Marie Pédrot2015-02-15
|
* Made the CoqIDE progress gutter clickable.Gravatar Pierre-Marie Pédrot2015-01-29
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Implementing a segment-viewer in CoqIDE.Gravatar Pierre-Marie Pédrot2015-01-05
| | | | | | | This allows a nifty display of the current state of the document through a dedicated progress bar. Also closes bug #3764.
* CoqIDE: better messagesGravatar Enrico Tassi2014-12-17
|
* Feedback: API cleaned up, documented and made user extensibleGravatar Enrico Tassi2014-11-27
|
* IDE: escape popup text (close: 3600)Gravatar Enrico Tassi2014-09-09
|
* Quick fix for avoiding infinitely many respawning and Warning "CoqGravatar Hugo Herbelin2014-08-12
| | | | died" when coqtop or coqtopide.cmxs are in inconsistent state.
* STM: code restructured to reuse task queue for tacticsGravatar Enrico Tassi2014-08-05
|
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
| | | | | | | | | | | | | | | | | | | | 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/
* CoqIDE: better error reporting for Qed on incomplete proofGravatar Enrico Tassi2014-03-26
|
* Stm: smarter delegation policyGravatar Enrico Tassi2014-03-12
| | | | | | | | | | | | | | | | | | | | 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.
* STM + CoqIDE: stop_worker message and UIGravatar Enrico Tassi2014-01-30
|
* STM: tell the user if the master is recomputing states validated by workersGravatar Enrico Tassi2014-01-30
| | | | | | When the worker fails, the master may need to recompute some states the worker has already validates. In this case they are colored accordingly.
* CoqIDE: do not unfocus if not needed on errors (closes: 3197)Gravatar Enrico Tassi2014-01-06
|
* CoqIDE: new feedback "incomplete" to signal partial QedGravatar Enrico Tassi2013-12-24
|
* CoqIDE: show error message for parsing errorsGravatar Enrico Tassi2013-11-27
|
* CoqIDE: scroll to the right position if there is an interp errorGravatar gareuselesinge2013-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16962 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: fix coloring bug when jumping back to the first phraseGravatar gareuselesinge2013-10-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16928 85f007b7-540e-0410-9357-904b9bb8a0f7
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: do not try to backtrack to a dummy idGravatar gareuselesinge2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16906 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: display in the errors window also the slaves statusGravatar gareuselesinge2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16900 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoqIDE: error reporting fixedGravatar gareuselesinge2013-10-10
| | | | | | | | | 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
* CoqIDE: ported to DocumentGravatar gareuselesinge2013-10-10
| | | | | | | | 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
* CoqIDE: move cmd_stack to a separate module: DocumentGravatar gareuselesinge2013-10-10
| | | | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-28 04:40:38 +0000