(version: 1.1.2)

20 Context buffer

The context buffer for Cedille allows the user to see the local variables in scope for the currently selected node. To display the context buffer, select a node and press C; this will open the context buffer and jump to it. If you just want to open the context buffer (but not jump to it), press c instead.

The context buffer has several built-in features to organize data:

• Sort entries alphabetically or by binding position
• Filter entries according to common properties. Only one filter may be active at a time.
• Show or hide shadowed variables

21 Controls

a/z

Sort all entries alphabetically from a-z/z-a

d/u

Sort all entries according to binding position in parse tree (descending/ascending)

e

Filter out entries that do not have an ’≃’ symbol

E

Filter out entries that are not literal statements of β-equality

f

Clear current filter so all entries are shown

s

Toggle display of shadowed variables

w

Hide or unhide type or kind of line currently under cursor

W

Unhide all types and kinds hidden with ’w’

c/C

Close the context mode window

h

Open information page for context mode

(version: 1.1.2)

22 Common commands

M-c

Copy the contents of the current buffer to the scratch buffer

+

Increase the size of the buffer by one line

-

Decrease the size of the buffer by one line

=

Reset the buffer’s size

f

Moves to the next defined variable in the buffer

b

Moves to the previous defined variable in the buffer

a

Moves to the first defined variable in the buffer

e

Moves to the last defined variable in the buffer

j

Jumps to the definition of the selected variable