Allow multiple coq buffers to opened at the same time #66
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This was referenced Sep 22, 2017
\o/ |
bluelightning32
force-pushed
the
pathogen-bundle
branch
2 times, most recently
from
dc87938 to
37a28f7
Compare
bluelightning32
force-pushed
the
pathogen-bundle
branch
4 times, most recently
from
c4e8f50 to
c6b37a3
Compare
bluelightning32
force-pushed
the
pathogen-bundle
branch
3 times, most recently
from
f2beea5 to
1f7faaf
Compare
bluelightning32
force-pushed
the
pathogen-bundle
branch
from
c39f121 to
720a0e8
Compare
|
Coquille with this PR seems to work fine. I saw few errors requiring restart, but they don't block the workflow completely and probably may be fixed later. Does anybody plan to merge it? Or maybe is there a coquille fork with it applied? |
|
I pretty much gave up on getting this merged. You can use my fork, bluelightning32:pathogen-bundle. |
|
Thanks! Could you please enable issues for this repository? I don't feel brave enough to fix possible errors but I am ready to report them. |
|
Done. I won't have time to work on issues for the next few weeks, but go ahead and file them. I am interested in supporting this project. |
|
Should be rebased on top of the master. |
Python no longer fails for most of coq errors. When sending an invalid argument during a proof, an error is displayed in the info box, but the cursor moves over the instruction : it may not be intuitive. Furthermote, moving to a Qed like that creates another python error.
1. Allow multiple instances of coqtop to run for different coq source buffers. 2. Support python 2 or 3. 3. Parse default coqtop args from _CoqProject 4. Allow multiple line ranges for the checked, sent, and error regions. This shows when coq processes statements out of order. 5. Fix parsing comments longer than 995 lines 6. Fix parsing strings over 995 lines 7. Add a utility to capture protocol traces from coqide 8. Use better default colors when the background is dark
If the error is serious enough, coqtop reports it happened in state 0. It is not possible to revert to state 0, because that is before the Init call. So skip the revert completely if coqtop says state 0.
The CursorMovedI event is triggered when new text is inserted, which is better than InsertEnter that would resync the buffer on the next insert. Also fix an off by one error around changing the last character in a statement, or jumping to the last character in a statement.
1. Allow multi character bullets, like -- 2. Do not treat the space directly after the bullet as part of the bullet. This is important so that when a new statement is added directly after the bullet, the bullet is not rewound.
Use byte offsets for the highlight ranges (sent, checked, error, and warning) instead of unicode characters offsets. Also fix python 2 support.
Match the coqide's goal message format. This is important for indicating whether an unfocused goal needs to be focused or the proof is done.
For the coq to cursor command, send the statements on a background thread while the main thread redraws the screen. This lets Coq accept multiple commands per screen redraw. The background thread is terminated after all the statements are sent.
bluelightning32
force-pushed
the
pathogen-bundle
branch
from
eb06e85 to
727ecaf
Compare
|
I rebased it on top of the pathogen-bundle. Is that what you meant? |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
shows when coq processes statements out of order.