Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Allow multiple coq buffers to opened at the same time #66

Open
wants to merge 12 commits into
base: pathogen-bundle
Choose a base branch
from
Open

Allow multiple coq buffers to opened at the same time #66

wants to merge 12 commits into from

Commits on Aug 22, 2019

  1. improve coq error handling 

    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.
    @dwarfmaster
    dwarfmaster authored and Kyle Stemen committed Aug 22, 2019
    Configuration menu
    Copy the full SHA
    6719ee5 View commit details
    Browse the repository at this point in the history

  2. no more python errors on Qed with subgoals

    @dwarfmaster
    dwarfmaster authored and Kyle Stemen committed Aug 22, 2019
    Configuration menu
    Copy the full SHA
    b2288de View commit details
    Browse the repository at this point in the history

  3. Allow multiple coq buffers to opened at the same time 

    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
    Kyle Stemen authored and Kyle Stemen committed Aug 22, 2019
    Configuration menu
    Copy the full SHA
    ec0d19f View commit details
    Browse the repository at this point in the history

  4. Handle errors where coqtop reports it failed in state 0 

    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.
    Kyle Stemen authored and Kyle Stemen committed Aug 22, 2019
    Configuration menu
    Copy the full SHA
    848e33e View commit details
    Browse the repository at this point in the history

  5. Rewind the first time new text is inserted in the processed region 

    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.
    Kyle Stemen authored and Kyle Stemen committed Aug 22, 2019
    Configuration menu
    Copy the full SHA
    a58f4e9 View commit details
    Browse the repository at this point in the history

  6. Fix bullet handling 

    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.
    Kyle Stemen authored and Kyle Stemen committed Aug 22, 2019
    Configuration menu
    Copy the full SHA
    c4e4b98 View commit details
    Browse the repository at this point in the history

  7. Fix highlight ranges for files with non-ascii characters 

    Use byte offsets for the highlight ranges (sent, checked, error, and warning)
instead of unicode characters offsets.

Also fix python 2 support.
    Kyle Stemen authored and Kyle Stemen committed Aug 22, 2019
    Configuration menu
    Copy the full SHA
    ff53079 View commit details
    Browse the repository at this point in the history

  8. If there are no focused goals, print the unfocused goals 

    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.
    Kyle Stemen authored and Kyle Stemen committed Aug 22, 2019
    Configuration menu
    Copy the full SHA
    49f3382 View commit details
    Browse the repository at this point in the history

  9. Send Coq statements on a background thread 

    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.
    Kyle Stemen authored and Kyle Stemen committed Aug 22, 2019
    Configuration menu
    Copy the full SHA
    177540e View commit details
    Browse the repository at this point in the history

  10. Show the warning highlight in the correct places in 8.7

    Kyle Stemen authored and Kyle Stemen committed Aug 22, 2019
    Configuration menu
    Copy the full SHA
    c79c217 View commit details
    Browse the repository at this point in the history

  11. Fix syncing the colors of a buffer when it is open in multiple tabs

    Kyle Stemen authored and Kyle Stemen committed Aug 22, 2019
    Configuration menu
    Copy the full SHA
    01a62bf View commit details
    Browse the repository at this point in the history

  12. Scroll the goal and info buffers back to the top whenever they change

    Kyle Stemen authored and Kyle Stemen committed Aug 22, 2019
    Configuration menu
    Copy the full SHA
    727ecaf View commit details
    Browse the repository at this point in the history