From 1c5497e632ef6bc7809a8ef54859ee120356421e Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Wed, 10 Sep 2014 15:18:26 -0700
Subject: [PATCH] feat(emacs/lean-project): add lean-project-create to imenu

Related with #170
---
 src/emacs/lean-mode.el    |  2 ++
 src/emacs/lean-project.el | 40 +++++++++++++++++++++++++++++++++++++++
 2 files changed, 42 insertions(+)
 create mode 100644 src/emacs/lean-project.el

diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el
index 7f90baa7e..5bd74c334 100644
--- a/src/emacs/lean-mode.el
+++ b/src/emacs/lean-mode.el
@@ -26,6 +26,7 @@
 (require 'lean-mmm-lua)
 (require 'lean-company)
 (require 'lean-server)
+(require 'lean-project)
 
 (defun lean-compile-string (exe-name args file-name)
   "Concatenate exe-name, args, and file-name"
@@ -93,6 +94,7 @@
   "Menu for the Lean major mode"
   `("Lean"
     ["Execute lean"         lean-execute                      t]
+    ["Create a new project" (call-interactively 'lean-project-create) (not (lean-project-inside-p))]
     "-----------------"
     ["Show type info"       lean-eldoc-documentation-function lean-eldoc-use]
     ["Fill a placeholder"   lean-fill-placeholder             (looking-at  (rx symbol-start "_"))]
diff --git a/src/emacs/lean-project.el b/src/emacs/lean-project.el
new file mode 100644
index 000000000..c0b82d763
--- /dev/null
+++ b/src/emacs/lean-project.el
@@ -0,0 +1,40 @@
+;; Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+;; Released under Apache 2.0 license as described in the file LICENSE.
+;;
+;; Author: Soonho Kong
+;;
+
+(require 'flycheck)
+(require 'lean-util)
+
+(defconst lean-project-file-name ".project"
+  "Project file name")
+
+(defun lean-project-find-root ()
+  (lean-find-file-upward lean-project-file-name))
+
+(defun lean-project-inside-p ()
+  (if (lean-project-find-root) t nil))
+
+(defun lean-project-create (directory)
+  (interactive
+   (list (read-directory-name "Project root: ")))
+  (let ((project-file (concat (file-name-as-directory directory)
+                               lean-project-file-name)))
+    (if (file-exists-p project-file)
+        (user-error "project-file %s already exists" project-file))
+    (find-file project-file)
+    (insert (string-join '("# Lean project file"
+                           ""
+                           "# Include all .lean files under this directory"
+                           "+ *.lean"
+                           ""
+                           "# Exclude flycheck generated temp files"
+                           "- flycheck*.lean"
+                           ""
+                           "# Exclude emacs temp files"
+                           "- .#*.lean")
+                         "\n"))
+    (save-buffer)))
+
+(provide 'lean-project)