EditorDoc Sections Nuprl Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Executing ML code with `{(m-z)(cm-z)}'. doc for ml execution cmds

Execute the term in ML, and return the textual response, indicating the type and value, or an error message, in a cover.
For example, you can easily find the type of an identifier this way; using this command on the identifier quicksort gives,

NOTICE: - : ((* -> * -> bool) -> * list -> * list) quicksort

If the ML name cache is active, which is the default (CLICK HERE if you need to activate it), and the term has free non-global variables as proper subexpressions then the type of the whole expression as well as the free variables will be ascertained if possible; if not, perhaps because it is not well typed, the lambda closure of the term (using its free identifiers that aren't cached) will be evaluated instead. This is especially handy for finding the types of subexpressions, and the types expected for its free identifiers. For example

NOTICE: *+int a int* list
b int* list list
x bool if x then (inl (last (hd a.b) 1)) else inr 0

The cover (NOTICE: <term> <term>) is easily removed with `(c-d)' or `(mouseleft)'.

DEFICIENCY: The utility misbehaves when evaluating a subterm that happens to contain cached ML identifiers that are bound above the point. A version of this function that would scan up for the context was too slow, so this inferior functionality was adopted. When you have no interest in the global binding of some identifier that you're using locally, it is sometimes worthwhile to remove the identifier from the cache with the aptly named button in the ML edit menu (ML) which you should be able to raise through the main menu (main menu).
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

EditorDoc Sections Nuprl Doc