search

idris-hackers / idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.
GNU General Public License v3.0
268 stars 70 forks source link

Holes #173

Open defanor opened 10 years ago

defanor commented 10 years ago

It would be nice to have holes closer to those from agda2-mode, I think:

  1. Add C-c C-p and C-c C-n to navigate between holes quickly;
  2. Improve "refine":
    1. Make holes to be of form { }, so it'll save one RET and will not require from user to switch his focus/attention to the mini-buffer;
    2. Move the cursor to the first new hole after refinement (as well as after other hole-producing actions, probably), if there are any new holes.

Changing holes (and the filling process) that way also should help to avoid the bug with "yas--on-protection-overlay-modification: Exit the snippet first!", which appears on emacs 24.3.1 after case-splitting, refinement or creating an initial pattern, when trying to remove the whole line or to do something similar (say, C-c C-s and then C-c C-c on an argument leads to such an error here).

david-christiansen commented 10 years ago

Agda's holes are quite nice. But I don't think they're going to happen for idris-mode in the near future, because they require substantial support from the compiler, and the Idris compiler is focused around metavariables. The interaction is a bit different. We might want to support both at some time in the future, but for now, we do not.

On the other hand, you are pointing out a legitimate bug relating to the yasnippet interaction. I just checked that it is in fact a problem. I can't immediately see what the problem is though - I imagine that yasnippet needs to have some state cleaned up that I'm not cleaning up. For now, try turning off the yasnippet integration in customize, and if I can't figure out how to make it work right, then I'll just remove the integration.

defanor commented 10 years ago

What kind of support do they require? I thought about it as a matter of representation (and a little text parsing) only: keeping it as it was in files (say, {-func-}?mv1), while showing/editing {func}mv1, refining func when the hole is active, and skipping { and }mv on C-f and C-b.

And thanks for the advice, it's nicer now.

david-christiansen commented 10 years ago

For holes to really work, you should be able to do things like type check an expression in the context of a hole to see if it matches and the like. We could do some kind of fake hole support with what we have now, I suppose, but it'd be a bit creaky. I'll certainly leave the issue open, as it's a legit thing that would be nice to do, but I don't plan on hacking on it atm.

Patches are certainly welcome, though!

defanor commented 10 years ago

Here is some basic holes support. Will make a pull request when case-splitting fixes will be accepted in Idris-dev, and test/debug until that. Most likely will also add insertion of terms too: if "refine" fails, try to replace the hole with expression, and if it typechecks - keep it that way; otherwise - keep the hole and probably show an error message, though not sure about the latter. Oh, and replacing of "?" with holes on load should be added too.

defanor commented 10 years ago

Added everything described above, testing now; need to fix a few more metavars-related functions, but it should be easy. Pushing new changes to https://github.com/defanor/idris-mode/tree/holes.

david-christiansen commented 10 years ago

@defanor What's the status on this hole support?

defanor commented 10 years ago

@david-christiansen Now the thing that blocks me is refinement time: it should be fast for comfortable editing, but it is too slow. It takes ~4 seconds to refine something in the end of an average-sized file (500-600 LOC) in the usual way, and ~8 to do that with a hack that adds this proposed functionality; and takes <1 second for little files. It also takes the same ~4 seconds to just load such a file, so I think the loading should be optimized first. Also there's a loading-related bug (at least in the version with holes, probably I've introduced it somehow): sometimes it does not load enough. So, I was going to check it all in master, try to debug, and create new issues, but unfortunately was too lazy lately.

david-christiansen commented 10 years ago

No worries. Just wanted to make sure good work wasn't getting lost.

Probably we need to start caching the already-elaborated beginning of files to make this really nice at the ends of files. Right now, we can stop loading at a particular point - we probably need to be able to just "unwind' the state to the last unedited bit without reloading everything.

2014-06-16 9:46 GMT+02:00 defanor notifications@github.com:

@david-christiansen https://github.com/david-christiansen Now the thing that blocks me is refinement time: it should be fast for comfortable editing, but it is too slow. It takes ~4 seconds to refine something in the end of an average-sized file (500-600 LOC) in the usual way, and ~8 to do that with a hack that adds this proposed functionality https://github.com/idris-lang/Idris-dev/issues/1307; and takes <1 second for little files. It also takes the same ~4 seconds to just load such a file, so I think the loading should be optimized first. Also there's a loading-related bug (at least in the version with holes, probably I've introduced it somehow): sometimes it does not load enough. So, I was going to check it all in master, try to debug, and create new issues, but unfortunately was too lazy lately.

— Reply to this email directly or view it on GitHub https://github.com/idris-hackers/idris-mode/issues/173#issuecomment-46149512 .