From e522343c88f90ed93dfd85ea3aae3e80792bad48 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 24 May 2017 20:51:09 -0400
Subject: [PATCH] doc(emacs): move configurations to emacs readme and expand
 try it out section

---
 doc/make/ubuntu-12.04-detailed.md | 32 ---------------------
 src/emacs/README.md               | 47 +++++++++++++++++++++++++++++--
 2 files changed, 45 insertions(+), 34 deletions(-)

diff --git a/doc/make/ubuntu-12.04-detailed.md b/doc/make/ubuntu-12.04-detailed.md
index 914aba322..2ae52c3cc 100644
--- a/doc/make/ubuntu-12.04-detailed.md
+++ b/doc/make/ubuntu-12.04-detailed.md
@@ -56,36 +56,4 @@ Preparing working environment on Ubuntu 12.04
     cmake -D CMAKE_BUILD_TYPE=Release -D BOOST=ON ../src
     make
 
-### If you are using Emacs, here are some basic configurations (optional)
-
-    (custom-set-variables
-      '(c-basic-offset 4)
-      '(global-font-lock-mode t nil (font-lock))
-      '(show-paren-mode t nil (paren))
-      '(transient-mark-mode t))
-
-
-    (tool-bar-mode -1)
-    (setq visible-bell t)
-    (setq-default indent-tabs-mode nil)
-    (setq visible-bell t)
-    (column-number-mode 1)
-
-    ;; Coding Style
-    (setq auto-mode-alist (cons '("\\.h$" . c++-mode) auto-mode-alist))
-    (defconst my-cc-style
-      '("cc-mode"
-       (c-offsets-alist . ((innamespace . [0])))))
-    (c-add-style "my-cc-mode" my-cc-style)
-    (add-hook 'c++-mode-hook '(lambda ()
-                                 (c-set-style "my-cc-mode")
-                                 (gtags-mode 1)
-                                ))
-
-    ;; C++ 11 new keywords
-    (font-lock-add-keywords 'c++-mode
-       '(("\\<\\(thread_local\\)\\>" . font-lock-warning-face)
-        ("\\<\\(constexpr\\)\\>" . font-lock-keyword-face)
-        ))
-
 ### You need to also set up the [Emacs Mode](../../src/emacs/README.md).
diff --git a/src/emacs/README.md b/src/emacs/README.md
index 351cb3085..b8133319e 100644
--- a/src/emacs/README.md
+++ b/src/emacs/README.md
@@ -152,6 +152,14 @@ that there are no errors and one piece of information displayed. Whenever
 you type, an asterisk should briefly appear after ``FlyC``, indicating that
 your file is being checked.
 
+If you get an error which contains `failed to lock file`, you need to create a `.project` file:
+- open a `.lean` or `.hlean` file
+- go to menu-bar (top of screen) -> Lean -> Create a new project
+- click open
+- it will ask "standard or hott": type which mode you want to use and press enter
+- now it has created a project file (which manages imports and so on for files outside the library), and if you go back to your `.lean` or `.hlean` file these error messages will disappear.
+
+
 
 Key Bindings and Commands
 =========================
@@ -181,6 +189,41 @@ To profile Lean performace on the file in the buffer, enter <kbd>M-x lean-execut
 `Lean execute` from the Lean menu, and add the option `--profile`.
 
 
+Some basic configurations (optional)
+====================================
+
+```lisp
+(custom-set-variables
+  '(c-basic-offset 4)
+  '(global-font-lock-mode t nil (font-lock))
+  '(show-paren-mode t nil (paren))
+  '(transient-mark-mode t))
+
+
+(tool-bar-mode -1)
+(setq visible-bell t)
+(setq-default indent-tabs-mode nil)
+(setq visible-bell t)
+(column-number-mode 1)
+
+;; Coding Style
+(setq auto-mode-alist (cons '("\\.h$" . c++-mode) auto-mode-alist))
+(defconst my-cc-style
+  '("cc-mode"
+   (c-offsets-alist . ((innamespace . [0])))))
+(c-add-style "my-cc-mode" my-cc-style)
+(add-hook 'c++-mode-hook '(lambda ()
+                             (c-set-style "my-cc-mode")
+                             (gtags-mode 1)
+                            ))
+
+;; C++ 11 new keywords
+(font-lock-add-keywords 'c++-mode
+   '(("\\<\\(thread_local\\)\\>" . font-lock-warning-face)
+    ("\\<\\(constexpr\\)\\>" . font-lock-keyword-face)
+    ))
+```
+
 Known Issues and Possible Solutions
 ===================================
 
@@ -207,10 +250,10 @@ You may also need to install [emacs-unicode-fonts](https://github.com/rolandwalk
  - Run `M-x package-refresh-contents`, `M-x package-install`, and type `unicode-fonts`.
  - Add the following lines in your emacs setup:
 
-   ```lisp
+```lisp
 (require 'unicode-fonts)
 (unicode-fonts-setup)
-   ```
+```
 
 Contributions
 =============