Prepare merge #1
Closed
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
Fixed make-lemma Added jump-to-def TODO 2 get evil leader working again proof search next add jump-to-def next 3 load-forward-line and load-backward-line. These are for "load-to-here" functionality to execute a partial file ... probably a lot more... Newbie to Idris, elisp and proving things
idris2-jump-to-def
choose. Also handles source files missing more gracefully.
isn't on a symbol when invoked. Created idris2-jump-to-def-same-window which is the same as idris2-jump-to-def, but will use the existing window when jumping to the new file position.
specified in customization. Did some whocall stuff (not implemented in Idris2 currently)
idris2-sources looking for source. Added xref pushes for who-calls
changes which I were made so long ago I don't remember what they were for anymore.
Only refresh ELPA cache if there's at least one package we need to in…
gallais
force-pushed
the
prepare-merge
branch
from
e783dfd
to
d09a588
Compare
And also revert some of the deletions made in idris2-mode. These should never have been stubbed out: it's Idris2's role to handle even commands that have not been implemented yet.
idris-thing-at-point is nowadays happy to open a prompt
gallais
force-pushed
the
prepare-merge
branch
from
4ce94ac
to
cf9f91b
Compare
|
Did this ever get merged back into idris-mode? I am a bit confused which mode to use. I commented on an issue in the Doom Emacs repository that you can find here: |
7 tasks
|
These days I'm using |
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.
I'm giving up on the subtle approach and
sedThis won't preserve the history of the patches but trying to do so creates