search

david-christiansen / jonprl-mode

An Emac major mode for writing JonPRL code
8 stars 5 forks source link

display forms #20

Open jonsterling opened 9 years ago

jonsterling commented 9 years ago

This is an "exploratory" issue, where hopefully I can learn what's possible (or practical) with Emacs.

Currently, I know how to replace an operator name with a symbol (and I just do this locally in my emacs configuration using pretty-mode; for some use-cases prettify-symbols-mode would also work).

However, what I am curious about is whether it is possible to have something more like Nuprl's editor, where a term gets displayed in "concrete" form (i.e. (Π x : A) B instead of fun(A; x. B)), and there'd be these little editable slots.

Is this super hard to do in Emacs?

ghost commented 9 years ago

By editable slots, do you mean like you click on the rendered display form and it allows you to edit it in underlying ASCII form? I think the way you might want to do this is with overlays (see ov.el for example).

david-christiansen commented 9 years ago

This would be medium-difficult to do in Emacs. The actual display part is fairly easy to do, but I'd prefer not to write a real parser if I can avoid it. JonPRL could make this a lot easier by providing a source-location-annotated AST to editors, kind of like how idris-mode, agda-mode, and structured-haskell-mode work.

jonsterling commented 9 years ago

OK; I think we should start by adding what is necessary to JonPRL itself, so that the emacs side may be as easy as possible.

david-christiansen commented 9 years ago

It might be worth thinking about whether Nuprl-style display forms are the right solution, as well. They do have a number of downsides:

  1. The command necessary to type something has little to do with how it looks in the source file
  2. Structure editors are difficult to implement in such a way that they aren't horrible to use
  3. It increases the unfamiliarity of the system relative to others that someone might have used - one of the goals of JonPRL is to be more easily runnable and accessible than Nuprl, if I've understood right.

It might make more sense to just define an ordinary parser and syntax for the built-in forms, or to pick a notation for ABT's that's more practical in practice, just like Lispers have learned to work effectively with sexprs.