README...

diff --git a/README.md b/README.md
index ae3781144334fa8c8206b5d6b652264e70825fe4..a9180c7e1fdf63ea0b2e78df970c587063391b49 100644 (file)
--- a/README.md
+++ b/README.md
@@ -64,6 +64,18 @@ To enable the debugging mode add the -d flag. In the interaction loop
 type :h to get a list of available commands. Note that the current
 directory will be taken as the search path for the imports.
 
+To enable emacs to edit ```*.ctt``` files in ```ctt-mode```, add the following
+line to your ```.emacs``` file:
+```
+(autoload 'ctt-mode "cubicaltt" "cubical editing mode" t)
+(setq auto-mode-alist (append auto-mode-alist '(("\\.ctt$" . ctt-mode))))
+```
+and ensure that the file ```cubicaltt.el``` is visible in one of the diretories
+on emacs' ```load-path```, or else load it in advance, either manually with
+```M-x load-file```, or with something like the following line in ```.emacs```:
+```
+(load-file "cubicaltt.el")
+```
 
 References and notes
 --------------------

diff --git a/examples/demo.ctt b/examples/demo.ctt
index f01b1b85922f6fcdb430a754df01e537f1bd1c99..f2f8e78a967ea21a0ebf64a871164f148216ebd0 100644 (file)
--- a/examples/demo.ctt
+++ b/examples/demo.ctt
@@ -416,3 +416,9 @@ generalize normal inductive types by allowing constructors that define
   - examples/integer.ctt: The integers as a HIT.
 
 -}
+
+{-
+Local Variables:
+compile-command: "echo :q | ../cubical demo.ctt"
+End:
+-}