EditorDoc Sections Nuprl Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The nuprl_sfa interface to Nuprl (Nuprl4 now, Nuprl5 later)

While these documentation pages do not constitute a tutorial or an exposition for the main ideas, one can get some idea of the capabilities from reading through them. Start at "How to use this interface".

Notable features:

1. This editor is powerful and extensible. Indeed, it was built by bootstrapping from the Nuprl editor primitives, through the creation of: ML code for both inference and editing utilities; operator definitions (used as macros); term-display methods; bindings of editor-primitive combinations to keyboard commands; documentation objects; menus of active button-like expressions; and examples. The ML code constitutes the bulk of these sources.
 
2. The structure of Terms used for proofs, program code, definitions, etc. is largely independent of how they are to be displayed. Display is user-specifiable and fairly flexible, exploiting a number of methods standard in informal notation. Although many operations on terms, such as making inferences, are mostly independent of terms' appearance, interactive structure-editing is highly influenced by how terms are displayed. That is, the editing operations are implicitly parameterized by various features of user-selected display, and editing is basically WYSIWYG. (And yet, the bulk of defined editing operations is still display-independent.)
 
3. While one could think of Nuprl Terms as parse trees generated from a very simple grammar, there would be little reason to do so, since, on one hand, the grammar is rather degenerate, and on the other, the strings one parsed would, it turns out, not be seen by the normal user; indeed, there is typically, though not necessarily, some user-specified ambiguity in the display of terms, so there is no certain path from the appearance to the underlying term. There is no significant "grammar" per se; any term can appear as an immediate subterm of any operator that takes subterms. One consequence is that rather than editing terms top-down or bottom-up, one may edit them "thought-first". Another is that operator definitions serve not only as mathematical notations, but also as system macros.
 
4. Naturally, there are hyperlinks between objects of the system (the content of an object is expressed as a term, and objects have names).
 
5. The development of new material by imitation of existing material is facilitated in various ways. One finds something that approximates what one wants, then adapts it.
 
6. One can attach "actions" to terms which are performed in response to various user gestures such as mouse-clicking on a term. In addition to a few editing operations, one can execute arbitrary user-written ML code this way. Indeed, the bulk of this editor is written in ML.
 
7. From a "meaningful" non-primitive expression of the system one can normally track down the sources that give it its meaning, such as operator definitions (macros), and definitions of ML globals (in the standard "prelude"; in the editor; in user defined code). And from a term instance in the editor one can find the sources that make it display that way.
 
8. Various methods have been incorporated for finding documentation pertinent to a given term instance, such as what keyboard commands one might use to insert or modify them, or whether they are "action" terms and what they do.
 
9. Other key utilities include name completion in several name spaces, finding theorems and definitions that mention a given operator, finding theorems that explicitly cite a given lemma, finding ML global definitions that cite another given ML global identifier, and "in-place" typing of ML code, which is useful for understanding and correcting ML code piece by piece.
 
10. Informal material can be combined with formal material. Indeed, this documentation as well as that of Nuprl Basics was built that way with this editor.
 
11. The style of interaction is "on-the-fly". When a user creates or modifies source material, such as operator definitions, buttons, display methods, ML code for inference or utilities, it is immediately usable, and no "system rebuild" is required.

(Oct 2001 - sfa)
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
EditorDoc Sections Nuprl Doc