(version: 1.1.2)

3 cedille-mode commands

To enter Cedille navigation mode (invoking the backend), the command is Alt-s. In Cedille navigation mode, the following commands are available:

4 Navigation

f/F

Navigate to the next same-level node in the parse tree

b/B

Navigate to the previous same-level node in the parse tree

p

Navigate to the parent of the current node in the parse tree

n

Navigate to the previously visited child (first by default) node of the current node in the parse tree

a/e

Navigate to the first/last node in the current level of the parse tree

r/R

Select next/previous error

t/T

Select first/last error in file

j

Jump to location associated with selected node

g

Clear current selection

,/.

Navigate to the previous/next page in browsing history

</>

Navigate to the first/last page in browsing history

5 Information

i/I

Toggle info mode (provides information about the currently selected node)

c/C

Toggle context mode (provides information about the context of the currently selected term)

s/S

Toggle summary mode (provides information about the contents of the entire file)

x/X

Toggle scratch mode

h

Open information documents describing how to use Cedille mode

1

Close all emacs windows except the current one; convenience keystroke for emacs command delete-other-windows.

#

Highlight/unhighlight all instances of the selected symbol (context-sensitive)

6 Interactive

If associated with a span (and the beginning and end characters of the span were not deleted), each of these commands will be re-called each time you enter into Cedille mode. They all begin with the ’C-i’ prefix.

C-i n

Show normalization of selected span. If no span is selected, this will prompt an expression to normalize.

C-i h

Like ’C-i n’, but shows head-normalization

C-i u

Show a single reduction of the selected span

C-i e

Show erasure of selected span. If no span is selected, this will prompt an expression to erase.

C-i r

Remove all interactive attributes associated with the selected span

C-i R

Remove all interactive attributes

C-i b

Open the beta-reduction buffer with an input expression. Copies global scope and local scope if a span is selected.

C-i B

Open the beta-reduction buffer with the selected span

C-i t

Open the beta-reduction buffer with the selected span’s expected type (or type if there is no expected type)

7 Other

M-x

Copy the selected span to the scratch buffer

C-h <int>

Alters highlighting scheme depending on value of <int>: 1: default highlighting 2: language level highlighting 3: checking mode highlighting

q/M-s/C-g

Quit Cedille mode

K

Kill the Cedille process and restart it if it is taking an unusually long time

$

Open customization window for configuring Cedille mode