Comments (3)
This is a really cool features and I'd love to have this. Any ideas as to how one might implement this? I had a few ideas:
-
Use
coqtop
'sDiffs
option.- So of course the first thing I tried was to just evaluate
Set Diffs "on".
in the main buffer, and then seeing if it did anything. No joy. Is it clear if this is a limitation of Coqtop's XML protocol? - Of course, the downside to this is that it won't be backwards compatible---this won't be available to those working with older versions of Coqtop before this feature was available.
- So of course the first thing I tried was to just evaluate
-
Use vim's builtin diff features.
- I tried manually creating a second buffer, copying the goal buffer state there, taking a step in the main buffer, and then using
:diffthis
on both buffers. The results are kind of patchy. - I could experiment more and try to toy with the different
diffopt
settings and algorithms, but what can be done will ultimately be limited by vim's functionality. I haven't had a chance to look intodiffexpr
or what it can do for us. - That being said, this is also the most straightforward solution---just keep a hidden "shadow" goal buffer around that lags a step behind, and allow the user to turn on diffing between that and the actual goal buffer, showing only the goal buffer with the highlighted terms. It'll be difficult to see missing terms, but it at least show something. The shadow buffer can just be repopulated using the undo history of the goal buffer.
- I tried manually creating a second buffer, copying the goal buffer state there, taking a step in the main buffer, and then using
-
Use Python to implement the algorithm described in the reference manual.
- If we can get the Python side to mark the highlight regions, we could pretty easily intercept the messages to and from Coqtop and do it from there. This can be done every time the goal buffer is updated.
- This is also the most easily powerful option, and can also be used to implement cool features beyond what other IDEs have.
- Probably also requires the most (invasive?) changes and work.
from coqtail.
I might even take a dip into #87 just to learn about how highlight regions work before trying anything here. I've mostly taken syntax highlighting for granted and it would be useful to learn about it by hacking on it.
from coqtail.
I had something in mind along the lines of option 1. When you enable diffs the XML protocol starts including messages with information about what changed in the proof state, which currently Coqtail ignores so it’s not visible. We’d just have to parse this information and then pass it to Vim to highlight with the appropriate color.
Option 2 is an interesting idea for a fallback for older versions of Coq without diff support. I’ve never really used Vim’s diffing capabilities much so I’d need to experiment and see what’s possible there.
Option 3 could potentially also work for older versions, but it does seem the most complicated. If Vim alone isn’t able to produce useful diffs then maybe some combination of 2 and 3 (using Python to preprocess the goal buffers a bit then passing it to Vim to actually do the Myers diff) would be best.
As for #87, I’ve started working on that a bit in a local branch. If you’re interested I could push it, you could fork it and open a pull request, and we could collaborate on it.
from coqtail.
Related Issues (20)
- Anonymous implicit generalization is not recognized HOT 3
- Register command is not recognized
- Requires Python 3.6 error in Neovim HOT 2
- Comments with leading * cannot be joined using J HOT 1
- Formatting comments (e.g. using gqq) does not work correctly HOT 1
- coqtail hangs on first command with `-noinit`
- Plugin does not load; WSL2 Ubuntu HOT 2
- Set Firstorder Solver idtac. HOT 1
- Feature Request: option to omit proofs when scripting (auto-admit) HOT 1
- Breaking with after/syntax directory HOT 5
- [Syntax] Is there a lack of support for math symbol shortcuts? HOT 2
- Detach panels from neovim instance HOT 3
- Unexpected error when debugging Unicoq HOT 2
- Coqtail doesn't recognize the option `-arg "-w all"`
- Coqtail does not officially support your version of Coq (8.19.0) HOT 7
- Feature: better support for dune HOT 4
- :Coq Set Printing Width not persistent HOT 1
- Comments inside of strings are not highlighted correctly
- Error on some large operations HOT 4
- Wrong syntax highlight for `Structure` HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from coqtail.