Skip to content

Commit

Permalink
Merge branch 'emacs-kbd-manual' of https://github.com/adamse/agda
Browse files Browse the repository at this point in the history
  • Loading branch information
@phile314
phile314 committed Oct 22, 2015
2 parents c087dec + 73110dd commit ace9318
Show file tree
Hide file tree
Showing 3 changed files with 113 additions and 1 deletion.
8 changes: 8 additions & 0 deletions doc/user-manual/tools/auto.rst
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
.. _auto:

*****************************
Automatic Proof Search (Auto)
*****************************

.. note::
This is a stub.
104 changes: 104 additions & 0 deletions doc/user-manual/tools/emacs-mode.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,3 +6,107 @@ Emacs Mode

.. note::
This is a stub.


Keybindings
===========

Commands working with types can be prefixed with ``C-u`` to compute
type without further normalisation and with ``C-u C-u`` to compute
normalised types.


Global commands
~~~~~~~~~~~~~~~

+-------------------------+-------------------------------------------------+
|``C-c C-l`` |**L**\ oad file |
+-------------------------+-------------------------------------------------+
|``C-c C-x C-c`` |**C**\ ompile file |
+-------------------------+-------------------------------------------------+
|``C-c C-x C-q`` |**Q**\ uit, kill the Agda process |
+-------------------------+-------------------------------------------------+
|``C-c C-x C-r`` |Kill and **r**\ estart the Agda process |
+-------------------------+-------------------------------------------------+
|``C-c C-x C-d`` |Remove goals and highlighting (**d**\ eactivate) |
| | |
+-------------------------+-------------------------------------------------+
|``C-c C-x C-h`` |Toggle display of **h**\ idden arguments |
+-------------------------+-------------------------------------------------+
|``C-c C-=`` |Show constraints |
+-------------------------+-------------------------------------------------+
|``C-c C-s`` |**S**\ olve constraints |
+-------------------------+-------------------------------------------------+
|``C-c C-?`` |Show all goals |
+-------------------------+-------------------------------------------------+
|``C-c C-f`` |Move to next goal (**f** \orward) |
+-------------------------+-------------------------------------------------+
|``C-c C-b`` |Move to precious goal (**b**\ ackwards) |
+-------------------------+-------------------------------------------------+
|``C-c C-d`` |Infer (**d**\ educe) type |
| | |
+-------------------------+-------------------------------------------------+
|``C-c C-o`` |M\ **o**\ dule c\ **o**\ ntents |
+-------------------------+-------------------------------------------------+
|``C-c C-n`` |Compute **n**\ ormal form |
+-------------------------+-------------------------------------------------+
|``C-u C-c C-n`` |Compute normal form, ignoring ``abstract`` |
| | |
+-------------------------+-------------------------------------------------+
|``C-c C-x M-;`` |Comment/uncomment rest of buffer |
+-------------------------+-------------------------------------------------+


Commands in context of a goal
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

+-------------------------+--------------------------------------------------------+
|``C-c C-SPC`` |Give (fill goal) |
+-------------------------+--------------------------------------------------------+
|``C-c C-r`` |**R**\ efine. Partial give: makes new holes for missing |
| |arguments |
+-------------------------+--------------------------------------------------------+
|``C-c C-a`` |:ref:`auto` |
+-------------------------+--------------------------------------------------------+
|``C-c C-c`` |**C**\ ase split |
+-------------------------+--------------------------------------------------------+
|``C-c C-h`` |Compute type of **h**\ elper function and add type |
| |signature to kill ring (clipboard) |
+-------------------------+--------------------------------------------------------+
|``C-c C-t`` |Goal **t**\ ype |
+-------------------------+--------------------------------------------------------+
|``C-c C-e`` |Context (**e**\ nvironment) |
+-------------------------+--------------------------------------------------------+
|``C-c C-d`` |Infer (**d**\ educe) type |
+-------------------------+--------------------------------------------------------+
|``C-c C-,`` |Goal type and context |
+-------------------------+--------------------------------------------------------+
|``C-c C-.`` |Goal type, context and inferred type |
+-------------------------+--------------------------------------------------------+
|``C-c C-o`` |M\ **o**\ dule c\ **o**\ ntents |
+-------------------------+--------------------------------------------------------+
|``C-c C-n`` |Compute **n**\ ormal form |
+-------------------------+--------------------------------------------------------+
|``C-u C-c C-n`` |Compute normal form, ignoring ``abstract`` |
| | |
+-------------------------+--------------------------------------------------------+


Other commands
~~~~~~~~~~~~~~

+-------------------------+----------------------------------------+
|``TAB`` |Indent current line, cycles between |
| |points |
+-------------------------+----------------------------------------+
|``S-TAB`` |indent curent line, cycles in opposite |
| |direction |
+-------------------------+----------------------------------------+
|``M-.`` |Go to definition of identifier under |
| |point |
+-------------------------+----------------------------------------+
|Middle mouse button |Go to definition of identifier clicked |
| |on |
+-------------------------+----------------------------------------+
|``M-*`` |Go back |
+-------------------------+----------------------------------------+
2 changes: 1 addition & 1 deletion doc/user-manual/tools/index.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ Tools
:maxdepth: 2

emacs-mode
auto
compilers
generating-html
generating-latex
package-system

0 comments on commit ace9318

Please sign in to comment.