Re: finding the schwerpunkt

On Apr 23, 3:22 pm, h...@... wrote:
> Great ideas; before I weigh in---half my professional work in
> the '80s was on versions of Emacs, including at the low
> level both the Lisp Machine and TECO->Multics-> Gosling->Gnu
> families--- I'd like to ask if you plan on this editor being
> modal or not.  E.g. Emacs is generally non-modal, you're by
> default in self-insert mode and special commands start from
> that mode.  WYSIWYG editors in my experience work that way
> as well.  Whereas vi is by default in a command mode and
> when you want to modify text you switch to a mode for that.
>
> In the context of your concept:
>
>   The structure of this editor would reflect something of
>   the structure of my proof assistant in chapter 15 of TBoS.
>   Essentially there are four components.
>
>    1.  An area of text entry which can sustain the usual cut
>         and paste.
>
>    2.  A command line where expressions are evaluated
>         relative to the document.
>
>    3.  An area where (type/syntax) error messages are
>         displayed.
>
>    4.  A conventional Shen REPL in which programs and
>         plugins to the editor can be loaded.
>
> Area 1 would I assume be non-modal, and keystrokes or
> mousing could move you to the other areas, which I guess
> would be non-modal as well (you want to be able to copy text
> from area 3 at minimum).
>
> - Harold

Yes; you have it.  On the command line I do not want to follow the
Control-Meta-Alt-X approach I remembered of Emacs.  Totally
unnecessary to have that crud if you have a command line that is
modelled on a Shen REPL.  For instance here is a piece out of TBoS
from the proof assistant where in miniature you have this model
driving the proof.

?- S

1. P
2. (P => Q)
3. (Q => R)
4. (R => S)

> (fix =>-left)
========================= [1]
?- P

1. P
2. (P => Q)
3. (Q => R)
4. (R => S)

> hyp

Here the > functions as the command line and the expression (fix =>-
left) is actually a partial application which yieds a closure of the
type valid --> valid i.e. something that builds a valid proof.  The
proof assistant is set up so that the final term of the application is
the valid proof itself.  This is exactly the structure that the
program editor should have.

Mark

--

-- 
You received this message because you are subscribed to the Google Groups "Qilang" group.
To post to this group, send email to qilang@...
To unsubscribe from this group, send email to qilang+unsubscribe <at> googlegroups.com.
For more options, visit this group at http://groups.google.com/group/qilang?hl=en.