From 71e1555eb4e31c04cbc607d13d2418019576ca87 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Dec 2014 13:09:23 -0800 Subject: [PATCH] feat(emacs): use lean-mode for .hlean --- bin/linja | 59 +++++++++++++++++++++++++++------------ src/emacs/lean-company.el | 8 ++++++ src/emacs/lean-mode.el | 2 ++ 3 files changed, 51 insertions(+), 18 deletions(-) diff --git a/bin/linja b/bin/linja index 63983d5b6..67f9a7c26 100755 --- a/bin/linja +++ b/bin/linja @@ -318,9 +318,12 @@ def process_args(args): args.cache = process_target(args.cache) if len(args.targets) != 1: error("--cache option can only be used with one target") - if not args.cache.endswith(".lean"): - error("cache argument has to be ends with .lean") - args.cache = args.cache[:-4] + "clean" + if not args.cache.endswith(".lean") and not args.cache.endswith(".hlean"): + error("cache argument has to end with .lean or .hlean") + if args.cache.endswith(".lean"): + args.cache = args.cache[:-4] + "clean" + else: + args.cache = args.cache[:-5] + "clean" args.phony_targets = list(set(g_phony_targets) & set(args.targets)) if args.verbose: g_logger.setLevel(logging.INFO) @@ -394,11 +397,14 @@ def handle_flycheck_failure(out, err, args): if failed: call_lean(target, args) -def process_lean_output(target, out, args): +def process_lean_output(target, out, args, using_hlean): n = args.flycheck_max_messages if target.endswith(".olean"): - target = target[:-5] + "lean" - if not target.endswith(".lean"): + if using_hlean: + target = target[:-5] + "hlean" + else: + target = target[:-5] + "lean" + if (not target.endswith(".lean") and not using_hlean) or (not target.endswith(".hlean") and using_hlean): print out return # Parse, filter, and remove extra items @@ -419,6 +425,8 @@ def call_ninja(args): for item in args.targets: if item.endswith(".lean"): targets.append(item[:-4] + "olean") + elif item.endswith(".hlean"): + targets.append(item[:-5] + "olean") else: targets.append(item) proc_out = proc_err = None @@ -431,8 +439,8 @@ def call_ninja(args): proc = subprocess.Popen([g_ninja_path] + ninja_option + targets, stdout=proc_out, stderr=proc_err) (out, err) = proc.communicate() if args.flycheck: - if len(args.targets) == 1 and args.targets[0].endswith(".lean"): - process_lean_output(targets[0], out, args) + if len(args.targets) == 1 and (args.targets[0].endswith(".lean") or args.targets[0].endswith(".hlean")): + process_lean_output(targets[0], out, args, args.targets[0].endswith(".hlean")) handle_flycheck_failure(out, err, args) else: print out + err @@ -443,17 +451,20 @@ def call_lean(filename, args): proc = subprocess.Popen([g_lean_path] + args.lean_options + [filename], stdout=subprocess.PIPE, stderr=subprocess.STDOUT) out = proc.communicate()[0] - process_lean_output(filename, out, args) + process_lean_output(filename, out, args, filename.endswith(".hlean")) return proc.returncode -def get_lean_names(lean_file, args): +def get_lean_names(lean_file, args, using_hlean): lean_file = os.path.abspath(lean_file) basename, ext = os.path.splitext(lean_file) basename = normalize_drive_name(basename) - lean_name_exts = ["lean", "olean", "clean", "ilean", "d"] item = {"base" : basename} + lean_name_exts = ["lean", "olean", "clean", "ilean", "d"] for ext in lean_name_exts: - item[ext] = basename + "." + ext + if ext == "lean" and using_hlean: + item[ext] = basename + ".hlean" + else: + item[ext] = basename + "." + ext if args.cache and len(args.targets) == 1 and item['lean'] == args.targets[0]: item['clean'] = args.cache return item @@ -493,13 +504,25 @@ def find_lean_files(args): files |= set(find_files(project_dir, pattern)) for pattern in exclude_patterns: files -= set(find_files(project_dir, pattern)) + has_lean = False + has_hlean = False for file in args.targets: if file.endswith(".lean"): + has_lean = True + if file.endswith(".hlean"): + has_hlean = True + if has_lean and has_hlean: + error("project cannot mix .lean and .hlean files") + for file in args.targets: + if file.endswith(".lean") or file.endswith(".hlean"): files.add(file) elif file.endswith(".olean"): - file.add(file[:-5] + "lean") + if has_hlean: + file.add(file[:-5] + "hlean") + else: + file.add(file[:-5] + "lean") for f in files: - find_lean_files.cached_list.append(get_lean_names(f, args)) + find_lean_files.cached_list.append(get_lean_names(f, args, has_hlean)) return find_lean_files.cached_list # Initialize static variable @@ -590,9 +613,9 @@ def make_deps_all_files(args): threads = [] i, num_of_files = 1, len(lean_files) for item in lean_files: - lean_file = item['lean'] - dlean_file = item['d'] - olean_file = item['olean'] + lean_file = item['lean'] + dlean_file = item['d'] + olean_file = item['olean'] if not os.path.isfile(dlean_file) or os.path.getmtime(dlean_file) < os.path.getmtime(lean_file): thread = threading.Thread(target=make_deps, args = [lean_file, dlean_file, olean_file]) sys.stderr.write("[%i/%i] generating dep... % -80s" % (i, num_of_files, dlean_file)) @@ -630,7 +653,7 @@ def main(argv=None): + g_project_filename + " file at the project root.") returncode = 0 for filename in args.targets: - if os.path.isfile(filename) and filename.endswith(".lean"): + if os.path.isfile(filename) and (filename.endswith(".lean") or filename.endswith(".hlean")): returncode |= call_lean(filename, args) return returncode diff --git a/src/emacs/lean-company.el b/src/emacs/lean-company.el index d435e5b23..a04d2a905 100644 --- a/src/emacs/lean-company.el +++ b/src/emacs/lean-company.el @@ -37,10 +37,18 @@ (s-left (- (length file-name) (length "/default.lean")) file-name)) + ((s-ends-with? "/default.hlean" file-name) + (s-left (- (length file-name) + (length "/default.hlean")) + file-name)) ((s-ends-with? ".lean" file-name) (s-left (- (length file-name) (length ".lean")) file-name)) + ((s-ends-with? ".hlean" file-name) + (s-left (- (length file-name) + (length ".hlean")) + file-name)) (t file-name))) (defun company-lean--import-candidates-main (root-dir) diff --git a/src/emacs/lean-mode.el b/src/emacs/lean-mode.el index 4ab969620..d4f078cab 100644 --- a/src/emacs/lean-mode.el +++ b/src/emacs/lean-mode.el @@ -214,10 +214,12 @@ Invokes `lean-mode-hook'. ;; Automatically use lean-mode for .lean files. ;;;###autoload (push '("\\.lean$" . lean-mode) auto-mode-alist) +(push '("\\.hlean$" . lean-mode) auto-mode-alist) ;; Use utf-8 encoding ;;;### autoload (modify-coding-system-alist 'file "\\.lean\\'" 'utf-8) +(modify-coding-system-alist 'file "\\.hlean\\'" 'utf-8) ;; Flycheck init (when lean-flycheck-use