From 254d8619707b5754f2fd1d972611d414329c91a0 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Mon, 15 Sep 2014 13:02:02 -0700
Subject: [PATCH] feat(bin/linja): pass -D config option to lean

Close #196
---
 bin/linja                  | 8 +++++---
 src/emacs/lean-flycheck.el | 2 ++
 2 files changed, 7 insertions(+), 3 deletions(-)

diff --git a/bin/linja b/bin/linja
index 3ec32b02f..f44d26391 100755
--- a/bin/linja
+++ b/bin/linja
@@ -404,13 +404,14 @@ def expand_target_to_fullname(target):
 def parse_arg(argv):
     global g_working_dir
     parser = argparse.ArgumentParser(description='linja: ninja build wrapper for Lean theorem prover.')
-    parser.add_argument('--flycheck', '-F', action='store', type=int, default=None, const=120, nargs='?', help="Use --flycheck option for Lean.")
+    parser.add_argument('--flycheck', '-F', action='store_true', default=False, help="Use --flycheck option for Lean.")
     parser.add_argument('--flycheck-max-messages', action='store', type=int, default=None, const=999999, nargs='?', help="Number of maximum flycheck messages to display.")
     parser.add_argument('--cache', action='store', help="Use specified cache (clean) file.")
     parser.add_argument('--directory', '-C', action='store', help="change to DIR before doing anything else.")
+    parser.add_argument('--lean-config-option', '-D', action='append', help="set a Lean configuration option (name=value)")
     parser.add_argument('targets', nargs='*')
     args = parser.parse_args(argv)
-    if (args.flycheck == None and args.flycheck_max_messages != None):
+    if (args.flycheck == False and args.flycheck_max_messages != None):
         error("Please use --flycheck option with --flycheck-max-messages option.")
     if args.cache:
         args.cache = expand_target_to_fullname(args.cache)
@@ -430,7 +431,8 @@ def get_lean_options(args):
     options = []
     if args.flycheck:
         options.append("--flycheck")
-        options.append("-D pp.width=%d" % args.flycheck)
+    for item in args.lean_config_option:
+        options.append("-D" + item)
     return options
 
 def clear_cache(project_dir, args):
diff --git a/src/emacs/lean-flycheck.el b/src/emacs/lean-flycheck.el
index 26b2ba080..8cc3f9aa1 100644
--- a/src/emacs/lean-flycheck.el
+++ b/src/emacs/lean-flycheck.el
@@ -5,6 +5,7 @@
 ;;
 
 (require 'lean-settings)
+(require 'lean-option)
 
 (defun lean-flycheck-command ()
   "Concat lean-flychecker-checker-name with options"
@@ -13,6 +14,7 @@
                   lean-flycheck-checker-options
                   '("--cache")
                   '(source-original)
+                  '((eval (lean-option-string)))
                   '("--")
                   '(source-inplace)))