Subject: Re: finding the schwerpunkt
Date: Monday 23rd April 2012 15:00:53 UTC (over 4 years ago)
On Apr 23, 3:22 pm, h...[email protected] 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) =========================  ?- 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 [email protected] To unsubscribe from this group, send email to [email protected] For more options, visit this group at http://groups.google.com/group/qilang?hl=en.