Subject: GUI

Keywords: ::structure-editor
          ::text
          ::term

Title: Term Text

--------------------------------------------------
Everything in nuprl is a term.
The text you are reading is a term Ie:
EXPLODED<<!text{The text you are reading is a term :s,}
            ()>> 

ML code you enter into an object or the proof editor is a term.
The ML compiler compiles text. Thus the ML code is text embedded in a term.
This can be done as string parameters of !text{s}() terms, joined by
!text_cons(0;0) terms which are interpreted by the ML scanner as text.
One can also define definitions which expand to such text terms. Where
and when such expansions happen is determened by the condition tags and
description property of the definition.
Such definitions will normally have slots which can contain embedded text.
Terms are common arguments to ML functions. They can in turn be embedded in
text as subterms of a !text_cons(0;0). The ML scanner will treat any term
which it does not recognize as text as a literal term. Thus no special syntax
or markers are needed to embed term literals in text. Historically though, 
term literals where identified by quasi-quotatation marks, eg: ⌜literal⌝.  
These quotes are not entered as character but as a !prl(0) term that displays
the quotes and is ignored by the scanner. 

In the editor you can open a slot to insert a term into text with the (c-o)
or (c-u) commands. The latter includes the quasi-quotation marks. 

Hopefully you shouldn't need to be aware of how the text embedding is
implemented, However the embedded text primitive operators are:
!text{<text>:s}()
!text_cons(0;0)
!ml_text_cons(0;0)
!newline()

!ml_tlx_cons is a definition that expands to embedded text and is used
in the ML TopLoop.

There are different flavors of text cons as there are different uses of text.
ML source used !ml_text_cons and most everything else uses !text_cons. 
In retrospect, we should have used a single operator for text cons but we
expected we'd want the editor to behave differently depending on context and
the varying cons-op allow easy discrimination of context. While that is true
there are other ways to determine context and the multiple cons ops create 
annoying problems when one is embedded in the other.

(cm-a)ctc will cause consistent use of the top text cons
op throught the hi-lited text block. 
  
⋅
--------------------------------------------------

Authors: RICH:t

Contributors: NUPRL:t

⋅

Home